Lambda Calculus

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 and M 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:

For example, here is the dentity function: λx[x]. It takes an x and returns x.

Here is a possible enconding of TRUE and FALSE: λ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]].

lambda calculus

lambda calculus