Lambda calculus

Introduction to Lambda Calculus

content/lambda-calculus/introduction/introduction.tex

% Part: lambda-calculus% Chapter: introduction\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{lam}{int}{Introduction}\begin{editorial}This chapter consists of Jeremy's original concise notes on the lambdacalculus. The sections need to be combined, and the material on lambdadefinability merged with the material in the separate, more detailedchapter on lambda definability.\end{editorial}\olimport{overview}\olimport{syntax}\olimport{reduction}\olimport{church-rosser}\olimport{currying}\olimport{lambda-definability}\olimport{lambda-computable}\olimport{computable-lambda}\olimport{basic-pr-lambda}\olimport{composition}\olimport{primitive-recursion}\olimport{fixed-point-combinator}\olimport{minimization}\OLEndChapterHook\end{document}

content/lambda-calculus/introduction/overview.tex

% Part: lambda-calculus% Chapter: introduction% Section: overview\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{ovr}\olsection{Overview}The lambda calculus was originally designed by Alonzo Church in theearly 1930s as a basis for constructive logic, and \emph{not} as amodel of the computable functions. But it was soon shown to beequivalent to other definitions of computability, such as the Turingcomputable functions and the partial recursive functions. The factthat this initially came as a small surprise makes thecharacterization all the more interesting.Lambda notation is a convenient way of referring to a functiondirectly by a symbolic expression which defines it, instead ofdefining a name for it. Instead of saying ``let $f$ be the functiondefined by $f(x) = x + 3$,'' one can say, ``let $f$ be the function$\lambd[x][(x + 3)]$.''  In other words, $\lambd[x][(x+3)]$ is just a\emph{name} for the function that adds three to its argument. In thisexpression, $x$ is a dummy variable, or a placeholder: the samefunction can just as well be denoted by $\lambd[y][(y + 3)]$. Thenotation works even with other parameters around. For example, suppose$g(x, y)$ is a function of two variables, and $k$ is a naturalnumber. Then $\lambd[x][g(x,k)]$ is the function which maps any~$x$to~$g(x, k)$.This way of defining a function from a symbolic expression is known as\emph{lambda abstraction}. The flip side of lambda abstraction is\emph{application}: assuming one has a function $f$ (say, defined onthe natural numbers), one can \emph{apply} it to any value, like 2. Inconventional notation, of course, we write~$f(2)$ for the result.What happens when you combine lambda abstraction with application?Then the resulting expression can be simplified, by ``plugging'' theapplicand in for the abstracted variable. For example,\[(\lambd[x][(x + 3)])(2)\]can be simplified to~$2 + 3$.Up to this point, we have done nothing but introduce new notations forconventional notions. The lambda calculus, however, represents a moreradical departure from the set-theoretic viewpoint. In this framework:\begin{enumerate}\item Everything denotes a function.\item Functions can be defined using lambda abstraction.\item Anything can be applied to anything else.\end{enumerate}For example, if $F$ is a term in the lambda calculus, $F(F)$ is alwaysassumed to be meaningful. This liberal framework is known as the\emph{untyped} lambda calculus, where ``untyped'' means ``norestriction on what can be applied to what.''\begin{digress}There is also a \emph{typed} lambda calculus, which is an importantvariation on the untyped version. Although in many ways the typedlambda calculus is similar to the untyped one, it is much easier toreconcile with a classical set-theoretic framework, and has some verydifferent properties.Research on the lambda calculus has proved to be central intheoretical computer science, and in the design of programminglanguages. LISP, designed by John McCarthy in the 1950s, is an earlyexample of a language that was influenced by these ideas.\end{digress}\end{document}

content/lambda-calculus/introduction/syntax.tex

