Lambda Calculus
Sam Goto

Three Rules:
 Variable: every variable (e.g.
x
) is a λterm  Abstraction: if M is a λterm and x is a variable, then
(λx[M])
is a λterm (sometimes,.
is also used as a separator, e.g.(λ x . M)
). e.g.(λx[x])
(x
is the argument andM
is what the function returns). You can also chain, e.g.λx[λy[x]]
, currying: instead of having functions that take multiple arguments, all functions take a single argument. Currying can delay parts of a function to be called later.  Application: if M and N are λterms, then so is
(M N)
. e.g.(M N)
, takes an abstraction and applies a parameter to it:
 Variable: every variable (e.g.

For example, here is the dentity function:
λx[x]
. It takes anx
and returnsx
. 
Here is a possible enconding of
TRUE
andFALSE
:λx[λy[x]]
andλx[λy[y]]
respectively. 
From there, you can define
NOT
,AND
,OR
, and so on. 
And encode arithmetic using church's encoding.

Examples: S =
λx[λy[λz[xz(yz)]]]
, K =λx[λy[x]]
.