This blog post provides supplementary material for the proof section of Lambda-Calculus and Combinator § 4C Theorem 4.20, the overall intention of the proof is to prove that total recursive functions conforming to Definition 4.18 can be represented using combinators. Here we briefly explain the key part of this proof - the construction of the iteration combinator. This can also be understood as: Writing an iterative program with specific termination conditions in Pure Lambda Calculus.
Recursion and Iteration: In constructing the $R_{\text{Bernays}}$ recursive combinator, to solve for the value $\phi(n)$ of some recursive function $\phi$, one feasible method is to start from $\phi(0)$ and iterate $n$ times to get $\phi(n)$ (roughly as follows: denoting the recursive step update function as $\chi$, $\phi(n) = \chi^n \phi(0)$). Iteration and recursion differ in forward versus reverse direction. The “recursion” in this article aims to describe the structural characteristic of “self-calling”, while the central focus is on solving iteration problems ($0 \rightarrow 1 \rightarrow … \rightarrow n$).
Construction Goal
Assuming we have a check function $X$, with iteration termination condition $XY=_{\beta,w}\bar{0}$, we want to construct a combinator $P$ to obtain the minimal $Y$ satisfying the termination condition. Starting from $Y = \bar{0}$, check if $(XY) =_{\beta,w} \bar{0}$. If the condition is met, return this $Y$, otherwise continue checking $X(\bar{\sigma}Y)$. We want to construct a combinator $P$ to automate this checking process. Formally, we expect $P$ to behave as follows:
$$ PXY =_{\beta,w}Y \quad \text{, if } XY = _{\beta,w}\bar{0};$$
$$ PXY =_{\beta,w}PX(\bar{\sigma}Y), \text{ otherwise} $$
Fully respecting expectations, write a $P$ combinator: $\textcolor{red}{P} \equiv \lambda xy.\textbf{D}y(\textcolor{red}{P}x(\bar{\sigma}y))(xy)$, where $\textbf{D}=\lambda xyz.z(\textbf{K}y)x$. We can use the $\textbf{Y}$ combinator to fix this $P$ ($P \equiv \textbf{Y}(\lambda pxy.\textbf{D}y(px(\bar{\sigma}y))(xy))$). The $P$ solved using the $\textbf{Y}$ combinator has no normal form. We won’t use this $P$ here; instead, we’ll try to construct a $P$ combinator with normal.
Construction Process
Basic Structure
Express the existing $P$ in high-level language pseudocode:
combinator p(x,y): // L1: define p
if (xy == 0):
return const(y)
else:
return p(x, σ y) // L5: call p
Recursive $\lambda$, like $P \equiv \lambda x. MPN$, matches our experience in high-level language programming but doesn’t conform to Lambda Calculus rules, as Lambda Calculus’s inductive definition of $\lambda$-terms doesn’t include rules for assigning identifiers to abstractions. We write identifiers like $P$ only to improve readability and clarify expression structure, not to define recursive functions through identifier reuse like in high-level languages. A detail worth noting is that the symbol we see in books for recording identifiers for $\lambda$-terms is $\equiv$ rather than $=$.
The fact that we can’t define recursion through identifier reuse doesn’t mean we can’t define recursion at all - we just need to rely on an additional layer of abstraction to construct something that is formally non-recursive but effectively recursive.
From a high-level programming perspective, if we want to replace the call to p itself in L5, we can modify our code as follows. For consistency between branches, we design a function list t where two functions correspond to two branches - function getCurrentY will return the current y value, and recursion_p will handle recursion: (Let’s not worry about specific function structure and parameter design/passing yet, we’ll figure that out later, here we only care about the overall structure)
t = [getCurrentY, recursion_p] // list of functions
combinator p(x,y):
if (xy == 0):
return t[0]
else:
return t[1]
How do we express this code in Lambda Calculus? To focus on our current level of abstraction, let’s first simplify the structure of $P \equiv \lambda xy.\textbf{D}y(Px(\bar{\sigma}y))(xy)$ to $P \equiv \lambda xy.\textbf{D}AB(xy)$
Based on expectations/above pseudocode, we can write out the rough $\lambda$ framework as follows:
$$ P \equiv \lambda xy. T(xy)[params] $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda [params]. \dots$$ $$ B \equiv \lambda [params]. …$$
Now $PXY = _{\beta,w} T(XY) $, $ XY = _{\beta, w} \bar{0} \longrightarrow PXY = A; XY \neq _{\beta, w} \bar{0} \longrightarrow PXY = B $ .
We expect to put branch-specific logic in $T$, and put branch selection and branch function parameter passing in $P$.
Specific Details
We ignored many details above, now it’s time to consider them :)
First note a fact: putting branch function parameter passing work in $P$ means that regardless of which branch the current $P$’s $(xy)$ will lead to, our parameter list must be consistent / can only be consistent. Since the case corresponding to $(xy) = _{\beta,w}\bar{0}$ is simpler, only needing to return the current $y$, we’ll consider it later and focus on the $(xy) \neq _{\beta,w}\bar{0}$ case first, letting the former accommodate the latter (since both branches relate to $y$, the parameter list must include $y$ - this is a commonality between branches; moreover, we can even pass all parameters corresponding to both branch functions, then in specific implementations of $A$,$B$ not bind parameters irrelevant to that branch).
Constructing the Recursive (Iterative) Branch
Goal: $XY \neq _{\beta, w} \bar{0} \longrightarrow PXY = B \xlongequal{\text{expected}} PX(\bar{\sigma}Y) $. We want the $\lambda$-term resulting from applying function $\underline{B}$ with $[\underline{params}]$ passed in $\underline{P}$ to have the same structure as $\underline{PXY}$ (note this is not that $B$ and $P$ abstractions themselves having the same structure), just with $Y$ replaced by $(\bar{\sigma}Y)$. To get the same structure as $P$, the simplest method is to pass $P$’s existing components as $[params]$ to $B$ (and also to $A$), then reassemble these components in $B$ to form $P$’s structure:
$$ P \equiv \lambda xy. T(xy)Txy $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda tuv. \dots$$ $$ B \equiv \lambda tuv. q(uv) $$
($ T \mapsto t, x \mapsto u, y \mapsto v$)
Due to $[params]$ passing, $P$’s structure has changed, so we need to synchronize $B$ with the new $P$ structure; additionally, we need to change the passed-in $y$ (bound by $v$) to $\bar{\sigma}y$ inside $B$:
$$ P \equiv \lambda xy. T(xy)Txy $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda tuv. \dots$$ $$ B \equiv \lambda tuv. q(u(\bar{\sigma}v))qu(\bar{\sigma}v) $$
Let’s check: when $XY \neq _{\beta, w} \bar{0}$:
$ \quad PXY $ $ = _{\beta,w} T(XY)TXY $ $ = _{\beta,w} BTXY $ $ = _{\beta,w} T(X(\bar{\sigma}Y))TX(\bar{\sigma}Y) $ $ = _{\beta,w} PX(\bar{\sigma}Y) $
This matches our expectations, completing the iteration branch construction.
Constructing the Iteration Termination Branch
Goal: $XY = _{\beta, w} \bar{0} \longrightarrow PXY = A \xlongequal{\text{expected}} Y $. During $B$’s construction, our existing parameter list is $ t \mapsto T, u \mapsto x, v \mapsto y$. In $A$, we just need to extract $y$, so $A = \lambda tuv.v$. If you want to stay consistent with Definition 4.8’s notation, then $A = \Pi^3_3$.
Complete $\lambda$
$$ P \equiv \lambda xy. T(xy)Txy $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda tuv. v (= _{\beta,w} \Pi^3_3) $$ $$ B \equiv \lambda tuv. q(u(\bar{\sigma}v))qu(\bar{\sigma}v) $$
Brief Note on $P$ in LCaC Theorem 4.20
The definition of $P$ given in LCaC Theorem 4.20 is:
$$ T \equiv \lambda x.\textbf{D}\bar{0}(\lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v)) $$ $$ P \equiv \lambda xy.Tx(xy)(Tx)y $$
Rewritten in format consistent with above:
$$ P \equiv \lambda xy.Tx(xy)(Tx)y $$ $$ T \equiv \lambda x.\textbf{D}AB $$ $$ A \equiv \bar{0} $$ $$ B \equiv \lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v) $$
Treating $(Tx)$ as a whole at times makes the expression more concise, while letting $x$ and $T$ have a binding relationship ($T \equiv \lambda x….$) - still allowing separate use of $x$ inside $T$; the closure of $(Tx)$ in $P$ makes the parameter passing form $B(Tx)y$ - rather than $BTxy$ - making $A$’s design more concise with $A \equiv \bar{0}$.
Though there are slight differences in details, the overall structure is consistent with the $P$ given in this article.
Other
Try expanding the above $P$:
$$ \lambda xy.\lambda x.\textbf{D}\bar{0}(\lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v))x(xy)(\lambda x.\textbf{D}\bar{0}(\lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v))x)y$$
If you’re willing to expand all of these too: $ \textbf{D} = _{\beta, w} \lambda xyz.z(\textbf{K}y)x, \quad \textbf{K} = _{\beta, w} \lambda xy.x $ $ \bar{0} = _{\beta, w} \lambda xy.y $ $ \bar{\sigma} = _{\beta, w} \lambda nfz. f (n f z)$
$$ \lambda xy.\lambda x.(\lambda xyz.z((\lambda xy.x)y)x)(\lambda xy.y)(\lambda uv.u(x(\lambda nfz. f (n f z)))u(\lambda nfz. f (n f z)))x(xy)(\lambda x.(\lambda xyz.z((\lambda xy.x)y)x)(\lambda xy.y)(\lambda uv.u(x(\lambda nfz. f (n f z)))u(\lambda nfz. f (n f z)))x)y$$
We can say that we’ve completed the construction of an iterative program using this pile of symbols + Pure Lambda Calculus computation rules - Programming in Pure Lambda Calculus., great!