% Part: lambda-calculus% Chapter: introduction% Section: syntax\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{syn}\olsection{The Syntax of the Lambda Calculus}One starts with a sequence of variables $x$, $y$, $z$,~\dots and someconstant symbols $a$, $b$, $c$,~\dots. The set of terms is definedinductively, as follows:\begin{enumerate}\item Each variable is a term.\item Each constant is a term.\item If $M$ and $N$ are terms, so is $(MN)$.\item If $M$ is a term and $x$ is a variable, then $(\lambd[x][M])$ is a  term.\end{enumerate}Terms of the form $(MN)$ are called \emph{applications} and those ofthe form $(\lambd[x][M])$ \emph{abstractions}.The system without any constants at all is called the \emph{pure}lambda calculus. We'll mainly be working in the pure$\lambd$-calculus, so all lowercase letters will stand for variables.We use uppercase letters ($M$, $N$, etc.) to stand for terms of the$\lambd$-calculus.We will follow a few notational conventions:\begin{conv}\begin{enumerate}\item When parentheses are left out, application takes place from left  to right. For example, if $M$, $N$, $P$, and $Q$ are terms, then  $MNPQ$ abbreviates $(((MN)P)Q)$.\item Again, when parentheses are left out, lambda abstraction is to  be given the widest scope possible. From example, $\lambd[x][MNP]$ is  read $(\lambd[x][((MN)P)])$.\item A lambda can be used to abstract multiple variables. For  example, $\lambd[xyz][M]$ is short for  $\lambd[x][\lambd[y][\lambd[z][M]]]$.\end{enumerate}\end{conv}For example,\[\lambd[xy][xxyx \lambd[z][xz]]\]abbreviates\[\lambd[x][\lambd[y][((((xx)y)x)(\lambd[z][(xz)]))]].\]You should memorize these conventions. They will drive you crazy atfirst, but you will get used to them, and after a while they willdrive you less crazy than having to deal with a morass of parentheses.Two terms that differ only in the names of the bound variables arecalled $\alpha$-equivalent; for example, $\lambd[x][x]$ and$\lambd[y][y]$. It will be convenient to think of these as being the``same'' term; in other words, when we say that $M$ and $N$ are thesame, we also mean ``up to renamings of the bound variables.''Variables that are in the scope of a $\lambd$ are called ``bound'',while others are called ``free.'' There are no free variables in theprevious example; but in\[(\lambd[z][yz])x\]$y$ and $x$ are free, and $z$ is bound.\end{document}

content/lambda-calculus/introduction/reduction.tex

% Part: lambda-calculus% Chapter: introduction% Section: reduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{red}\olsection{Reduction of Lambda Terms}What can one do with lambda terms? Simplify them. If $M$ and $N$ areany lambda terms and $x$ is any variable, we can use $\Subst{M}{N}{x}$ todenote the result of substituting $N$ for~$x$ in~$M$, after renamingany bound variables of $M$ that would interfere with the freevariables of~$N$ after the substitution. For example,\[\Subst{(\lambd[w][xxw])}{yyz}{x} = \lambd[w][(yyz)(yyz)w].\]\begin{digress}Alternative notations for substitution are $[N/x]M$, $[x/N]M$, andalso $M[x/N]$. Beware!\end{digress}Intuitively, $(\lambd[x][M])N$ and $\Subst{M}{N}{x}$ have the samemeaning; the act of replacing the first term by the second is called\emph{$\beta$-contraction}. $(\lambd[x][M])N$ is called a \emph{redex}and $\Subst{M}{N}{x}$ its \emph{contractum}. Generally, if it ispossible to change a term $P$ to~$P'$ by $\beta$-contraction of somesubterm, we say that $P$ \emph{$\beta$-reduces to $P'$ in one step},and write $P \redone P'$. If from $P$ we can obtain~$P'$ with somenumber of one-step reductions (possibly none), then $P$\emph{$\beta$-reduces} to~$P'$; in symbols, $P \red P'$. A term thatcannot be $\beta$-reduced any further is called\emph{$\beta$-irreducible}, or \emph{$\beta$-normal}. We will say``reduces'' instead of ``$\beta$-reduces,'' etc., when the context isclear.Let us consider some examples.\begin{enumerate}\item We have\begin{align*}(\lambd[x][xxy]) \lambd[z][z] & \redone (\lambd[z][z])(\lambd[z][z]) y \\& \redone (\lambd[z][z]) y \\& \redone y.\end{align*}\item ``Simplifying'' a term can make it more complex:\begin{align*}(\lambd[x][xxy])(\lambd[x][xxy]) & \redone (\lambd[x][xxy])(\lambd[x][xxy])y \\& \redone (\lambd[x][xxy])(\lambd[x][xxy])yy \\& \redone \dots\end{align*}\item It can also leave a term unchanged:\[(\lambd[x][xx])(\lambd[x][xx]) \redone (\lambd[x][xx])(\lambd[x][xx]).\]\item Also, some terms can be reduced in more than one way; for  example,\[(\lambd[x][(\lambd[y][yx]) z)] v \redone (\lambd[y][yv]) z\]by contracting the outermost application; and\[(\lambd[x][(\lambd[y][yx]) z)] v \redone (\lambd[x][zx]) v\]by contracting the innermost one. Note, in this case, however, thatboth terms further reduce to the same term, $zv$.\end{enumerate}The final outcome in the last example is not a coincidence, but ratherillustrates a deep and important property of the lambda calculus, known as the``Church--Rosser property.''\end{document}

