Lambda Definability

Source file content/lambda-calculus/lambda-definability/lambda-definability.tex

Source file content/lambda-calculus/lambda-definability/introduction.tex

Introduction

At first glance, the lambda calculus is just a very abstract calculus of expressions that represent functions and applications of them to others. Nothing in the syntax of the lambda calculus suggests that these are functions of particular kinds of objects, in particular, the syntax includes no mention of natural numbers. Its basic operations---application and lambda abstractions---are operations that apply to any function, not just functions on natural numbers.

Nevertheless, with some ingenuity, it is possible to define arithmetical functions, i.e., functions on the natural numbers, in the lambda calculus. To do this, we define, for each natural number $n \in \Nat$source, a special $\lambd$source-term $\num n$source, the Church numeral for $n$source. (Church numerals are named for Alonzo Church.)

The Church numeral $\num n$source is encoded as a lambda term which represents a function accepting two arguments $f$source and $x$source, and returns $f^n(x)$source. Church numerals are evidently in normal form.

A representation of natural numbers in the lambda calculus is only useful, of course, if we can compute with them. Computing with Church numerals in the lambda calculus means applying a $\lambd$source-term $F$source to such a Church numeral, and reducing the combined term $F\, \num n$source to a normal form. If it always reduces to a normal form, and the normal form is always a Church numeral $\num m$source, we can think of the output of the computation as being the number $m$source. We can then think of $F$source as defining a function $f\colon \Nat \to \Nat$source, namely the function such that $f(n) = m$source iff $F\, \num n \red \num m$source. Because of the Church--Rosser property, normal forms are unique if they exist. So if $F\, \num n \red \num m$source, there can be no other term in normal form, in particular no other Church numeral, that $F \, \num n$source reduces to.

Conversely, given a function $f\colon \Nat \to \Nat$source, we can ask if there is a term $F$source that defines $f$source in this way. In that case we say that $F$source lambda-defines $f$source, and that $f$source is lambda-definable. We can generalize this to many-place and partial functions.

A very simple example are the constant functions. The term $C_k \ident \lambd[x][\num{k}]$source lambda-defines the function $c_k\colon \Nat \to \Nat$source such that $c(n) = k$source. For $C_k \, \num n \ident (\lambd[x][\num{k}])\num n \redone \num{k}$source for any $n$source. The identity function is lambda-defined by $\lambd[x][x]$source. More complex functions are of course harder to define, and often require a lot of ingenuity. So it is perhaps surprising that every computable function is lambda-definable. The converse is also true: if a function is lambda-definable, it is computable.

Source file content/lambda-calculus/lambda-definability/arithmetical-functions.tex

lambda definable Arithmetical Functions

The definition of exponentiation as a $\lambd$source-term is surprisingly simple:

The first argument $b$source is the base and the second $e$source is the exponent. Intuitively, $e f$source is $f^e$source by our encoding of numbers. If you find it hard to understand, we can still define exponentiation also by iterated multiplication:

Predecessor and subtraction on Church numeral is not as simple as we might think: it requires encoding of pairs.

Source file content/lambda-calculus/lambda-definability/pairs.tex

Pairs and Predecessor

Intuitively it is a function that accepts a function, and applies that function to the two elements of the pair. Following this idea we have this constructor, which takes two terms and returns the pair containing them:

Given a pair, we also want to recover its elements. For this we need two access functions, which accept a pair as argument and return the first or second elements in it:

Now with pairs we can lambda-define the predecessor function:

Remember that $\num n\, f x$source reduces to $f^{n}(x)$source; in this case $f$source is a function that accepts a pair $p$source and returns a new pair containing the second component of $p$source and the successor of the second component; $x$source is the pair $\tuple{0,0}$source. Thus, the result is $\tuple{0,0}$source for $n=0$source, and $\tuple{\num{n-1}, \num n}$source otherwise. $\fn{Pred}$source then returns the first component of the result.

Subtraction can be defined as $\fn{Pred}$source applied to $a$source, $b$source times:

Source file content/lambda-calculus/lambda-definability/truth-values.tex

Truth Values and Relations

We can encode truth values in the pure lambda calculus as follows:

Truth values are represented as selectors, i.e., functions that accept two arguments and returning one of them. The truth value $\fn{true}$source selects its first argument, and $\fn{false}$source its second. For example, $\fn{true}\, M N$source always reduces to $M$source, while $\fn{false}\, M N$source always reduces to $N$source.

For instance, the relation $\fn{IsZero} = \{0\}$source which holds of $0$source and $0$source only, is lambda-definable by

How does it work? Since Church numerals are defined as iterators (functions which apply their first argument $n$source times to the second), we set the initial value to be $\fn{true}$source, and for every step of iteration, we return $\fn{false}$source regardless of the result of the last iteration. This step will be applied to the initial value $n$source times, and the result will be $\fn{true}$source if and only if the step is not applied at all, i.e., when $n = 0$source.

On the basis of this representation of truth values, we can further define some truth functions. Here are two, the representations of negation and conjunction:

The function “$\fn{Not}$source” accepts one argument, and returns $\fn{true}$source if the argument is $\fn{false}$source, and $\fn{false}$source if the argument is $\fn{true}$source. The function “$\fn{And}$source” accepts two truth values as arguments, and should return $\fn{true}$source iff both arguments are $\fn{true}$source. Truth values are represented as selectors (described above), so when $x$source is a truth value and is applied to two arguments, the result will be the first argument if $x$source is $\fn{true}$source and the second argument otherwise. Now $\fn{And}$source takes its two arguments $x$source and $y$source, and in return passes $y$source and $\fn{false}$source to its first argument $x$source. Assuming $x$source is a truth value, the result will evaluate to $y$source if $x$source is $\fn{true}$source, and to $\fn{false}$source if $x$source is $\fn{false}$source, which is just what is desired.

Note that we assume here that only truth values are used as arguments to $\fn{And}$source. If it is passed other terms, the result (i.e., the normal form, if it exists) may well not be a truth value.

Source file content/lambda-calculus/lambda-definability/primitive-recursive-functions.tex

Primitive Recursive Functions are lambda definable

Recall that the primitive recursive functions are those that can be defined from the basic functions $\Zero$source, $\Succ$source, and $\Proj{n}{i}$source by composition and primitive recursion.

Note that the lemma on closure under composition did not require that $f$source and $g_0$source, dots, $g_{k-1}$source are primitive recursive; it is only required that they are total and lambda-definable.

Source file content/lambda-calculus/lambda-definability/fixpoints.tex

Fixpoints

Suppose we wanted to define the factorial function by recursion as a term $\fn{Fac}$source with the following property:

That is, the factorial of $n$source is $1$source if $n = 0$source, and $n$source times the factorial of $n-1$source otherwise. Of course, we cannot define the term $\fn{Fac}$source this way since $\fn{Fac}$source itself occurs in the right-hand side. Such recursive definitions involving self-reference are not part of the lambda calculus. Defining a term, e.g., by

only involves previously defined terms in the right-hand side, such as $\fn{Add}$source. We can always remove $\fn{Add}$source by replacing it with its defining term. This would give the term $\fn{Mult}$source as a pure lambda term; if $\fn{Add}$source itself involved defined terms (as, e.g., $\fn{Add}'$source does), we could continue this process and finally arrive at a pure lambda term.

However this is not true in the case of recursive definitions like the one of $\fn{Fac}$source above. If we replace the occurrence of $\fn{Fac}$source on the right-hand side with the definition of $\fn{Fac}$source itself, we get:

and we still haven't gotten rid of $\fn{Fac}$source on the right-hand side. Clearly, if we repeat this process, the definition keeps growing longer and the process never results in a pure lambda term. Thus this way of defining factorial (or more generally recursive functions) is not feasible.

The recursive definition does tell us something, though: If $f$source were a term representing the factorial function, then the term

applied to the term $f$source, i.e., $\fn{Fac}'\,f$source, also represents the factorial function. That is, if we regard $\fn{Fac}'$source as a function accepting a function and returning a function, the value of $\fn{Fac'}\, f$source is just $f$source, provided $f$source is the factorial. A function $f$source with the property that $\fn{Fac}' \, f \equal[\beta] f$source is called a fixpoint of $\fn{Fac}'$source. So, the factorial is a fixpoint of $\fn{Fac}'$source.

There are terms in the lambda calculus that compute the fixpoints of a given term, and these terms can then be used to turn a term like $\fn{Fac}'$source into the definition of the factorial.

Of course, since $Yg$source is a redex, the reduction can continue indefinitely:

So we can think of $Yg$source as $g$source applied to itself infinitely many times. If we apply $g$source to it one additional time, we---so to speak---aren't doing anything extra; $g$source applied to $g$source applied infinitely many times to $Yg$source is still $g$source applied to $Yg$source infinitely many times.

Note that the above sequence of $\beta$source-reduction steps starting with $Yg$source is infinite. So if we apply $Yg$source to some term, i.e., consider $(Yg)N$source, that term will also reduce to infinitely many different terms, namely $(g(Yg))N$source, $(g(g(Yg)))N$source, dots. It is nevertheless possible that some other sequence of reduction steps does terminate in a normal form.

Take the factorial for instance. Define $\fn{Fac}$source as $Y\, \fn{Fac}'$source (i.e., a fixpoint of $\fn{Fac'}$source). Then:

What goes for $\fn{Fac'}$source goes for any recursive definition. Suppose we have a recursive equation

The $Y$source combinator of the definition of Turing's fixpoint combinator is due to Alan Turing. Alonzo Church had proposed a different version which we'll call $Y_C$source:

Church's combinator is a bit weaker than Turing's in that $Yg \equal[\beta] g(Yg)$source but not $Yg \bred g(Yg)$source. Let $V$source be the term $\lambd[x][g(xx)]$source, so that $Y_C \ident \lambd[g][VV]$source. Then

In other words, $Y_Cg$source and $g(Y_Cg)$source reduce to a common term $g(VV)$source; so $Y_Cg \equal[\beta] g(Y_Cg)$source. This is often enough for applications.

Source file content/lambda-calculus/lambda-definability/minimization.tex

Minimization

The general recursive functions are those that can be obtained from the basic functions $\Zero$source, $\Succ$source, $\Proj{n}{i}$source by composition, primitive recursion, and regular minimization. To show that all general recursive functions are lambda-definable we have to show that any function defined by regular minimization from a lambda definable function is itself lambda-definable.

Source file content/lambda-calculus/lambda-definability/partial-recursive-functions.tex

Partial Recursive Functions are lambda definable

Partial recursive functions are those obtained from the basic functions by composition, primitive recursion, and unbounded minimization. They differ from general recursive function in that the functions used in unbounded search are not required to be regular. Not requiring regularity means that functions defined by minimization may sometimes not be defined.

At first glance it might seem that the same methods used to show that the (total) general recursive functions are all lambda-definable can be used to prove that all partial recursive functions are lambda-definable. For instance, the composition of $f$source with $g$source is lambda-defined by $\lambd[x][F (G x)]$source if $f$source and $g$source are lambda-defined by terms $F$source and $G$source, respectively. However, when the functions are partial, this is problematic. When $g(x)$source is undefined, meaning $G x$source has no normal form. In most cases this means that $F (G x)$source has no normal forms either, which is what we want. But consider when $F$source is $\lambd[x][\lambd[y][y]]$source, in which case $F (G x)$source does have a normal form ($\lambd[y][y]$source).