Lambda calculus

Lambda Definability

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

% Part: lambda-calculus% Chapter: lambda-definability\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{lam}{rep}{Lambda Definability}\begin{editorial}  This chapter is experimental. It needs more explanation, and the  material should be structured better into definitions and  propositions with proofs, and more examples.\end{editorial}\olimport{introduction}\olimport{arithmetical-functions}\olimport{pairs}\olimport{truth-values}%\olimport{lists}\olimport{primitive-recursive-functions}\olimport{fixpoints}\olimport{minimization}\olimport{partial-recursive-functions}\olimport{lambda-definable-recursive}\OLEndChapterHook\end{document}

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

% Part: lambda-calculus% Chapter: lambda-definability% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{ldf}{int}\olsection{Introduction}At first glance, the lambda calculus is just a very abstract calculusof expressions that represent functions and applications of them toothers. Nothing in the syntax of the lambda calculus suggests thatthese are functions of particular kinds of objects, in particular, thesyntax includes no mention of natural numbers. Its basicoperations---application and lambda abstractions---are operations thatapply to any function, not just functions on naturalnumbers.Nevertheless, with some ingenuity, it is possible to definearithmetical functions, i.e., functions on the natural numbers, in thelambda calculus. To do this, we define, for each natural number~$n \in\Nat$, a special $\lambd$-term~$\num n$, the \emph{Church numeral}for~$n$. (Church numerals are named for Alonzo Church.)\begin{defn}  If $n \in \Nat$, the corresponding \emph{Church numeral} $\num{n}$  represents~$n$:  \[    \num{n} \ident \lambd[fx][f^n(x)]  \]  Here, $f^n(x)$ stands for the result of applying $f$ to~$x$ $n$  times. For example, $\num{0}$ is $\lambd[fx][x]$, and $\num{3}$ is  $\lambd[fx][f(f(f\,x))]$.\end{defn}  The Church numeral $\num n$ is encoded as a lambda term whichrepresents a function accepting two arguments $f$ and $x$, andreturns $f^n(x)$. Church numerals are evidently in normal form.A representation of natural numbers in the lambda calculus is onlyuseful, of course, if we can compute with them.  Computing with Churchnumerals in the lambda calculus means applying a $\lambd$-term~$F$ tosuch a Church numeral, and reducing the combined term~$F\, \num n$ toa normal form. If it always reduces to a normal form, and the normalform is always a Church numeral~$\num m$, we can think of the outputof the computation as being the number~$m$. We can then think of~$F$as defining a function $f\colon \Nat \to \Nat$, namely the functionsuch that $f(n) = m$ iff $F\, \num n \red \num m$. Because of theChurch--Rosser property, normal forms are unique if they exist. So if$F\, \num n \red \num m$, there can be no other term in normal form,in particular no other Church numeral, that $F \, \num n$ reduces to.Conversely, given a function $f\colon \Nat \to \Nat$,we can ask if there is a term $F$ that defines~$f$ in this way. Inthat case we say that $F$ \emph{!!{lambda define}s}~$f$, and that $f$ is!!{lambda definable}. We can generalize this to many-place and partialfunctions.\begin{defn}Suppose $f\colon \Nat^k \to \Nat$. We say that a lambda term~$F$\emph{!!{lambda define}s} $f$ if for all $n_0$, \dots,~$n_{k-1}$,\[F \, \num{n_0} \, \num{n_1} \dots \num{n_{k-1}} \red \num{f(n_0, n_1, \dots,  n_{k-1})}\]if $f(n_0, \dots, n_{k-1})$ is defined, and $F \, \num{n_0} \,\num{n_1} \dots \num{n_{k-1}}$ has no normal form otherwise.\end{defn}A very simple example are the constant functions. The term $C_k \ident\lambd[x][\num{k}]$ !!{lambda define}s the function $c_k\colon \Nat \to\Nat$ such that $c(n) = k$. For $C_k \, \num n \ident(\lambd[x][\num{k}])\num n \redone \num{k}$ for any~$n$. The identityfunction is !!{lambda defined} by $\lambd[x][x]$. More complexfunctions are of course harder to define, and often require a lot ofingenuity. So it is perhaps surprising that every computable functionis !!{lambda definable}. The converse is also true: if a function is!!{lambda definable}, it is computable.\end{document}

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