content/lambda-calculus/introduction/church-rosser.tex

% Part: lambda-calculus% Chapter: introduction% Section: church-rosser\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{cr}\olsection{The Church--Rosser Property}\begin{thm}\ollabel{thm:church-rosser}Let $M$, $N_1$, and $N_2$ be terms, such that $M \red N_1$ and $M \redN_2$. Then there is a term $P$ such that $N_1 \red P$ and $N_2 \red P$.\end{thm}\begin{cor}Suppose $M$ can be reduced to normal form. Then this normal form isunique.\end{cor}\begin{proof}If $M \red N_1$ and $M \red N_2$, by the previous theorem there is aterm~$P$ such that $N_1$ and $N_2$ both reduce to~$P$. If $N_1$and~$N_2$ are both in normal form, this can only happen if $N_1 \ident P \identN_2$.\end{proof}Finally, we will say that two terms $M$ and~$N$ are\emph{$\beta$-equivalent}, or just \emph{equivalent}, if they reduceto a common term; in other words, if there is some $P$ such that $M\red P$ and $N \red P$. This is written $M \equal[\beta] N$. Using\olref{thm:church-rosser}, you can check that $\equal[\beta]$ is anequivalence relation, with the additional property that for every $M$and~$N$, if $M \red N$ or $N \red M$, then $M \equal[\beta] N$. (In fact, onecan show that $\equal[\beta]$ is the \emph{smallest} equivalence relationhaving this property.)\end{document}

content/lambda-calculus/introduction/currying.tex

