Primer on Lambda Calculus - The Beard Sage

Expression

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*}$

Name

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$ .

Function

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.

Application

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*}$

Scope

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 t.yt) \end{equation*}$

Examples

$\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*}$

References

https://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf