\documentclass[a4paper,10pt]{article}
\usepackage{amssymb}

%opening
\title{Primitive recursion in pure $\lambda$-calculus}
\author{Viktor Engelmann\\Viktor.Engelmann@RWTH-Aachen.de}

\begin{document}

\maketitle

\begin{abstract}

\end{abstract}

\section{Definitions}
...
For example the addition of two numbers $n$ and $m$ can be
achieved by applying the $succ$ function $n$ times to $m$ by using 
\begin{eqnarray*}
 & & n\: succ\: m \\
&=& (\lambda f. \lambda x. \underbrace{f ( f ( \cdots ( f}_{n\textrm{ times}}\: x ) \cdots ) ) ) \: succ \: m \\
&=& (\lambda x. \underbrace{succ (succ ( \cdots ( succ}_{n\textrm{ times}}\: x ) \cdots ) ) )\: m \\
&=& \underbrace{succ (succ ( \cdots ( succ}_{n\textrm{ times}}\: m ) \cdots ) ) \\
\end{eqnarray*}


...
\section{Theorem}
primitive recursive functions can be computed in pure $\lambda$-calculus without the use of a fixedpoint-combinator.


Proof (constructive):\\

Let $\overline{f}$ a primitive recursion with
\begin{eqnarray*}
 \overline{f}(0, x_1, \cdots, x_n) &=& \overline{g}(x_1,\cdots,x_n)\\
 \overline{f}(i, x_1, \cdots, x_n) &=& \overline{h}(x_1,\cdots,x_n, i-1, \overline{f}(i-1,x_1,\cdots,x_n)) \textrm{ for } i > 0
\end{eqnarray*}
and let $g$ and $h$ be $\lambda$-terms that calculate $\overline{g}$ and $\overline{h}$.
if you apply such a function to some values of $i$, you notice a simple pattern

\begin{center}
\begin{tabular}{c|r}
 $i$ & $\overline{f}(i,x_1,\cdots,x_n)$ \\\hline
$0$ & $\overline{g}(x_1,\cdots,x_n)$ \\
$1$ & $\overline{h}(x_1,\cdots,x_n, 0, \overline{g}(x_1,\cdots,x_n))$ \\
$2$ & $\overline{h}(x_1,\cdots,x_n, 1, \overline{h}(x_1,\cdots,x_n, 0, \overline{g}(x_1,\cdots,x_n)))$ \\
$3$ & $\overline{h}(x_1,\cdots,x_n, 2, \overline{h}(x_1,\cdots,x_n, 1, \overline{h}(x_1,\cdots,x_n, 0, \overline{g}(x_1,\cdots,x_n))))$
\end{tabular}
\end{center}

Keep in mind that in the $\lambda$-calculus the result of $h\:x_1\:\cdots\: x_n\: (i-1)$ is a \underline{function}, which is
applied to the result of the recursive call. Let's look at the previous table in terms of the $\lambda$-calculus.

\begin{center}
\begin{tabular}{c|r}
 $i$ & $f\:i\:x_1\: \cdots \: x_n$ \\\hline
$0$ & $g\: x_1 \: \cdots \: x_n $\\
$1$ & $(h\: x_1 \: \cdots \: x_n\: 0)\: (g\:x_1\:\cdots\:x_n) $\\
$2$ & $(h\: x_1 \: \cdots \: x_n\: 1)\: ((h\: x_1\:\cdots\:x_n\: 0)\: (g\:x_1\:\cdots\:x_n))$ \\
$3$ & $(h\: x_1\:\cdots\:x_n\: 2)\: ((h\: x_1 \: \cdots \: x_n \: 1)\: ((h\: x_1\:\cdots\:x_n\: 0)\: (g\: x_1\:\cdots\:x_n))) $
\end{tabular}
\end{center}

Now imagine that $h$ didn't get the $i-1$ parameter. The $\lambda$-terms then would look like this

\begin{center}
\begin{tabular}{c|r}
 $i$ & $f\:i\:x_1\: \cdots \: x_n$ \\\hline
$0$ & $g\: x_1 \: \cdots \: x_n $\\
$1$ & $(h\: x_1 \: \cdots \: x_n)\: (g\:x_1\:\cdots\:x_n) $\\
$2$ & $(h\: x_1 \: \cdots \: x_n)\: ((h\: x_1\:\cdots\:x_n)\: (g\:x_1\:\cdots\:x_n))$ \\
$3$ & $(h\: x_1\:\cdots\:x_n)\: ((h\: x_1 \: \cdots \: x_n)\: ((h\: x_1\:\cdots\:x_n)\: (g\: x_1\:\cdots\:x_n))) $
\end{tabular}
\end{center}

so if $h$ didn't get the $i-1$ parameter, $f\:i\:x_1\:\cdots\:x_n$ would be equivalent to the $i$-fold application of $(h\:x_1\:\cdots\:x_n)$ to $(g\:x_1\:\cdots\:x_n)$.\\[2ex]