% Part: lambda-calculus% Chapter: representability% Section: currying\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{rep}{cur} \olsection{Currying}A $\lambd$-abstract $\lambd[x][M]$ represents a function of oneargument, which is quite a limitation when we want to define functionaccepting multiple arguments.  One way to do this would be byextending the $\lambd$-calculus to allow the formation of pairs,triples, etc., in which case, say, a three-place function$\lambd[x][M]$ would expect its argument to be a triple.  However, itis more convenient to do this by \emph{Currying}.Let's consider an example. We'll pretend for a moment that we have a$+$ operation in the $\lambd$-calculus. The addition function is$2$-place, i.e., it takes two arguments.  But a $\lambd$-abstract onlygives us functions of one argument: the syntax does not allowexpressions like $\lambd[(x,y)][(x+y)]$.  However, we can consider theone-place function~$f_x(y)$ given by $\lambd[y][(x+y)]$, which adds$x$ to its single argument~$y$.  Actually, this is not a singlefunction, but a family of different functions ``add $x$,'' one foreach number~$x$.  Now we can define another one-place function~$g$ as$\lambd[x][f_x]$. Applied to argument $x$, $g(x)$ returns thefunction~$f_x$---so its values are other functions.  Now if we apply$g$ to $x$, and then the result to~$y$ we get: $(g(x))y = f_x(y) =x+y$.  In this way, the one-place function~$g$ can do the same job asthe two-place addition function. ``Currying'' simply refers to thistrick for turning two-place functions into one place functions (whosevalues are one-place functions).Here is an example properly in the syntax of the $\lambd$-calculus.How do we represent the function $f(x,y) = x$? If we want to define afunction that accepts two arguments and returns the first, we canwrite $\lambd[x][\lambd[y][x]]$, which literally is a function thataccepts an argument~$x$ and returns the function~$\lambd[y][x]$. Thefunction $\lambd[y][x]$ accepts another argument~$y$, but drops it,and always returns~$x$.  Let's see what happens when we apply$\lambd[x][\lambd[y][x]]$ to two arguments:\begin{align*}  (\lambd[x][\lambd[y][x]])MN   \bredone & (\lambd[y][M])N \\  \bredone & M\end{align*}In general, to write a function with parameters $x_1$, \dots,~$x_n$defined by some term~$N$, we can write$\lambd[x_1][\lambd[x_2][\ldots\lambd[x_n][N]]]$. If we apply $n$ argumentsto it we get:\begin{multline*}  (\lambd[x_1][\lambd[x_2][\ldots\lambd[x_n][N]]]) M_1 \dots M_n \bredone\\  \begin{aligned}  \bredone {} & (\Subst{(\lambd[x_2][\ldots\lambd[x_n][N]])}{M_1}{x_1}) M_2  \dots M_n\\   \eqs {} & (\lambd[x_2][\ldots\lambd[x_n][\Subst{N}{M_1}{x_1}]]) M_2            \dots M_n \\  \vdots & \\  \bredone {} &\Subst{\Subst{P}{M_1}{x_1}\ldots}{M_n}{x_n}  \end{aligned}\end{multline*}The last line literally means substituting $M_i$ for $x_i$ in the bodyof the function definition, which is exactly what we want whenapplying multiple arguments to a function.\end{document}

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

% Part: lambda-calculus% Chapter: introduction% Section: lambda-definability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{rep}\olsection{\usetoken{S}{lambda definable} Arithmetical Functions}How can the lambda calculus serve as a model of computation? At first,it is not even clear how to make sense of this statement. To talkabout computability on the natural numbers, we need to find a suitablerepresentation for such numbers. Here is one that works surprisinglywell.\begin{defn}For each natural number~$n$, define the \emph{Church numeral}$\num{n}$ to be the lambda term $\lambd[x][\lambd[y][(x(x(x(\dotsx(y)))))]]$, where there are $n$ $x$'s in all.\end{defn}The terms $\num{n}$ are ``iterators'': on input $f$, $\num{n}$ returnsthe function mapping $y$ to $f^n(y)$. Note that each numeral isnormal. We can now say what it means for a lambda term to ``compute''a function on the natural numbers.\begin{defn}Let $f(x_0, \dots, x_{k-1})$ be an $n$-ary partial function from $\Nat$to $\Nat$. We say a $\lambd$-term~$F$ \emph{!!{lambda define}s}~$f$ iff for everysequence of natural numbers $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}\begin{thm}\ollabel{thm:lambda-def}A function $f$ is a partial computable function if and only if it is!!{lambda defined} by a lambda term.\end{thm}\begin{explain}This theorem is somewhat striking. As a model of computation, thelambda calculus is a rather simple calculus; the only operations arelambda abstraction and application!{} From these meager resources,however, it is possible to implement any computational procedure.\end{explain}\end{document}

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