% Part: lambda-calculus% Chapter: lambda-definablity% Section: arithmetical-functions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{rep}{arf}\olsection{\usetoken{S}{lambda definable} Arithmetical Functions}\begin{prop}  \ollabel{prop:succ-ld}  The successor function~$\Succ$ is !!{lambda definable}.\end{prop}\begin{proof}A term that !!{lambda define}s the successor function is\begin{align*}  \fn{Succ} & \ident \lambd[a][\lambd[fx][f ({a} f x)]].  \intertext{Given our conventions, this is short for}  \fn{Succ} & \ident \lambd[a][\lambd[f][\lambd[x][(f (({a} f) x))]]].  \intertext{$\fn{Succ}$ is a function that accepts as argument a    number~$a$, and evaluates to another function, $\lambd[fx][f ({a}      f x)]$. That function is not itself a Church numeral. However,    if the argument $a$ is a Church numeral, it reduces to one. Consider:}   (\lambd[a][\lambd[fx][f ({a} f x)]])\,\num{n} & \redone   \lambd[fx][f ({\num{n}} f x)].   \intertext{The embedded term $\num{n}fx$ is a redex, since     $\num{n}$ is $\lambd[fx][f^nx]$. So $\num{n}fx \redone f^nx$ and     so, for the entire term we have}   \fn{Succ}\, \num n & \red \lambd[fx][f(f^n(x))],\end{align*}i.e., $\num{n+1}$.\end{proof}\begin{ex}  Let's look at what happens when we apply $\fn{Succ}$ to~$\num{0}$,  i.e., $\lambd[fx][x]$. We'll spell the terms out in full:  \begin{align*}    \fn{Succ}\, \num{0} & \ident (\lambd[a][\lambd[f][\lambd[x][(f (({a} f) x))]]])(\lambd[f][\lambd[x][x]])\\    & \redone \lambd[f][\lambd[x][(f (({(\lambd[f][\lambd[x][x]])} f) x))]] \\    & \redone \lambd[f][\lambd[x][(f ({(\lambd[x][x])} x))]] \\    & \redone \lambd[f][\lambd[x][(f x)]] \ident \num{1}\\  \end{align*}\end{ex}\begin{prob}  The term   \begin{align*}    \fn{Succ}' & \ident \lambd[{n}][\lambd[fx][{n} f (f x)]]  \end{align*}  !!{lambda define}s the successor function. Explain why.\end{prob}\begin{prop}  \ollabel{prop:add-ld}  The addition function~$\Add$ is !!{lambda definable}.\end{prop}\begin{proof}Addition is !!{lambda define}d by the terms  \begin{align*}  \fn{Add} & \ident \lambd[{a}{b}][\lambd[fx][{a} f ({b} f x)]]\intertext{or, alternatively,}  \fn{Add}' & \ident \lambd[{a}{b}][{a}\, \fn{Succ} \, {b}].\intertext{The first addition works as follows: $\fn{Add}$ first  accept two numbers ${a}$ and ${b}$. The result is a function that  accepts $f$ and $x$ and returns $af(bfx)$. If $a$ and $b$ are Church  numerals $\num{n}$ and $\num{m}$, this reduces to $f^{n+m}(x)$,  which is identical to $f^{n}(f^{m}(x))$. Or, slowly:}  (\lambd[{a}{b}][\lambd[fx][{a} f ({b} f x)]])\num n\,\num m & \redone  \lambd[fx][\num{n}\, f (\num {m}\, f x)] \\  & \redone \lambd[fx][\num{n}\, f (f^m x)] \\  & \redone \lambd[fx][f^n (f^m x)] \ident \num {n+m}.\intertext{The second representation of addition $\fn{Add'}$ works  differently: Applied to two Church numerals $\num{n}$ and  $\num{m}$,}\fn{Add}' \num n \,\num m& \redone \num{n}\, \fn{Succ}\, \num{m}.\intertext{But $\num{n} f x$ always reduces to $f^n(x)$. So,}  \num{n}\,  \fn{Succ}\, \num{m} & \red \fn{Succ}^n(\num{m}).\end{align*}And since $\fn{Succ}$ !!{lambda define}s the successor function, and thesuccessor function applied $n$ times to~$m$ gives $n+m$, this in turnreduces to~$\num{n+m}$.\end{proof}\begin{prop}  \ollabel{prop:mult-ld}  Multiplication is !!{lambda definable} by the term  \[  \fn{Mult} \ident \lambd[ab][\lambd[fx][a (b f) x]]  \]\end{prop}\begin{proof}  To see how this works, suppose we apply $\fn{Mult}$ to Church numerals  $\num{n}$ and $\num{m}$: $\fn{Mult} \, \num{n} \, \num{m}$ reduces to  $\lambd[fx][\num{n}(\num{m}\, f)x]$.  The term $\num{m} f$ defines a  function which applies $f$ to its argument $m$ times. Consequently,  $\num{n} (\num{m} f) x$ applies the function ``apply $f$ $m$ times''  itself $n$ times to~$x$. In other words, we apply $f$ to $x$, $n\cdot  m$ times. But the resulting normal term is just the Church numeral  $\num{nm}$.\end{proof}\begin{editorial}We can actually simplify this term further by $\eta$-reduction:\[  \fn{Mult} \ident \lambd[ab][\lambd[f][a (b f)]].\]But then we first have to explain $\eta$-reduction.\end{editorial}\begin{prob}Multiplication can be !!{lambda define}d by the term\[  \fn{Mult}' \ident \lambd[ab][a (\fn{Add}\, a) \num{0}].\]Explain why this works.\end{prob}The definition of exponentiation as a $\lambd$-term issurprisingly simple:\[  \fn{Exp} \ident \lambd[be][e b].\]The first argument $b$ is the base and the second~$e$ is the exponent.Intuitively, $e f$ is $f^e$ by our encoding of numbers. If you find ithard to understand, we can still define exponentiation also byiterated multiplication:\[  \fn{Exp}' \ident \lambd[be][e (\fn{Mult}\, b) \num{1}].\]Predecessor and subtraction on Church numeral is not as simple as wemight think: it requires encoding of pairs.\end{document}

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

% Part: lambda-calculus% Chapter: lambda-definability% Section: pairs\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{ldf}{pai}\olsection{Pairs and Predecessor}\begin{defn}The pair of $M$ and $N$ (written $\tuple{M,N}$) is defined as follows:\[\tuple{M,N} \ident \lambd[f][fMN].\]\end{defn}  Intuitively it is a function that accepts a function, and applies thatfunction to the two elements of the pair. Following this idea we havethis constructor, which takes two terms and returns the pair containingthem:\[  \fn{Pair} \ident \lambd[mn][\lambd[f][fmn]]\]Given a pair, we also want to recover its elements.For this we need two access functions, which accept a pair as argument andreturn the first or second elements in it:\begin{align*}  \fn{Fst} & \ident \lambd[p][p(\lambd[mn][m])]\\  \fn{Snd} & \ident \lambd[p][p(\lambd[mn][n])]\end{align*}\begin{prob}  Explain why the access functions $\fn{Fst}$ and $\fn{Snd}$ work.\end{prob}Now with pairs we can !!{lambda define} the predecessor function:\[  \fn{Pred} \ident \lambd[n][\fn{Fst}(n (\lambd[p][\tuple{\fn{Snd}\, {p}, \fn{Succ}(\fn{Snd}\, {p})}]) \tuple{\num 0, \num 0})]\]Remember that $\num n\, f x$ reduces to $f^{n}(x)$; in thiscase $f$ is a function that accepts a pair $p$ and returns a newpair containing the second component of $p$ and the successor of thesecond component; $x$ is the pair $\tuple{0,0}$. Thus, theresult is $\tuple{0,0}$ for $n=0$, and $\tuple{\num{n-1}, \num n}$otherwise. $\fn{Pred}$ then returns the first component of the result.Subtraction can be defined as $\fn{Pred}$ applied to $a$, $b$ times:\[\fn{Sub} \ident \lambd[ab][b \fn{Pred}\, a].\]    \end{document}

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

% Part: lambda-calculus% Chapter: lambda-definability% Section: truth-values\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{ldf}{tvr}\olsection{Truth Values and Relations}We can encode truth values in the pure lambda calculus as follows:\begin{align*}  \fn{true} & \ident \lambd[x][\lambd[y][x]]\\  \fn{false} & \ident \lambd[x][\lambd[y][y]]\end{align*}Truth values are represented as \emph{selectors}, i.e., functions thataccept two arguments and returning one of them. The truth value$\fn{true}$ selects its first argument, and $\fn{false}$ itssecond. For example, $\fn{true}\, M N$ always reduces to $M$, while$\fn{false}\, M N$ always reduces to~$N$.\begin{defn}We call a relation $R \subseteq \Nat^n$ !!{lambda definable} if there isa term~$R$ such that\begin{align*}  R\, \num{n_1} \dots \num{n_k} & \bred \fn{true}  \intertext{whenever $R(n_1, \dots, n_k)$ and}  R\, \num{n_1} \dots \num{n_k} & \bred \fn{false}\end{align*}otherwise.\end{defn}For instance, the relation $\fn{IsZero} = \{0\}$ which holds of $0$and $0$ only, is !!{lambda definable} by\[  \fn{IsZero} \ident \lambd[n][n (\lambd[x][\fn{false}])\, \fn{true}].\]How does it work? Since Church numerals are defined as iterators(functions which apply their first argument $n$~times to the second),we set the initial value to be $\fn{true}$, and for every step ofiteration, we return $\fn{false}$ regardless of the result of the lastiteration.  This step will be applied to the initial value $n$times, and the result will be $\fn{true}$ if and only if the step isnot applied at all, i.e., when $n = 0$.On the basis of this representation of truth values, we can furtherdefine some truth functions. Here are two, the representations ofnegation and conjunction:\begin{align*}  \fn{Not} & \ident \lambd[x][x\, \fn{false}\, \fn{true}]\\  \fn{And} & \ident \lambd[x][\lambd[y][xy \,\fn{false}]]\end{align*}The function ``$\fn{Not}$'' accepts one argument, and returns$\fn{true}$ if the argument is $\fn{false}$, and $\fn{false}$ if theargument is~$\fn{true}$.  The function ``$\fn{And}$'' accepts twotruth values as arguments, and should return $\fn{true}$ iff botharguments are~$\fn{true}$. Truth values are represented as selectors(described above), so when $x$ is a truth value and is applied to twoarguments, the result will be the first argument if $x$ is $\fn{true}$and the second argument otherwise. Now $\fn{And}$ takes its twoarguments $x$ and $y$, and in return passes $y$ and $\fn{false}$ toits first argument~$x$. Assuming $x$ is a truth value, the resultwill evaluate to~$y$ if $x$ is $\fn{true}$, and to $\fn{false}$ if $x$is $\fn{false}$, which is just what is desired.Note that we assume here that only truth values are used as argumentsto $\fn{And}$. If it is passed other terms, the result (i.e., thenormal form, if it exists) may well not be a truth value.\begin{prob}  Define the functions $\fn{Or}$ and $\fn{Xor}$ representing the truth  functions of inclusive and exclusive disjunction using the encoding  of truth values as $\lambd$-terms.\end{prob}\end{document}

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

% Part: lambda-calculus% Chapter: lambda-definability% Section: primitive-recursive-functions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{ldf}{prf}\olsection{Primitive Recursive Functions are \usetoken{S}{lambda definable}} Recall that the primitive recursive functions are those that can bedefined from the basic functions $\Zero$, $\Succ$, and $\Proj{n}{i}$by composition and primitive recursion.\begin{lem}  \ollabel{lem:basic}  The basic primitive recursive functions $\Zero$, $\Succ$, and  projections~$\Proj{n}{i}$ are !!{lambda definable}.\end{lem}\begin{proof}They are !!{lambda define}d by the following terms:\begin{align*}  \fn{Zero} & \ident \lambd[a][\lambd[fx][x]]\\  \fn{Succ} & \ident \lambd[a][\lambd[fx][f (a f x)]] \\  \fn{Proj}^n_i & \ident \lambd[x_0\dots x_{n-1}][x_i]\end{align*}\end{proof}\begin{lem}  \ollabel{lem:comp} Suppose the $k$-ary function $f$, and $n$-ary  functions $g_0, \dots, g_{k-1}$, are !!{lambda definable} by terms  $F$, $G_0$, \dots, $G_k$, and $h$ is defined from them by composition.  Then $H$ is !!{lambda definable}.\end{lem}\begin{proof}  $h$ can be !!{lambda define}d by the term  \[  H \ident \lambd[x_0 \dots x_{n-1}][F\, (G_0 x_0 \dots    x_{n-1}) \dots (G_{k-1} x_0 \dots x_{n-1})]  \]  We leave verification of this fact as an exercise.\end{proof}\begin{prob}  Complete the proof of \olref[lam][ldf][prf]{lem:comp} by showing  that $H\num{n_0}\dots\num{n_{n-1}} \red \num{h(n_0, \dots,    n_{n-1})}$.\end{prob}Note that \olref{lem:comp} did not require that $f$ and $g_0$,\dots,~$g_{k-1}$ are primitive recursive; it is only required thatthey are total and !!{lambda definable}.\begin{lem}\ollabel{lem:prim}  Suppose $f$ is an $n$-ary function and~$g$ is an $n+2$-ary function,  they are !!{lambda definable} by terms $F$ and~$G$, and the  function~$h$ is defined from $f$ and $g$ by primitive  recursion. Then $h$ is also !!{lambda definable}.\end{lem}\begin{proof}  Recall that $h$ is defined by  \begin{align*}    h(x_1, \dots, x_n, 0) &= f(x_1, \dots, x_n)\\    h(x_1, \dots, x_n, y+1) & = h(x_1, \dots, x_n, y, h(x_1, \dots, x_n, y)).  \end{align*}  Informally speaking, the primitive recursive definition iterates the  application of the function $h$ $y$ times and applies it to $f(x_1,  \dots, x_n)$. This is reminiscent of the definition of Church  numerals, which is also defined as a iterator.  For simplicity, we give the definition and proof for a single  additional argument~$x$. The function $h$ is !!{lambda define}d by:  \begin{align*}    H \ident & \lambd[x][\lambd[y][\fn{Snd} (y        D \tuple{\num{0}, F x})]]    \intertext{where }    D \ident & \lambd[p][\tuple{\fn{Succ} (\fn{Fst}\, p), (G x          (\fn{Fst}\, p) (\fn{Snd}\, p))}]  \end{align*}  The iteration state we maintain is a pair, the first of which is the  current $y$ and the second is the corresponding value of~$h$. For  every step of iteration we create a pair of new values of $y$ and  $h$; after the iteration is done we return the second part of the  pair and that's the final $h$ value. We now prove this is indeed a  representation of primitive recursion.  We want to prove that for any $n$ and $m$, $H\,\num{n}\,\num{m} \red  \num{h(n,m)}$. To do this we first show that if $D_n \ident  \Subst{D}{\num{n}}{x}$, then $D_n^m \tuple{\num{0}, F\, \num{n}} \red  \tuple{\num{m}, \num{h(n, m)}}$ We proceed by induction on~$m$.  If $m=0$, we want $D_n^0 \tuple{\num{0}, F\, \num{n}} \red  \tuple{\num{0}, \num{h(n, 0)}}$. But $D_n^0 \tuple{\num{0}, F\,    \num{n}}$ just is $\tuple{\num{0}, F\, \num{n}}$. Since $F$  !!{lambda define}s~$f$, this reduces to $\tuple{\num{0},    \num{f(n)}}$, and since $f(n) = h(n, 0)$, this is $\tuple{\num{0},    \num{h(n,0)}}$  Now suppose that $D_n^m \tuple{\num{0}, F\, \num{n}} \red  \tuple{\num{m}, \num{h(n, m)}}$. We want to  show that $D_n^{m+1} \tuple{\num{0}, F\, \num{n}} \red  \tuple{\num{m+1}, \num{h(n, m+1)}}$.  \begin{align*}    D_n^{m+1} \tuple{\num{0}, F\, \num{n}}    & \ident D_n(D_n^{m} \tuple{\num{0}, F\, \num{n}})\\    & \red D_n\,\tuple{\num{m}, \num{h(n, m)}} \text{\qquad (by IH)}\\    & \ident (\lambd[p][      \tuple{        \fn{Succ} (\fn{Fst}\, p), (G \, \num{n} (\fn{Fst}\, p) (\fn{Snd}\, p))    }]) \tuple{\num{m}, \num{h(n,m)}}\\    & \redone    \tuple{\fn{Succ} (\fn{Fst}\, \tuple{\num{m}, \num{h(n,m)}}),\\      & \qquad (G \, \num{n} (\fn{Fst}\, \tuple{\num{m}, \num{h(n,m)}}) (\fn{Snd}\, \tuple{\num{m}, \num{h(n,m)}}))}\\    & \red     \tuple{\fn{Succ}\, \num{m}, (G \, \num{n} \,\num{m} \, \num{h(n,m)})}\\    & \red \tuple{\num{m+1}, \num{g(n, m, h(n, m))}}  \end{align*}  Since $g(n, m, h(n, m)) = h(n, m+1)$, we are done.  Finally, consider  \begin{align*}    H\,\num n\,\num m &\ident \lambd[x][\lambd[y][\fn{Snd} (y        (\lambd[p].\tuple{\fn{Succ} (\fn{Fst}\, p), (G\, x\,          (\fn{Fst}\, p)\, (\fn{Snd}\, p))}) \tuple{\num{0}, F x})]]\\    & \qquad\,\num n\, \num m\\    & \red \fn{Snd} (\num m \,    \underbrace{(\lambd[p].\tuple{\fn{Succ} (\fn{Fst}\, p), (G \,\num n\,      (\fn{Fst}\, p) (\fn{Snd}\, p))})}_{D_n} \tuple{\num{0}, F \num n})\\    & \ident \fn{Snd} (\num m \, D_n\, \tuple{\num{0}, F \num n})\\    & \red \fn{Snd} \,(D_n^m  \tuple{\num{0}, F \num n})\\    & \red \fn{Snd} \,\tuple{\num{m}, \num{h(n, m)}} \\    & \red \num{h(n,m)}.   \end{align*}  \end{proof}\begin{prop}  Every primitive recursive function is !!{lambda definable}.\end{prop}\begin{proof}  By \olref{lem:basic}, all basic functions are !!{lambda definable},  and by \olref{lem:comp} and \olref{lem:prim}, the !!{lambda definable}  functions are closed under composition and primitive recursion.\end{proof}\end{document}

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

% Part: lambda-calculus% Chapter: lambda-definability% Section: fixpoints\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{ldf}{fp}\olsection{Fixpoints}Suppose we wanted to define the factorial function by recursion as aterm $\fn{Fac}$ with the following property:\[\fn{Fac} \ident \lambd[n][\fn{IsZero}\, n\, \num 1 (\fn{Mult}\, n (\fn{Fac}(\fn{Pred} \, n)))]\]That is, the factorial of $n$ is $1$ if $n = 0$, and $n$ times thefactorial of $n-1$ otherwise.  Of course, we cannot define the term$\fn{Fac}$ this way since $\fn{Fac}$ itself occurs in the right-handside. Such recursive definitions involving self-referenceare not part of the lambda calculus. Defining a term, e.g., by\[\fn{Mult} \ident \lambd[ab][a (\fn{Add}\, a) 0]\]only involves previously defined terms in the right-hand side, such as$\fn{Add}$. We can always remove $\fn{Add}$ by replacing it with itsdefining term.  This would give the term $\fn{Mult}$ as a pure lambdaterm; if $\fn{Add}$ itself involved defined terms (as, e.g.,$\fn{Add}'$ does), we could continue this process and finally arrive ata pure lambda term.However this is not true in the case of recursive definitions like theone of $\fn{Fac}$ above. If we replace the occurrence of $\fn{Fac}$ onthe right-hand side with the definition of $\fn{Fac}$ itself, we get:\begin{align*}  \fn{Fac} & \ident \lambd[n][\fn{IsZero}\, n\, \num{1}] \\    & \qquad (\fn{Mult}\, n  ((\lambd[n][\fn{IsZero} \, n \, \num 1\, (\fn{Mult}\, n\, (\fn{Fac}    (\fn{Pred}\, n)))]) (\fn{Pred}\, n)))\end{align*}and we still haven't gotten rid of $\fn{Fac}$ on the right-handside. Clearly, if we repeat this process, the definition keeps growinglonger and the process never results in a pure lambda term. Thus thisway of defining factorial (or more generally recursive functions)is not feasible.The recursive definition does tell us something, though: If $f$ were aterm representing the factorial function, then the term\[\fn{Fac}' \ident \lambd[g][\lambd[n][\fn{IsZero} \, n \, \num 1\, (\fn{Mult} \, n\, (g (\fn{Pred} n)))]]\]applied to the term $f$, i.e., $\fn{Fac}'\,f$, also represents thefactorial function.  That is, if we regard $\fn{Fac}'$ as a functionaccepting a function and returning a function, the value of$\fn{Fac'}\, f$ is just~$f$, provided $f$ is the factorial. Afunction~$f$ with the property that $\fn{Fac}' \, f \equal[\beta] f$ is calleda \emph{fixpoint} of $\fn{Fac}'$. So, the factorial is a fixpoint of$\fn{Fac}'$.There are terms in the lambda calculus that compute the fixpoints of agiven term, and these terms can then be used to turn a term like$\fn{Fac}'$ into the definition of the factorial. \begin{defn}  \ollabel{defn:Turing-Y}  The \emph{Y-combinator} is the term:  \[  Y \ident (\lambd[ux][x(uux)])(\lambd[ux][x(uux)]).  \]\end{defn}\begin{thm}  $Y$ has the property that $Yg \red g(Yg)$ for any term $g$. Thus,  $Yg$ is always a fixpoint of~$g$.\end{thm}\begin{proof}  Let's abbreviate $(\lambd[ux][x(uux)])$ by~$U$, so that $Y \ident UU$. Then  \begin{align*}    Y g &\ident (\lambd[ux][x(uux)])U\,g \\    &\red (\lambd[x][x(UUx)])g\\    & \red g(UUg) \ident g(Yg).  \end{align*}  Since $g(Yg)$ and $Yg$ both reduce to $g(Yg)$, $g(Yg) \equal[\beta]  Yg$, so $Yg$ is a fixpoint of~$g$.\end{proof}Of course, since $Yg$ is a redex, the reduction can continue indefinitely:\begin{align*}  Y g &\red g (Y g) \\    &\red g (g (Y g)) \\    &\red g(g (g (Y g)))\\    &\ldots\end{align*}So we can think of $Yg$ as $g$ applied to itself infinitely manytimes. If we apply~$g$ to it one additional time, we---so tospeak---aren't doing anything extra; $g$~applied to~$g$ appliedinfinitely many times to~$Yg$ is still $g$~applied to~$Yg$ infinitelymany times.Note that the above sequence of $\beta$-reduction steps startingwith~$Yg$ is infinite. So if we apply $Yg$ to some term, i.e.,consider $(Yg)N$, that term will also reduce to infinitely manydifferent terms, namely $(g(Yg))N$, $(g(g(Yg)))N$, \dots. It isnevertheless possible that some \emph{other} sequence of reductionsteps does terminate in a normal form.Take the factorial for instance. Define $\fn{Fac}$ as $Y\, \fn{Fac}'$(i.e., a fixpoint of $\fn{Fac'}$). Then:\begin{align*}  \fn{Fac}\,\num 3  &\red Y\, \fn{Fac}' \, \num 3 \\  &\red \fn{Fac}' (Y \,\fn{Fac}') \, \num 3 \\  &\ident (\lambd[x][\lambd[n][\fn{IsZero} \, n\, \num 1\,      (\fn{Mult}\, n\, (x (\fn{Pred}\, n)))]]) \, \fn{Fac} \, \num 3\\  & \red \fn{IsZero} \, \num 3\, \num 1\,      (\fn{Mult}\, \num 3\, (\fn{Fac} (\fn{Pred}\, \num 3))) \\  &\red  \fn{Mult}\, \num 3 \, (\fn{Fac} \, \num 2).  \intertext{Similarly,}  \fn{Fac}\,\num 2  &\red  \fn{Mult}\, \num 2 \, (\fn{Fac} \, \num 1) \\  \fn{Fac}\,\num 1  &\red  \fn{Mult}\, \num 1 \, (\fn{Fac} \, \num 0)  \intertext{but}  \fn{Fac}\,\num 0  &\red \fn{Fac}' (Y \,\fn{Fac}') \, \num 0 \\  &\ident (\lambd[x][\lambd[n][\fn{IsZero} \, n\, \num 1\,      (\fn{Mult}\, n\, (x (\fn{Pred}\, n)))]]) \, \fn{Fac} \, \num 0\\  & \red \fn{IsZero} \, \num 0\, \num 1\,      (\fn{Mult}\, \num 0\, (\fn{Fac} (\fn{Pred}\, \num 0))).\\  &\red \num 1.  \intertext{So together}  \fn{Fac}\,\num 3  &\red  \fn{Mult}\, \num 3 \,  (\fn{Mult} \, \num 2\, (\fn{Mult} \, \num 1\, \num 1)).\end{align*}What goes for $\fn{Fac'}$ goes for any recursive definition. Suppose wehave a recursive equation\begin{align*}g\,x_1\dots x_n & \equal[\beta] N\intertext{where $N$ may contain~$g$ and $x_1$, \dots,~$x_n$. Then there isalways a term~$G \ident (Y \lambd[g][\lambd[x_1\dots x_n][N]])$ suchthat}G\,x_1 \dots x_n & \equal[\beta] \Subst{N}{G}{g}.\intertext{For by the fixpoint theorem,}G \ident (Y \lambd[g][\lambd[x_1\dots x_n][N]]) & \red \lambd[g][\lambd[x_1\dots x_n][N]](Y \lambd[g][\lambd[x_1\dots x_n][N]])\\& \ident (\lambd[g][\lambd[x_1\dots x_n][N]])\,G\intertext{and consequently}G\,x_1 \dots x_n & \red (\lambd[g][\lambd[x_1\dots x_n][N]])\,G\,x_1\dots x_n\\& \red (\lambd[x_1\dots x_n][\Subst{N}{G}{g}])\,x_1\dots x_n\\  & \red \Subst{N}{G}{g}.\end{align*}The $Y$ combinator of \olref{defn:Turing-Y} is due to AlanTuring. Alonzo Church had proposed a different version which we'llcall~$Y_C$:\[Y_C \ident \lambd[g][(\lambd[x][g(xx)])(\lambd[x][g(xx)])].\]Church's combinator is a bit weaker than Turing's in that $Yg\equal[\beta] g(Yg)$ but not $Yg \bred g(Yg)$. Let $V$ be the term$\lambd[x][g(xx)]$, so that $Y_C \ident \lambd[g][VV]$. Then\begin{align*}  VV & \ident (\lambd[x][g(xx)])V \red g(VV)  \text{ and thus}\\  Y_C g & \ident (\lambd[g][VV])g \red VV \red g(VV), \text{ but also}\\  g(Y_C g) & \ident g((\lambd[g][VV])g) \red g(VV).\end{align*}In other words, $Y_Cg$ and $g(Y_Cg)$ reduce to a common term $g(VV)$; so $Y_Cg\equal[\beta] g(Y_Cg)$. This is often enough for applications.\end{document}

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

% Part: lambda-calculus% Chapter: lambda-definability% Section: minimization\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{ldf}{min}\olsection{Minimization}The general recursive functions are those that can be obtained fromthe basic functions $\Zero$, $\Succ$, $\Proj{n}{i}$ by composition,primitive recursion, and regular minimization. To show that allgeneral recursive functions are !!{lambda definable} we have to showthat any function defined by regular minimization from !!a{lambda  definable} function is itself !!{lambda definable}.\begin{lem}  \ollabel{lem:min} If $f(x_1, \dots, x_k, y)$ is regular and  !!{lambda definable}, then $g$~defined by  \[  g(x_1, \dots, x_k) = \umin{y}{f(x_1,\dots,x_k, y) = 0}  \]  is also !!{lambda definable}.\end{lem}\begin{proof}  Suppose the lambda term~$F$ $\lambda$-defines the regular  function $f(\vec x, y)$. To !!{lambda define}~$h$ we use a search  function and a fixpoint combinator:  \begin{align*}    \fn{Search} & \ident \lambd[g][\lambd[f\,\vec{x}\,y][        \fn{IsZero} (f\, \vec{x}\, y)\, y\, (g\, \vec{x} (\fn{Succ}\, y)]]\\    H & \ident \lambd[\vec x][(Y \, \fn{Search}) F\, \vec{x}\, \num{0}],  \end{align*}  where $Y$ is any fixpoint combinator. Informally speaking,  $\fn{Search}$ is a self-referencing function: starting with~$y$,  test whether $f\, \vec x\, y$ is zero: if so, return~$y$, otherwise call  itself with $\fn{Succ}\, y$. Thus $(Y \, \fn{Search}) F  \num{n_1}\dots\num{n_k}\,\num{0}$ returns the least~$m$ for which $f(n_1,  \dots, n_k, m) = 0$.    Specifically, observe that  \begin{align*}    (Y \, \fn{Search}) F \num{n_1}    \dots\num{n_k}\, \num{m} & \red \num{m}    \intertext{if $f(n_1, \dots,      n_k, m) = 0$, or}    & \red (Y \, \fn{Search}) F\, \num{n_1} \dots\num{n_k}\, \num{m+1}    \intertext{otherwise. Since $f$ is regular, $f(n_1, \dots, n_k, y)      = 0$ for some $y$, and so}    (Y \, \fn{Search}) F \num{n_1} \dots\num{n_k}\,\num{0}    & \red \num{h(n_1, \dots, n_k)}.    \end{align*}\end{proof}\begin{prop}  Every general recursive function is !!{lambda definable}.\end{prop}\begin{proof} By \olref[prf]{lem:basic}, all basic functions are !!{lambda definable}, and by \olref[prf]{lem:comp}, \olref[prf]{lem:prim}, and \olref{lem:min}, the !!{lambda definable} functions are closed under composition, primitive recursion, and regular minimization.\end{proof}\end{document}

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

% Part: lambda-calculus% Chapter: lambda-definability% Section: partial-recursive-functions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{ldf}{par}\olsection{Partial Recursive Functions are \usetoken{S}{lambda definable}}Partial recursive functions are those obtained from the basicfunctions by composition, primitive recursion, and unboundedminimization. They differ from general recursive function in that thefunctions used in unbounded search are not required to be regular.Not requiring regularity means that functions defined by minimizationmay sometimes not be defined. At first glance it might seem that the same methods used to show thatthe (total) general recursive functions are all !!{lambda definable} canbe used to prove that all partial recursive functions are!!{lambda definable}.  For instance, the composition of $f$ with $g$ is!!{lambda define}d by $\lambd[x][F (G x)]$ if $f$ and $g$ are!!{lambda define}d by terms $F$ and~$G$, respectively. However, when thefunctions are partial, this is problematic. When $g(x)$ is undefined,meaning $G x$ has no normal form. In most cases this means that $F (Gx)$ has no normal forms either, which is what we want.  But considerwhen $F$ is $\lambd[x][\lambd[y][y]]$, in which case $F (G x)$ doeshave a normal form ($\lambd[y][y]$). This problem is not insurmountable, and there are ways to!!{lambda define} all partial recursive functions in such a way thatundefined values are represented by terms without a normal form.These ways are, however, somewhat more complicated and less intuitivethan the approach we have taken for general recursive functions. Werecord the theorem here without proof:\begin{thm}  All partial recursive functions are !!{lambda definable}.\end{thm}\end{document}

content/lambda-calculus/lambda-definability/lambda-definable-recursive.tex

% Part: lambda-calculus% Chapter: lambda-definability% Section: lambda-definable-recursive\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{dfl}{ldr}\olsection{\usetoken{S}{lambda definable} Functions are Recursive}Not only are all partial recursive functions !!{lambda definable}, theconverse is true, too. That is, all !!{lambda definable} functions arepartial recursive.\begin{thm}  \ollabel{thm:lambda-computable} If a partial function $f$ is  !!{lambda definable}, it is partial recursive.\end{thm}\begin{proof}  We only sketch the proof. First, we arithmetize $\lambd$-terms,  i.e., systematially assign G\"odel numbers to $\lambd$-terms, using  the usual power-of-primes coding of sequences. Then we define a  partial recursive function $\fn{normalize}(t)$ operating on the  G\"odel number~$t$ of a lambda term as argument, and which returns  the G\"odel number of the normal form if it has one, or is undefined  otherwise.  Then define two partial recursive functions  $\fn{toChurch}$ and $\fn{fromChurch}$ that maps natural numbers to  and from the G\"odel numbers of the corresponding Church numeral.  Using these recursive functions, we can define the function~$f$ as a  partial recursive function. There is a $\lambd$-term~$F$ that  !!{lambda define}s~$f$. To compute $f(n_1, \dots, n_k)$, first obtain  the G\"odel numbers of the corresponding Church numerals using  $\fn{toChurch}(n_i)$, append these to $\Gn{F}$ to obtain the G\"odel  number of the term $F \num{n_1}\dots\num{n_k}$. Now use  $\fn{normalize}$ on this G\"odel number. If $f(n_1, \dots, n_k)$ is  defined, $F \num{n_1}\dots\num{n_k}$ has a normal form (which must  be a Church numeral), and otherwise it has no normal form (and so  \[\fn{normalize}(\Gn{F\num{n_1}\dots\num{n_k}})\] is undefined).  Finally, use $\fn{fromChurch}$ on the G\"odel number of the  normalized term.\end{proof}\end{document}