In the \underline{pure} $\lambda$-calculus the natural number $i$ is represented by the $\lambda$-term
\[ \lambda f.\lambda x.\underbrace{f (f (\cdots ( f}_{i \textrm{\tiny{ times}}} x ) \cdots ) ) \]
which is the $i$-fold application of the first parameter to the second. Therefore $f$ could be written as
\[ f = \lambda i. \lambda x_1. \cdots .\lambda x_n . i\: (h\: x_1\: \cdots \: x_n)\: (g \: x_1 \: \cdots \: x_n) \]
\\[2ex]

However $h$ still has to get the $i-1$ parameter, but in the pure $\lambda$-terms, it doesn't have to be passed as a parameter
from outside of the functioncall. Instead we can hand it over from the inner terms to the outer terms. To achieve this, we can
simply define functions $\dot{g}$ and $\dot{h}$ which return a \underline{pair} containing the result and also the $i-1$ parameter
for the outer applications of $h$.

\begin{eqnarray*}
 \dot{g} & = & \lambda x_1.\cdots\lambda x_n.( 0, g \: x_1 \: \cdots \: x_n ) \\
 \dot{h} & = & \lambda x_1.\cdots\lambda x_n. \underbrace{\lambda r}_\textrm{\tiny{recursion result}}. ( 1 + (sel_1^2\: r) , h\: x_1\: \cdots \: x_n \: (\underbrace{sel_1^2 \: r}_{i-1}) \: (sel_2^2\: r)) \\
 f&=&\lambda i. \lambda x_1. \cdots \lambda x_n. sel_2^2\: (i\: (\dot{h}\: x_1\: \cdots\: x_n) \: (\dot{g}\: x_1\: \cdots\: x_n))
\end{eqnarray*}

Using known definitions for tuples, this can be translated to pure $\lambda$-calculus like this:
\begin{eqnarray*}
\tilde{g} &=& \lambda x_1.\cdots \lambda x_n.(\underbrace{(\lambda z_1.\lambda z_2.\lambda f.f\: z_1\: z_2)}_{tuple_2}\:\underbrace{(\lambda p.\lambda x.x)}_{0}\:(g\:x_1\:\cdots\:x_n))\\
\tilde{h} &=& \lambda x_1.\cdots\lambda x_n.\lambda r.(\underbrace{(\lambda z_1.\lambda z_2.\lambda f.f\: z_1\: z_2)}_{tuple_2}\: (\underbrace{(\lambda n.\lambda f.\lambda x.f\:(n\: f\:x))}_{succ}\: (((\underbrace{\lambda g.g\:(\lambda y_1.\lambda y_2.y_1)}_{sel_1^2})\: r)))\\
& & (h\:x_1\:\cdots\: x_n\: ((\underbrace{\lambda g.g\:(\lambda y_1.\lambda y_2.y_1)}_{sel_1^2})\: r))\: ((\underbrace{\lambda g.g\:(\lambda y_1.\lambda y_2.y_2)}_{sel_2^2})\: r)))\\
f&=& \lambda i. \lambda x_1.\cdots\lambda x_n.(\underbrace{\lambda g.g\:(\lambda y_1.\lambda y_2.y_2)}_{sel_2^2}) \: (i\: (\tilde{h}\: x_1\: \cdots \: x_n)\: (\tilde{g}\: x_1\: \cdots \: x_n))
\end{eqnarray*}
\begin{flushright}
 $\Box$
\end{flushright}

\section{Conclusions}
One important observation is that this gives us a new characterization for the borderline between primitive-recursive and $\mu$-recursive functions: in the pure $\lambda$-calculus, primitive recursive functions can be computed without using fixedpoint-combinators (provable by structural induction - the above theorem is the crucial part of the induction step), while $\mu$-recursive functions in general require them.\\[1ex]

Also, since every computable set can be computed by \underline{once} applying the $\mu$-operator to a primitive recursive function\footnote{see http://s-inf.de/Skripte/HS/Rekursionstheorie.2003-SS-Thomas.(JRe).Skript.ps page 16}, this also shows that every computable set can
be computed in pure $\lambda$-calculus using only one fixedpoint-combinator (because the $\mu$-operator can be implemented using
only one fixedpoint-combinator).\\[1ex]

Using the same idea as in the proof for the theorem, we don't have to pass $x_1\: \cdots\: x_n$ to $\tilde{h}$ directly, either. Instead we can
define functions which return an $n+2$-tuple, that also contains the $x_1\:\cdots \: x_n$ parameters and get a term for $f$, that has the form
\[ f = \lambda i.\lambda x_1.\cdots\lambda x_n. sel_{n+2}^{n+2}( i\: \ddot{h}\: (\ddot{g}\: x_1\:\cdots \: x_n) )\]
\end{document}