% Part: lambda-calculus% Chapter: introduction% Section: lambda-computable\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{cmp}\olsection{\usetoken{S}{lambda definable} Functions are Computable}\begin{thm}\ollabel{thm:lambda-computable}If a partial function $f$ is !!{lambda defined} by a lambda term, it iscomputable.\end{thm}\begin{proof}Suppose a function~$f$ is !!{lambda defined} by a lambda term~$X$. Let usdescribe an informal procedure to compute~$f$. On input $m_0$,\dots,~$m_{n-1}$, write down the term $X \num m_0 \ldots \numm_{n-1}$. Build a tree, first writing down all the one-step reductionsof the original term; below that, write all the one-step reductions ofthose (i.e., the two-step reductions of the original term); and keepgoing. If you ever reach a numeral, return that as the answer;otherwise, the function is undefined.An appeal to Church's thesis tells us that this function iscomputable. A better way to prove the theorem would be to give arecursive description of this search procedure. For example, onecould define a sequence primitive recursive functions and relations,``$\fn{IsASubterm}$,'' ``$\fn{Substitute}$,''``$\fn{ReducesToInOneStep}$,'' ``$\fn{ReductionSequence}$,''``$\fn{Numeral}$,'' etc. The partial recursive procedure for computing$f(m_0, \dots, m_{n-1})$ is then to search for a sequence of one-stepreductions starting with $X \num{m_0} \dots \num{m_{n-1}}$ and endingwith a numeral, and return the number corresponding to that numeral.The details are long and tedious but otherwise routine.\end{proof}\end{document}

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

% Part: lambda-calculus% Chapter: introduction% Section: computable-lambda\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{lrp}\olsection{Computable Functions are \usetoken{S}{lambda definable}}\begin{thm}\ollabel{thm:computable-lambda}Every computable partial function is !!{lambda definable}.\end{thm}\begin{proof}We need to show that every partial computable function~$f$ is!!{lambda defined} by a lambda term~$F$. By Kleene's normal formtheorem, it suffices to show that every primitive recursive functionis !!{lambda defined} by a lambda term, and then that the functions!!{lambda definable} are closed under suitable compositions andunbounded search. To show that every primitive recursive function is!!{lambda defined} by a lambda term, it suffices to show that theinitial functions are !!{lambda definable}, and that the partialfunctions that are !!{lambda definable} are closed undercomposition, primitive recursion, and unbounded search.\end{proof}We will use a more conventional notation to make the rest of the proofmore readable. For example, we will write $M(x, y, z)$ instead of$Mxyz$. While this is suggestive, you should remember that terms inthe untyped lambda calculus do not have associated arities; so, forthe same term~$M$, it makes just as much sense to write $M(x,y)$ and$M(x,y,z,w)$. But using this notation indicates that we are treating$M$ as a function of three variables, and helps make the intentionsbehind the definitions clearer. In a similar way, we will say ``define$M$ by $M(x,y,z) = \dots$'' instead of ``define $M$ by $M =\lambd[x][\lambd[y][\lambd[z][\dots]]]$.''\end{document}

content/lambda-calculus/introduction/basic-pr-lambda.tex

% Part: lambda-calculus% Chapter: introduction% Section: basic-pr-lambda\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{bas}\olsection{The Basic Primitive Recursive Functions are \usetoken{S}{lambda definable}}\begin{lem}The functions $\Zero$, $\Succ$, and $\Proj{n}{i}$ are !!{lambda definable}.\end{lem}\begin{proof}$\Zero$ is just$\lambd[x][\lambd[y][y]]$.The successor function~$\Succ$, isdefined by $\fn{Succ}(u) = \lambd[x][\lambd[y][x(uxy)]]$. You shouldthink about why this works; for each numeral $\num{n}$, thought of asan iterator, and each function~$f$, $\fn{Succ}(\num{n},f)$ is a function that,on input~$y$, applies $f$ $n$ times starting with~$y$, and thenapplies it once more.There is nothing to say about projections: $\fn{Proj}^n_i(x_0, \dots,x_{n-1}) = x_i$. In other words, by our conventions, $\fn{Proj}^n_i$ isthe lambda term $\lambd[x_0][\dots \lambd[x_{n-1}][x_i]]$.\end{proof}\end{document}

