Resume

Research

Learning

Blog

Teaching

Jokes

Kernel Papers

Developed by Alonzo Church to establish the existence of an undecidable problem.

Like the SKI calculus, the $\lambda$-calculus focuses on functions, but unlike the SKI calculus, the $\lambda$-calculus$ has a notion of a variable. The $\lambda$-calculus is a context-free grammar where each expression can be reduced (“converted” into one of three possibilities:

- Variable, written \(x\)
- Abstraction (i.e., function definition), written \(\lambda x.e\), and interpreted as \(x\) is the input variable and \(e\) is the body of the function
- Application (i.e., function call), written \(e_1 e_2\)

Note that $\lambda x.e$ can be both a function definition, a function argument or even the result of a function. In shorthand, we write:

\[e \rightarrow x \lvert \lambda x . e \lvert e e\]The \(\lambda\)-calculus associates to the left, and the body of a \(\lambda\)-abstraction extends as far right as possible. Thus,

\[\lambda x.x \lambda y.y = \lambda x.(x \lambda y.y)\]In a function call e.g., \((\lambda x.e_1) e_2\), the formal parameter \(x\) is replaced
with the provided value e.g., \(e_1[x := e_2]\). This is called a *beta reduction*. The
substitution (reduction) rules are as follows:

- Identity \(I\) is defined as \(\lambda x.x\)
- Constant \(K\) is defined as \(\lambda z . \lambda y . z\)
- \((\lambda x.x) e\) is reduced to \(e\)
- \((\lambda x.y) e\) is reduced to \(y\)
- \((e_1 e_2)[x := e_3]\) is reduced to \((e_1[x := e_3])(e_2[x := e_3])\)
- \((\lambda x . e1)[x := e]\) is reduced to \((\lambda x . e1)\). This is because \((\lambda x. e1)\) is a function and the variable \(x\) does not appear in the expression
- \((\lambda y . e1)[x := e] = \lambda y . e1[x := e]\) if \(x \neq y\) and \(y \not \in FV(e)\) (see below Free Variables)

This last rule is intended to ensure that symbols refer to the proper variables. For instance, in \((\lambda y . x) [x = y]\), the \(y\) variable that we are substituting is different than the \(y\) formal parameter of the function. We do not want the substitution to return \(\lambda y . y\).

A variable is free if it isn’t governed by a \(\lambda\) i.e. there is no enclosing \(\lambda\) that defines the variables i.e. the free variables of an expression are the variables not bound in an abstraction (recalling that abstraction means function definition). Concretely

- \(FV(x) = \{ x \}\) i.e. the free variables in the expression consisting of a single variable \(x\) is exactly that variable
- \[FV(e_1 e_2) = FV(e_1) \cup FV(e_2)\]
- \(FV(\lambda x. e) = FV(e) - \{ x \}\) i.e. by using \(x\) as the formal parameter, that symbol \(x\) is no longer free

To avoid collisions, we can always rename bound variables i.e. \(\lambda x.x\) is the same as
\(lambda y.y\). Renaming bound variables is called *alpha conversion*

How can we implement booleans? We need an encoding of True and False. Similar to our approach in the SKI calculus, let’s define True as taking the first of two arguments and False as taking the second of two arguments.

\(True := \lambda x.\lambda y.x\) \(False := \lambda x.\lambda y. y\)

In the SKI calculus, we saw how the abstraction algorithm works. The \(\lambda\) calculus has a similar way to abstract. Suppose we want: \(True x y\) to evaluate to \(x\). To abstract the left hand side (LHS), move the variables from the LHS to the RHS and wrap with \(\lambda\):

\[True := \lambda x. \lambda y. x\]Similarily for False:

\[False := \lambda x. \lambda y. y\]We want \(pair x y z\) to become \(z x y\). Abstracting pair yields:

\[pair := \lambda x . \lambda y . \lambda z . z x y\]\(n\) applies its first argument \(n\) times to its second argument, meaning \(n f x\) should be equal to \(f^n(x)\). Abstracting:

\(0 f x\) should be reduced to \(x\), and thus \(0 = \lambda f . \lambda x . x\)

Succ (short for successor) should behave as \(succ n f x\) is \(f ( n f x)\); applying the abstraction algorithm yields $$succ := \lambda n . \lambda f . \lambda x . f (n f x).