Terms have to have the following form:
\x.M | Abstraction
(M N) | Application
x | Variable
const
\a.\b.a
omega (infinite recursion -> doesn't terminate)
(\f.(f f) \f.(f f))
y-combinator
\f.(\x.(f (x x)) \x.(f (x x)))
addition (on church numerals)
\n.\f.\x.(n (f x))