content/lambda-calculus/introduction/composition.tex

% Part: lambda-calculus% Chapter: introduction% Section: composition\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{com}\olsection{The \usetoken{S}{lambda definable} Functions are Closed under Composition}\begin{lem}The !!{lambda definable} functions are closed under composition.\end{lem}\begin{proof}Suppose $f$ is defined by composition from $h$, $g_0,$\dots,~$g_{k-1}$. Assuming $h$, $g_0$, \dots,~$g_{k-1}$ are!!{lambda defined} by $H$, $G_0$, \dots,~$G_{k-1}$,respectively, we need to find a term~$F$ that !!{lambda define}s~$f$. But wecan simply define~$F$ by\[F(x_0, \dots, x_{l-1}) = H(G_0(x_0, \dots, x_{l-1}),\dots, G_{k-1}(x_0, \dots, x_{l-1})).\]In other words, the language of the lambda calculus is well suited torepresent composition.\end{proof}\end{document}

content/lambda-calculus/introduction/primitive-recursion.tex

% Part: lambda-calculus% Chapter: introduction% Section: primitive-recursion\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{pr}\olsection{\usetoken{S}{lambda definable} Functions are Closed under Primitive Recursion}When it comes to primitive recursion, we finally need to do somework. We will have to proceed in stages. As before, on the assumptionthat we already have terms $G$ and $H$ that !!{lambda define} functions$g$ and~$h$, respectively, we want a term $H$ that !!{lambda define}s thefunction~$f$ defined by\begin{align*}f(0, \vec z) & = g(\vec z) \\f(x+1, \vec z) & = h(z, f(x,\vec z), \vec z).\end{align*}So, in general, given lambda terms $G'$ and~$H'$, it suffices to finda term~$F$ such that\begin{align*}F(\num{0}, \vec z) & \equiv G(\vec z) \\F(\overline{n+1}, \vec z) & \equiv H(\num{n}, F(\num{n}, \vec z), \vec z)\end{align*}for every natural number~$n$; the fact that $G'$ and~$H'$ !!{lambda define}$g$ and~$h$ means that whenever we plug in numerals $\num{\vec m}$for $\vec z$, $F(\num{n+1}, \num{\vec m})$ will normalize to theright answer.But for this, it suffices to find a term~$F$ satisfying\begin{align*}F(\num 0) & \equiv G \\F(\overline {n+1}) & \equiv H(\num{n},F(\num{n}))\intertext{for every natural number $n$,  where}G & = \lambd[\vec z][G'(\vec z)] \text{ and}\\H(u,v) & = \lambd[\vec z][H'(u,v(u,\vec z),\vec z)].\end{align*}In other words, with lambda trickery, we can avoid having to worryabout the extra parameters $\vec z$---they just get absorbed in thelambda notation.Before we define the term $F$, we need a mechanism for handlingordered pairs. This is provided by the next lemma.\begin{lem}There is a lambda term $D$ such that for each pair of lambda terms $M$and~$N$, $D(M,N)(\num{0}) \red M$ and $D(M,N)(\num{1}) \red N$.\end{lem}\begin{proof}First, define the lambda term $K$ by\[K(y) = \lambd[x][y].\]In other words, $K$ is the term $\lambd[y][\lambd[x][y]]$. Looking at itdifferently, for every $M$, $K(M)$ is a constant function thatreturns~$M$ on any input.Now define $D(x,y,z)$ by $D(x,y,z) = z (K(y))x$. Then we have\begin{align*}D(M,N,\num 0) & \red \num 0 (K(N)) M \red M \text{ and}\\D(M,N,\num 1) & \red \num 1 (K(N)) M \red K(N) M \red N,\end{align*}as required.\end{proof}The idea is that $D(M,N)$ represents the pair $\tuple{M, N}$, and if$P$ is assumed to represent such a pair, $P(\num 0)$ and $P(\num 1)$represent the left and right projections, $(P)_0$ and $(P)_1$. We willuse the latter notations.\begin{lem}The !!{lambda definable} functions are closed under primitive recursion.\end{lem}\begin{proof}We need to show that given any terms, $G$ and $H$, we can find a term$F$ such that\begin{align*}F(\num{0}) & \equiv G \\F(\num{n+1}) & \equiv H(\num{n}, F(\num{n}))\end{align*}for every natural number~$n$. The idea is roughly to compute sequencesof \emph{pairs}\[\tuple{\num 0, F(\num 0)}, \tuple{\num 1, F(\num 1)}, \dots,\]using numerals as iterators. Notice that the first pair is just$\tuple{\num 0, G}$. Given a pair $\tuple{\num{n}, F(\num{n})}$, thenext pair, $\tuple{\num{n+1}, F(\num{n+1})}$ is supposed tobe equivalent to $\tuple{\num{n+1}, H(\num{n}, F(\num{n}))}$. Wewill design a lambda term~$T$ that makes this one-step transition.The details are as follows. Define $T(u)$ by\[T(u) = \tuple{S((u)_0), H((u)_0,(u)_1)}.\]Now it is easy to verify that for any number~$n$,\[T(\tuple{\num{n}, M}) \red \tuple{\num{n+1}, H(\num{n}, M)}.\]As suggested above, given $G$ and $H$, define~$F(u)$ by\[F(u) = (u(T,\tuple{\num 0, G}))_1.\]In other words, on input~$\num{n}$, $F$ iterates $T$ $n$ times on$\tuple{\num 0, G}$, and then returns the second component. To startwith, we have\begin{enumerate}\item $\num{0} (T, \tuple{\num 0, G}) \equiv \tuple{\num{0}, G}$\item $F(\num{0}) \equiv G$\end{enumerate}By induction on~$n$, we can show that for each natural number one hasthe following:\begin{enumerate}\item $\num{n+1}(T, \tuple{\num{0}, G}) \equiv \tuple{\num{n+1}, F(\num{n+1})}$\item $F(\num{n+1}) \equiv H(\num{n}, F(\num{n}))$\end{enumerate}For the second clause, we have\begin{align*}F(\num{n+1}) & \red (\num{n+1}(T, \tuple{\num 0, G}))_1 \\& \equiv (T(\num{n} (T, \tuple{\num 0, G})))_1 \\& \equiv (T(\tuple{\num{n}, F(\num{n})}))_1 \\& \equiv (\tuple{\num{n+1}, H(\num{n}, F(\num{n}))})_1 \\& \equiv H(\num{n}, F(\num{n})).\end{align*}Here we have used the induction hypothesis on the second-to-lastline. For the first clause, we have\begin{align*}\num{n+1} (T, \tuple{\num 0, G}) &\equiv T(\num{n} (T, \tuple{\num 0, G})) \\& \equiv T( \tuple{\num{n}, F(\num{n})}) \\& \equiv \tuple{\num{n+1}, H(\num{n}, F(\num{n}))} \\& \equiv \tuple{\num{n+1}, F(\num{n+1})}.\end{align*}Here we have used the second clause in the last line. So we have shown$F(\num 0) \equiv G$ and, for every $n$, $F(\num {n+1}) \equiv H(\numn, F(\num{n}))$, which is exactly what we needed.\end{proof}\end{document}

