The Pragmatics of the Lambda Calculus

The lambda calculus represents a minimalistic, prototypical programming language. This post indicates how to develop "programs" in the lambda calculus.

Data Types

The lambda calculus is an intensional calculus of functions. Thus, how do we represent data in the lambda calculus?

The basic idea of the Scott encoding of data types is as follows. For each constructor of a data type, we append its formal parameters to a list of pattern matching handler parameters, one per constructor.

Example: Booleans

As an example, consider the booleans. In a functional programming language, we might write something like this:

data Bool = True | False

The Bool data type has two constructors:

• a nullary constructor True that constructs a fixed boolean outright (representing truth).
• a nullary constructor False that constructs a fixed boolean outright (representing falsity).

We would represent True using the Scott encoding as follows:

\[\text{TRUE} \equiv \lambda t . \lambda f . t.\]

Since True is a nullary constructor, the encoding accepts no additional parameters and consists solely of the pattern matching handler parameters and invokes the handler representing True, namely \(t\).

We would represent False using the Scott encoding as follows:

\[\text{FALSE} \equiv \lambda t . \lambda f . f.\]

Since False is a nullary constructor, the encoding accepts no additional parameters and consists solely of the pattern matching handler parameters and invokes the handler representing False, namely \(f\).

In a functional programming language, we can apply pattern matching to write functions whose domain is the booleans:

not True = False
not False = True

To represent not in the lambda calculus, we could write

\[\text{NOT} \equiv \lambda b . b ~\text{FALSE} ~\text{TRUE}.\]

Note that \(\text{NOT TRUE}\) evaluates to \(\text{FALSE}\) and \(\text{NOT FALSE}\) evaluates to \(\text{TRUE}\).

Example: Natural Numbers

As another example, consider the simplest recursive data type, the natural numbers. In a functional programming language, we might write something like this:

data Nat = Zero | Succ Nat

The Nat data type has two constructors:

• a nullary constructor Zero that constructs a fixed natural number outright (representing \(0\)).
• a unary constructor Succ that constructs a natural number, namely the successor, given another, previously constructed natural number (the predecessor) as input, i.e., it takes a number \(n\) and produces \(n+1\).

We would represent Zero using the Scott encoding as follows:

\[\text{ZERO} \equiv \lambda z . \lambda s . z.\]

Since Zero is a nullary constructor, the encoding accepts no additional parameters and consists solely of the pattern matching handler parameters and invokes the handler representing Zero, namely \(z\).

\[\text{SUCC} \equiv \lambda n . \lambda z . \lambda s . s n.\]

Since Succ is a unary constructor, the encoding accepts one additional parameter \(n\) representing the predcessor and additionally contains pattern matching parameters and invokes the handler representing Succ, namely \(s\) applied with argument \(n\).

In a functional programming language, we might then apply pattern matching to write functions whose domain is the natural numbers as follows:

isZero Zero = True
isZero (Succ _) = False

Thus, to represent the isZero function, we would write

\[\text{IS-ZERO} \equiv \lambda n . n ~ \text{TRUE} ~ (\lambda m . \text{FALSE}).\]

Note that \(\text{IS-ZERO ZERO}\) evaluates to \(\text{TRUE}\) and \(\text{IS-ZERO} (\text{SUCC}~ n)\) evaluates to \(\text{FALSE}\).

Recursive Functions

How can we represent recursive functions? Consider the following example:

double Zero = Zero
double (Succ n) = Succ (Succ (double n))

In programming languages, functions can refer to themselves by name and thus recur. The lambda calculus is a calculus of anonymous functions, however, so how can recursive functions be represented?

If we augment a lambda abstraction with an additional parameter \(r\) (representing a recursive call), we obtain the following representation:

