Primer on Lambda Calculus


The fundamental concept in lambda calculus is the notion if an expression. An expression is defined as

    \begin{equation*} <expression> = <name> | <function> | <application> \end{equation*}


A name, also called a variable, is an identifier which, in general, can be any of the letters a, b, c, \cdots z. For example, x.


An function is defined as

    \begin{equation*} <function> = \lambda <name> \cdot <expression> \end{equation*}

An example of a function is the following

    \begin{equation*}      \lambda x.x \end{equation*}

This expression defines the identity function. The name after the \lambda is the identifier or the argument of this function. The expression after the point (in this case a single x) is called the body of the function.

Functions can be applied to expressions.


An application is defined as

    \begin{equation*} <application> = <expression> @ <expression> \end{equation*}

An example of an application is the following

    \begin{equation*}      (\lambda x.x) @ y \end{equation*}

This is the identity function applied to y. Parenthesis are used for clarity in order to avoid ambiguity. Function applications are evaluated by substituting the value of the argument x (in this case y) in the body of the function definition, i.e.

    \begin{equation*}      (\lambda x.x) @ y = [y/x]x = y \end{equation*}

In this transformation the notation [y/x] is used to indicate that all occurrences of x are substituted by y in the expression to the right.

Order of Evaluation

An expression can be surrounded with parenthesis for clarity, that is, if E is an expression, (E) is the same expression. The only keywords used in the language are \lambda and the dot. In order to avoid cluttering expressions with parenthesis, the convention is that function application associates from the left.

For example the expression

    \begin{equation*}      E_1 E_2 E_3 \cdots E_n \end{equation*}

is evaluated applying the expressions as follows

    \begin{equation*}      (\cdots ((E_1 E_2) E_3) \cdots E_n) \end{equation*}


In \lambda calculus all names are local to definitions. In the function \lambda x.x, x is bound since its occurrence in the body of the definition is preceded by \lambda x. A name not preceded by a \lambda is called a free variable. In the expression

    \begin{equation*}      (\lambda x.xy)  \end{equation*}

the variable x is bound and y is free. In the expression

    \begin{equation*}      (\lambda x.x)(\lambda y.yx)  \end{equation*}

The x in the body of the first expression from the left is bound to the first \lambda. The y in the body of the second expression is bound to the second \lambda and the x is free. It is very important to notice that the x in the second expression is totally independent of the x in the first expression.

Be careful when performing substitutions to avoid mixing up free occurrences of an identifier with bound ones. In the expression

    \begin{equation*}      (\lambda x.(\lambda y.xy)) @ y  \end{equation*}

the function to the left contains a bound y, whereas the y at the right is free. Simply by renaming the bound y to t, this confusion is avoided

    \begin{equation*}      (\lambda x.(\lambda t.xt)) @y = (\lambda      \end{equation*}


    \begin{align*}      \lambda x.eats(x)@john & = [john/x]eats(x) \\ & = eats(john) \\ \end{align*}

    \begin{align*}      \lambda y. \lambda x. eats(x, y)@rice & = [rice/y]\lambda x. eats(x, y) \\ & = \lambda x. eats(x, rice) \\ \end{align*}

    \begin{align*}      \lambda y. \lambda x. eats(x, y) @rice @john  & = ((\lambda y . \lambda x. eats(x, y) @rice) @john) \\ & = ([rice/y]\lambda x. eats(x, y) @john) \\ & = (\lambda x. eats(x, rice) @john) \\ & = [john/x] eats(x, rice) \\ & = eats(john, rice) \\ \end{align*}

    \begin{align*}      \lambda w. \lambda z. \forall x(w@x \rightarrow z@x) @\lambda y.boxer(y)  &= [\lambda y.boxer(y)/w] \lambda z. \forall x(w@x \rightarrow z@x) \\ &= \lambda z. \forall x(\lambda y.boxer(y)@x \rightarrow z@x) \\ &= \lambda z. \forall x([x/y]boxer(y) \rightarrow z@x) \\ &= \lambda z. \forall x(boxer(x) \rightarrow z@x) \\ \end{align*}

    \begin{align*}      \lambda w. \lambda z. \forall x(w@x \rightarrow z@x) @\lambda y.boxer(y) @\lambda y.walks(y) &= ([\lambda y.boxer(y)/w] \lambda z. \forall x(w@x \rightarrow z@x) @\lambda y.walks(y)) \\ &= (\lambda z. \forall x(\lambda y.boxer(y)@x \rightarrow z@x) @\lambda y.walks(y)) \\ &= (\lambda z. \forall x([x/y]boxer(y) \rightarrow z@x) @\lambda y.walks(y)) \\ &= (\lambda z. \forall x(boxer(x) \rightarrow z@x) @\lambda y.walks(y)) \\ &= [\lambda y.walks(y)/z] \forall x(boxer(x) \rightarrow z@x) \\ &= \forall x(boxer(x) \rightarrow \lambda y.walks(y)@x) \\ &= \forall x(boxer(x) \rightarrow [x/y].walks(y)) \\ &= \forall x(boxer(x) \rightarrow walks(x)) \\ \end{align*}

    \begin{align*}      \lambda v. \lambda z. \exists x(v@x \text{ } and \text{ } z@x) @\lambda y.plane(y) &= [\lambda y.plane(y)/v] \lambda z. \exists x(v@x \text{ } and \text{ } z@x) \\ &= \lambda z. \exists x(\lambda y.plane(y)@x \text{ } and \text{ } z@x) \\ &= \lambda z. \exists x([x/y]plane(y) \text{ } and \text{ } z@x) \\ &= \lambda z. \exists x(plane(x) \text{ } and \text{ } z@x) \\ \end{align*}

    \begin{align*}      F &= \lambda p. \lambda q.(p@(\lambda r.takes(q,r)))@(\lambda v. \lambda z. \exists x(v@x \text{ } and \text{ } z@x) @\lambda y.plane(y)) \\ &= \lambda p. \lambda q.(p@(\lambda r.takes(q,r)))@(\lambda z. \exists x(plane(x) \text{ } and \text{ } z@x)) \\ &= [\lambda z. \exists x(plane(x) \text{ } and \text{ } z@x)/p] \lambda q.(p@(\lambda r.takes(q,r))) \\ &= \lambda q.(\lambda z. \exists x(plane(x) \text{ } and \text{ } z@x)@(\lambda r.takes(q,r))) \\ &= \lambda q.([\lambda r.takes(q,r))/z] \exists x(plane(x) \text{ } and \text{ } z@x) \\ &= \lambda q.(\exists x(plane(x) \text{ } and \text{ } \lambda r.takes(q,r))@x) \\ &= \lambda q.(\exists x(plane(x) \text{ } and \text{ } [x/r] takes(q,r))) \\ &= \lambda q.(\exists x(plane(x) \text{ } and \text{ } takes(q,x))) \\ \end{align*}

    \begin{align*} F@john  &= \lambda q.(\exists x(plane(x) \text{ } and \text{ } takes(q,x))) @john \\ &= [john/q] (\exists x(plane(x) \text{ } and \text{ } takes(q,x))) \\ &= \exists x(plane(x) \text{ } and \text{ } takes(john,x)) \end{align*}


Leave a Reply

Your email address will not be published. Required fields are marked *