content/lambda-calculus/introduction/fixed-point-combinator.tex

% Part: lambda-calculus% Chapter: introduction% Section: fixed-point-combinator\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{fix}\olsection{Fixed-Point Combinators}Suppose you have a lambda term $g$, and you want another term $k$ withthe property that $k$ is $\beta$-equivalent to $gk$. Define terms\[\fn{diag}(x) = xx\]and\[l(x) = g(\fn{diag}(x))\]using our notational conventions; in other words, $l$ is the term$\lambd[x][g(xx)]$. Let $k$ be the term $ll$. Then we have\begin{align*}k & = (\lambd[x][g(xx)])(\lambd[x][g(xx)]) \\& \red  g((\lambd[x][g(xx)])(\lambd[x][g(xx)])) \\& = gk.\end{align*}If one takes\[Y = \lambd[g][((\lambd[x][g(xx)])(\lambd[x][g(xx)]))]\]then $Yg$ and $g(Yg)$ reduce to a common term; so $Yg \equiv_\betag(Yg)$. This is known as ``Curry's combinator.'' If instead one takes\[Y = (\lambd[xg][g(xxg)])(\lambd[xg][g(xxg)])\]then in fact $Yg$ reduces to $g(Yg)$, which is a stronger statement.This latter version of $Y$ is known as ``Turing's combinator.''\end{document}