\[\text{DOUBLE'} \equiv \lambda r . \lambda n . n ~ \text{ZERO} ~ (\lambda m . \text{SUCC} (\text{SUCC}~(r m))).\]

But what do we supply for \(r\)? If we can compute a fixed point of \(\text{DOUBLE'}\), i.e., a term \(\text{FIX DOUBLE'}\) such that \(\text{DOUBLE'}(\text{FIX DOUBLE'}) = \text{FIX DOUBLE'}\), then we may define

\[\text{DOUBLE} \equiv \text{FIX DOUBLE'}.\]

Note the following:

\begin{align*}\text{DOUBLE} &\equiv \text{FIX DOUBLE'} \\&= \text{DOUBLE'}(\text{FIX DOUBLE'}) \\&= \lambda n . n ~ \text{ZERO} ~ (\lambda m . \text{SUCC} (\text{SUCC}~((\text{FIX DOUBLE'}) ~m))) \\&= \lambda n . n ~ \text{ZERO} ~ (\lambda m . \text{SUCC} (\text{SUCC}~(\text{DOUBLE} ~m))).\end{align*}

Thus, we have effectively recovered self-reference via fixed points.

If it is possible to produce a fixed point for every closed lambda term, then this strategy will succeed. It is indeed possible to do so, but the method for doing so varies depending on the evaluation strategy used. For call-by-name, the following fixed point combinator works:

\[\text{Y} \equiv \lambda f . (\lambda x . f (x x)) (\lambda x . f (x x)).\]

Note the following:

\begin{align*}\text{Y}f &= (\lambda x . f (x x)) (\lambda x . f (x x)) \\&= f((\lambda x . f (x x)) (\lambda x . f (x x))) \\&= f(\text{Y}f)\end{align*}

Note, however, that for the call-by-value evaluation strategy, the term \(Yf =(\lambda x . f (x x)) (\lambda x . f (x x))\) would diverge since it would step to \(f(Yf)\) and then to \(f(f(Yf))\), etc., infinitely. For the call-by-name evaluation strategy, the unevaluated term \(Yf =(\lambda x . f (x x)) (\lambda x . f (x x))\) is substituted into the lambda abstraction for \(f\) and thus does not diverge prior to substitution. For the call-by-value strategy, an "eta-expanded" variant of the \(Y\) combinator (where the immediate self-application \(xx\) is replaced with a deferred self-application \(\lambda v . x x v\)) can be used:

\[\text{Z} \equiv \lambda f . (\lambda x . f (\lambda v . x x v)) (\lambda x . f (\lambda v . x x v)).\]

Note the following:

\begin{align*}\text{Z}f &= (\lambda x . f (\lambda v . x x v)) (\lambda x . f (\lambda v . x x v)) \\&= f (\lambda v . (\lambda x . f (\lambda v . x x v)) (\lambda x . f (\lambda v . x x v)) v) \\&= f(\lambda v . \text{Z}fv)\end{align*}

Thus, the \(\text{Z}\) combinator produces fixed points up to eta expansion. However, since \(\lambda v . fv \sim_{\mathrm{s}} f\) for either evaluation strategy \(\mathrm{s}\), it follows that

\[\mathrm{FIX} ~ f \sim_{\mathrm{s}} f(\mathrm{FIX}~f).\]

We can therefore define \(\text{FIX} = \text{Y}\) for call-by-name, and \(\text{FIX} = \text{Z}\) for call-by-value.

Thus, in general, fix point combinators compute fixed points up to equivalence (applicative bisimilarity).

Extrinsic Types

We can define extrinsic types, i.e., sets of lambda terms closed under term equivalence (applicative bisimilarity).

We define the universe of extrinsic types as follows:

\[\mathcal{T}_{\mathrm{s}} = \{T \subseteq \Lambda(\emptyset) \mid t \in T \land t \sim_{\mathrm{s}} t' \Rightarrow t' \in T\},\]

where \(\mathrm{s} \in \{\mathrm{n}, \mathrm{v}\}\) indicates the evaluation strategy.

An extrinsic type is therefore a saturated set of closed terms (i.e. a set closed under term equivalence).

Note that this set is a complete lattice when equipped with the \(\subseteq\) relation. This means that we can use this set as an ambient universe; inductive types are least fixed points of monotone operators on this universe, and coinductive types are greatest fixed points of monotone operators on this universe.

Meets

We define the meet of an arbitrary family of sets \(\mathcal{F} \subseteq \mathcal{T}\) as

\[\bigwedge \mathcal{F} = \bigcap \mathcal{F}.\]

Suppose \(t \in \bigwedge \mathcal{F}\) and \(t \sim_{\mathrm{s}} t'\). Then, for all \(T \in \mathcal{F}\), \(t \in T\), and hence \(t' \in T\), which means that \(t' \in \bigwedge \mathcal{F}\) and hence \(\bigwedge \mathcal{F} \in \mathcal{T}_{\mathrm{s}}\).

Joins

We define the join of an arbitrary family of set \(\mathcal{F}\) as

\[\bigvee \mathcal{F} = \bigcup \mathcal{F}.\]

Suppose \(t \in \bigvee \mathcal{F}\) and \(t \sim_{\mathrm{s}} t'\). Then, there exists a \(T \in \mathcal{F}\) such that \(t \in T\), and hence \(t' \in T\), which means that \(t' \in \bigvee \mathcal{F}\) and hence \(\bigwedge \mathcal{F} \in \mathcal{T}_{\mathrm{s}}\).

Least Element

The least element \(\bot\) is defined as

\[\bot = \emptyset.\]

This element vacuously satisfies the property of being closed under term equivalence. Furthermore, \(\bigwedge \mathcal{T}_{\mathrm{s}} = \bot\) as required.

Greatest Element

The greatest element \(\top\) is defined as

\[\top = \bigcup\mathcal{T}_{\mathrm{s}}.\]

This satisfies the closure property as already demonstrated, and it is trivially the case that \(\bigvee \mathcal{T}_{\mathrm{s}} = \top\).

Inductive Types

For the booleans, we define an inductive type \(\text{Bool}\) according to the following production rules:

\[\frac{}{t \in \text{Bool}}, \frac{}{\text{FALSE} \in \text{Bool}}, \frac{b \in \text{Bool}, t \sim_{\mathrm{s}} b}{t \in \mathrm{Bool}}.\]

In other words, we choose the least fixed point of the following monotone operator on \(\mathcal{T}_{\mathrm{s}}\):

\[F_{\text{Bool}}(B) = [\text{TRUE}] \cup [\text{FALSE}].\]

Here \([ \cdot ]\) denotes the equivalence class under \(\sim_{\mathrm{s}}\).

The type \(\text{Bool}\) is thus:

\[\text{Bool} = \mu F_{\text{Bool}}.\]

For the natural numbers, we consider the following production rules:

\[\frac{}{\text{ZERO} \in \text{Nat}}, \frac{n \in \text{Nat}}{\text{SUCC}~n \in \text{Nat}}, \frac{n \in \mathrm{Nat}, t \sim_{\mathrm{s}} n}{t \in \mathrm{Nat}}.\]

In other words, we choose the least fixed point of the following monotone operator on \(\mathcal{T}_{\mathrm{s}}\):

\[F_{\text{Nat}}(N) = [\text{ZERO}] \cup [\text{SUCC}~n \mid n \in N]\]

where

\[[\text{SUCC}~n \mid n \in N] = \{t \in \Lambda(\emptyset) \mid \exists n \in N(\text{SUCC}~n \sim_{\mathrm{s}} t)\}.\]

The type \(\text{Nat}\) is thus:

\[\text{Nat} = \mu F_{\text{Nat}}.\]

Coinductive Types

We can also define coinductive data types.

If we take the production rules for the natural number, yet employ the greatest fixed point instead, we define the type of conatural numbers (or extended natural numbers):

\[\text{Conat} = \nu F_{\text{Nat}}.\]

This type contains a special additional term:

\[\text{INF} \equiv \text{FIX} ~ (\lambda r . \text{SUCC} ~ r).\]

This implies that

\[\text{INF} \sim_{\mathrm{s}} \text{SUCC INF}.\]

We may think of this as an "infinite" number. To prove that \(\text{INF} \in \text{Conat}\), we may employ the coinductive proof principle, i.e., we must show that the set

\[X = \{\text{INF}\}\]

is a post-fixed point of \(F_{\text{Nat}}\), i.e., that \(X \subseteq F_{\text{Nat}}(X)\). In this case, since \(\text{Conat}\) is the greatest post-fixed point, it will follow that \(X \subseteq \text{Conat}\) and hence \(\text{INF} \in \text{Conat}\). But \(F_{\text{Nat}}(X) = [\text{ZERO}] \cup [\text{SUCC INF}]\), so this is indeed the case since \(\text{SUCC INF} \sim_{\mathrm{s}} \text{INF}\).

Additional Types

In this section, we will define a few common data types.

Options

In a functional programming language, we might define an option type as follows:

data Option A = None | Some A

The encoding is as follows:

\[\text{NONE} \equiv \lambda n . \lambda s . n,\]

\[\text{SOME} \equiv \lambda a . \lambda n . \lambda s . s a.\]

The inductive type \(\text{Option}_A\) of options with elements of type \(A\) is defined by the following production rules:

\[\frac{}{\text{NONE} \in \text{Option}_A}, \frac{a \in A}{\text{SOME} \in \text{Option}_A}, \frac{t \in \text{Option}_A, t \sim_{\mathrm{s}} t'}{t' \in \text{Option}_A}.\]

Thus, it is the least fixed point of the monotone map \(F_{\text{Option}, A}\) defined as

\[F_{\text{Option}, A}(O) = [\text{NONE}] \cup [\text{SOME}~a \mid a \in A],\]

that is, \(\text{Option}_A = \mu F_{\text{Option}, A}\).

Lists

In a functional programming language, we might define a list type as follows:

data List A = Empty | Cons A (List A)

The encoding is as follows:

\[\text{EMPTY} \equiv \lambda e . \lambda c . e,\]

\[\text{CONS} \equiv \lambda h . \lambda t . \lambda e . \lambda c . c h t.\]

The inductive type \(\text{List}_A\) of homogeneous lists with elements of type \(A\) is defined by the following production rules:

\[\frac{}{\text{EMPTY} \in \text{List}_A}, \frac{h \in A, t \in \text{List}_A}{\text{CONS} ~ h ~ t \in \text{List}_A}, \frac{l \in \text{List}_A, l' \sim_{\mathrm{s}} l}{l' \in \text{List}}.\]

Thus, it is the least fixed point of the monotone map \(F_{\text{List}, A}\) defined as

\[F_{\text{List}, A}(L) = [\text{EMPTY}] \cup [\text{CONS} ~ h ~ t \mid h \in A, t \in L],\]

that is, \(\text{List}_A = \mu F_{\text{List}, A}\).

The inductive type \(\text{List}\) of heterogeneous lists is defined by the following production rules:

\[\frac{}{\text{EMPTY} \in \text{List}}, \frac{h \in \Lambda(\emptyset), t \in \text{List}}{\text{CONS} ~ h ~ t \in \text{List}}, \frac{l \in \text{List}, l' \sim_{\mathrm{s}} l}{l' \in \text{List}}.\]

Thus, it is the least fixed point of the monotone map \(F_{\text{List}, A}\) defined as

\[F_{\text{List}}(L) = [\text{EMPTY}] \cup [\text{CONS} ~ h ~ t \mid h \in \Lambda(\emptyset), t \in L],\]

that is, \(\text{List} = \mu F_{\text{List}}\).

Streams

The coinductive counterpart of lists are often called streams.

In a programming language with lazy evaluation, we might write the following:

natAdd Zero n = n
natAdd (Succ m) n = Succ (natAdd m n)

fib Zero = Zero
fib (Succ Zero) = Succ Zero
fib (Succ (Succ n)) = natAdd (fib (Succ n)) (fib n)

fibs n = Cons (fib n) (fibs (Succ n))

The expression fibs n produces a stream (i.e., infinite list) representing a suffix of the Fibonacci sequence starting at the n-th index (so fibs 0 represents the entire sequence).

We encode this as follows:

\[\text{NAT-ADD} \equiv \text{FIX} (\lambda r . \lambda m . \lambda n . m n (\lambda m' . \text{SUCC} (r m' n))),\]

\[\text{FIB} \equiv \text{FIX} (\lambda r . \lambda n . n ~\text{ZERO} ~(\lambda n' . n' (\text{SUCC} ~n') (\lambda n'' . \text{NAT-ADD} ~(r n') ~r n'')),\]

\[\text{FIBS} \equiv \text{FIX}(\lambda r . \lambda n . \text{CONS} ~(\text{FIB}~n) (r ~(\text{SUCC}~n))).\]

The type of streams of elements of type \(A\) (i.e. finite and infinite lists of elements of type \(A\)) is the greatest fixed point \(\text{Stream}_A = \nu F_{\text{List},A}\).

To prove that \(\text{FIBS}~n \in \text{Stream}_A\) for all \(n \in \text{Nat}\), we must exhibit a set \(X\) such that \(X \subseteq F_{\text{List},A}(X)\) and \(\text{FIBS}~n \in X\). We chose the following set:

\[X = \{\text{FIBS}~n \mid n \in \text{Nat}\}.\]

Note that, according to the fundamental property of \(\text{FIX}\) and the definition of \(\sim_{\mathrm{s}}\),

\[\text{FIBS} ~n \sim_{\mathrm{s}} \text{CONS} ~(\text{FIB}~n) (\text{FIBS} ~(\text{SUCC}~n)).\]

Since \(\text{FIB}~n \in \text{Nat}\) and \(\text{FIBS} ~(\text{SUCC}~n) \in X\), it follows that \(\text{CONS} ~(\text{FIB}~n) (\text{FIBS} ~(\text{SUCC}~n)) \in F_{\text{List},\text{Nat}}(X)\), and since \(\text{FIBS} ~n \sim_{\mathrm{s}} \text{CONS} ~(\text{FIB}~n) (\text{FIBS} ~(\text{SUCC}~n))\), it follows that \(\text{FIBS} ~n \in F_{\text{List},\text{Nat}}(X)\). Thus, \(X \subseteq F_{\text{List},\text{Nat}}(X)\), and so \(X \subseteq \nu F_{\text{List},\text{Nat}}\) and \(\text{FIBS} ~n \in \nu F_{\text{List},\text{Nat}}\).

Trees

In a functional programming language, we might define a data type of binary trees as follows:

data Tree A = Leaf | Node (Tree A) A (Tree A)

This is encoded as follows:

\[\text{LEAF} \equiv \lambda l . \lambda n . l,\]

\[\text{NODE} \equiv \lambda t . \lambda a . \lambda t' . \lambda l . \lambda n . n t a t'.\]

The production rules for the inductive type of binary trees with node labels of type \(A\) are as follows:

\[\frac{}{\text{LEAF} \in \text{Tree}_A}, \frac{t \in \text{Tree}_A, a \in A, t' \in \text{Tree}_A}{\text{NODE}~ t ~ a ~t' \in \text{Tree}_A}, \frac{t \in \text{Tree}_A, t' \sim_{\mathrm{s}} t'}{t' \in \text{Tree}_A}.\]

The type is the least fixed point of the following monotone map:

\[F_{\text{Tree},A}(T) = [\text{LEAF}] \cup [\text{NODE}~ t ~ a ~t' \mid t \in T, a \in A, t' \in T],\]

that is, \(\text{Tree} = \mu F_{\text{Tree},A}\).

Integers

In a functional programming language, we might define a data type of integers as follows:

data Int = IntZero | IntSucc Nat | IntPred Nat

Here, IntZero is chosen to be distinct from Zero (from Nat) and IntSucc represents the successor of a natural number and IntPred represents the predecessor of a natural number (and hence introduces negative numbers). There are other ways to represent this data type, but this representation has the advantage that every integer is uniquely expressed (there is only one way to express each integer).

The encoding is as follows:

\[\text{INT-ZERO} = \lambda z . \lambda s . \lambda p . z,\]

\[\text{INT-SUCC} = \lambda n . \lambda z . \lambda s . \lambda p . s n,\]

\[\text{INT-PRED} = \lambda n . \lambda z . \lambda s . \lambda p . p n.\]

The production rules for the inductive type of integers are as follows:

\[\frac{}{\text{INT-ZERO} \in \text{Int}}, \frac{n \in \text{Nat}}{\text{INT-SUCC}~n \in \text{Int}}, \frac{n \in \text{Nat}}{\text{INT-PRED}~n \in \text{Nat}}, \frac{i \in \text{Int}, i \sim_{\mathrm{s}} i'}{i' \in \text{Int}}.\]

Thus, the type is the least fixed point of the following monotone map:

\[F_{\text{Int}}(I) = [\text{INT-ZERO}] \cup [\text{INT-SUCC}~n \mid n \in \text{Nat}] \cup [\text{INT-PRED}~n \mid n \in \text{Nat}],\]

that is, \(\text{Int} = \mu F_{\text{Int}}\).

Rational Numbers

In a functional programming language, we might define a data type of rational numbers as follows:

data Rat = Frac Int Nat

Here, Frac represents a fraction whose numerator is signed and whose denominator is shifted by \(1\) (so that \(0\) never occurs in the denominator and every constructed element is well-defined), i.e., Frac n d represents \(\frac{n}{d+1}\).

The encoding is as follows:

\[\text{FRAC} = \lambda n . \lambda d . \lambda f . f n d.\]

The production rules for the inductive type of rational numbers are as follows:

\[\frac{n \in \text{Int}, d \in \text{Nat}}{\text{Frac}~n~d \in \text{Rat}}, \frac{r \in \text{Rat}, r \sim_{\mathrm{s}} r'}{r' \in \text{Rat}}.\]

Thus, the type is the least fixed point of the following monotone map:

\[F_{\text{Rat}} = [\text{FRAC}~n~d \mid n \in \text{Int}, d \in \text{Nat}],\]

that is, \(\text{Rat} = \mu F_{\text{Rat}}\).

Tree Sort

As an example, we will implement the tree sort algorithm.

insert le a Leaf = Node Leaf a Leaf
insert le a (Node l a' r) = if le a a' 
                         then Node (insert le a l) a' r
                         else Node l a' (insert le a r)

concat Empty r = r
concat l Empty = l
concat (Cons a l) r = Cons a (concat l r)

flatten Leaf = Empty
flatten Node l a r = concat (flatten l) (concat (singleton a) (flatten r))

singleton a = Cons a Empty

fold f x Empty = x
fold f x (Cons a l) = f a (fold f x l) 

sort le l = flatten (fold (insert le) Leaf l)

leNat Zero n = True
leNat (Succ m) Zero = False
leNat (Succ m) (Succ n) = leNat m n

We define a conditional ("if-then-else") construct as follows:

\[\text{COND} \equiv \lambda b . \lambda t . \lambda f . b t f.\]

We define a comparison operator for the natural numbers as follows:

\[\text{LE-NAT} \equiv \text{FIX}(\lambda r . \lambda m .\lambda n . m ~ \text{TRUE} ~ (\lambda m' . n ~ \text{FALSE} ~ (\lambda n' . r m' n'))).\]

We define a right-fold operation on lists as follows:

\[\text{FOLD} \equiv \text{FIX}(\lambda r . \lambda f . \lambda x . \lambda l . l ~ x ~ (\lambda a l' . f a (r f x l'))).\]

We define a singleton list helper function as follows:

\[\text{SINGLETON} \equiv (\lambda a . \text{CONS} ~ a ~ \text{EMPTY}).\]

We define a list concatenation function as follows:

\[\text{CONCAT} \equiv \text{FIX} (\lambda r . \lambda x . \lambda y . x y (\lambda a x' . y x (\lambda b y' . \text{CONS}~ a (r x' y) ))).\]

We define the flatten operation as follows:

\[\text{FLATTEN} \equiv \text{FIX}(\lambda r . \lambda t . t ~ \text{EMPTY} ~ (\lambda x . \lambda a . \lambda y . \text{CONCAT} ~ (r x) (\text{CONCAT} ~ (\text{SINGLETON}~a) (r y)))).\]

We define the insert operation as follows:

\[\text{INSERT} \equiv \text{FIX}(\lambda r . \lambda c . \lambda a . \lambda t . t~(\text{NODE} ~\text{LEAF} ~ a ~ \text{LEAF}) ~ (\lambda x . \lambda a' . \lambda y . \text{COND} ~ (c a a') ~ (\text{NODE} ~ (r c a x) ~ a' ~ y) ~ (\text{NODE} ~ x ~ a' ~ (r c a y)))).\]

Finally, we define the sort operation as follows:

\[\text{SORT} \equiv (\lambda c . \lambda l . \text{FLATTEN}~(\text{FOLD} ~ (\text{INSERT} ~ c) ~ \text{LEAF} ~ l)).\]

We may then sort a list of natural numbers \(l\) as follows:

\[\text{SORT}~\text{LE-NAT} ~ l.\]