Phrase structure grammar
\(
\begin{array}{lcl}
< program > & ::= & < exp > \\
< exp > & ::= & < var\ exp > \\
& | & < lambda\ abs > \\
& | & < app\ exp > \\
& | & < church > \\
< lambda\ abs > & ::= & λ \ < var\ exp >\ .\ < exp > \\
< app\ exp > & ::= & '('\ < exp >\ < exp >\ ')' \\
< church > & ::= & < number > \\
& | & < number >\ + < number > \\
& | & < number >\ * < number > \\
& | & < boolean > \\
& | & < boolean >\ {\large ||\ } < boolean > \\
& | & < boolean >\ \&\& < boolean > \\
& | & ! < boolean > \\
\end{array}
\)
Lexical grammar
\(
\begin{array}{lcl}
< var\ exp > & ::= & < letter >\ (\ < letter >\ |\ < digit >\ |\ \ \_\ \ )^*\\
< digit > & ::= & 0\ |\ 1\ |\ 2\ |\ ...\ |\ 8\ |\ 9\\
< letter > & ::= & a\ |\ b\ |\ ...\ |\ z\ |\ A\ |\ B\ |\ ...\ |\ Z\\
< boolean > & ::= & true\quad |\quad false\\
< number > & ::= & < digit > \\
& | & (\ succ\ < number >\ ) \\
\end{array}
\)