content/lambda-calculus/introduction/minimization.tex

% Part: lambda-calculus% Chapter: introduction% Section: minimization\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{min}\olsection{The \usetoken{S}{lambda definable} Functions are Closed under Minimization}\begin{lem}Suppose $f(x,y)$ is !!{lambda definable}. Let $g$ be defined by\[g(x) \simeq \umin{y}{f(x,y)}.\]Then $g$ is !!{lambda definable}.\end{lem}\begin{proof}The idea is roughly as follows. Given $x$, we will use the fixed-pointlambda term $Y$ to define a function $h_x(n)$ which searches for a~$y$starting at~$n$; then $g(x)$ is just $h_x(0)$. The function~$h_x$ canbe expressed as the solution of a fixed-point equation:\[h_x(n) \simeq\begin{cases}n & \text{if $f(x,n) = 0$} \\h_x(n+1) & \text{otherwise.}\end{cases}\]Here are the details. Since $f$ is primitive recursive, it is!!{lambda defined} by some term $F$. Remember that we also have a lambdaterm~$D$, such that $D(M, N, \bar{0}) \red M$ and $D(M, N, \bar{1})\red N$. Fixing $x$ for the moment, to !!{lambda define} $h_x$ we want tofind a term~$H$ (depending on~$x$) satisfying\[H(\num{n}) \equiv D(\num{n}, H(S(\num{n})), F(x, \num{n})).\]We can do this using the fixed-point term~$Y$. First, let $U$ be theterm\[\lambd[h][\lambd[z][D(z,(h(Sz)),F(x,z))]],\]and then let $H$ be the term~$YU$. Notice that the only free variablein~$H$ is~$x$. Let us show that $H$ satisfies the equation above.By the definition of $Y$, we have\[H = YU \equiv U(YU) = U(H).\]In particular, for each natural number~$n$, we have\begin{align*}H(\num{n}) & \equiv U(H, \num{n}) \\& \red D(\num{n}, H(S(\num{n})), F(x, \num{n})),\end{align*}as required. Notice that if you substitute a numeral $\num{m}$ for~$x$in the last line, the expression reduces to $\num{n}$ if $F(\num{m},\num{n})$ reduces to $\num{0}$, and it reduces to $H(S(\num{n}))$ if$F(\num{m}, \num{n})$ reduces to any other numeral.To finish off the proof, let $G$ be $\lambd[x][H(\num 0)]$. Then $G$!!{lambda define}s~$g$; in other words, for every~$m$, $G(\num m)$reduces to~$\overline {g(m)}$, if $g(m)$ is defined, and has no normalform otherwise.\end{proof}\end{document}