Infinite lists in Lambda calculus....

Question

I have been learning Haskell for a number of months now and am now trying to understand the underpinning $\lambda$-calculus, but I have run into a bit of a mental block! How would I go about writing a $λ$-term corresponding to an infinite list (for example $[0, 1, 2, \dots]$)?

Answer 1

The infinite list $[0, 1, 2, \dots]$ satisfies the following identity in Haskell (see here): $$\tag{1} [0,1,2, \dots] = 0 : \mathtt{map} \, (+1) \, [0,1,2,\dots] $$ where $(+1)$ is the function computing the successor of an integer, and $:$ is the function that appends an element to the front of a list. Indeed, $$\mathtt{map} \, (+1) \, [0,1,2,\dots] = [(+1) \, 0, (+1) \, 1, (+1) \, 2, \dots] = [1, 2, 3, \dots]$$ and clearly $$0 : [1, 2, 3, \dots] = [0,1, 2, \dots]$$ therefore, Identity $(1)$ holds.

Can Identity $(1)$ be expressed in the $\lambda$-calculus? Yes! Indeed:

• The natural number $0$ is represented in the $\lambda$-calculus by the Church numeral $\underline{0} = \lambda f. \lambda x. x$ (see here);
• The function $(+1)$ is represented in the $\lambda$-calculus by the $\lambda$-term $\mathsf{succ} = \lambda n. \lambda f. \lambda x. f(n f x)$ (see here);
• The function $:$ is represented in the $\lambda$-calculus by the $\lambda$-term $\mathsf{cons} = \lambda x. \lambda l. \lambda c. \lambda n. c x (l c n)$ (see here);
• The function $\mathtt{map}$ is represented in the $\lambda$-calculus by the $\lambda$-term $\mathsf{map} = \lambda f. \lambda l. \lambda c. l \, \lambda x. c (f x)$ (see here, unfortunately the author of the question has inexplicably deleted it, I hope he/she will undelete it).

Apparently, the only missing $\lambda$-term to represent $(1)$ in the $\lambda$-calculus is $[0,1,2,\dots]$, that is, the $\lambda$-term that we want to define! Let us denote it by $X$, as an unknown variable in a mathematical equation. Thus, $(1)$ can be rewritten as an equation in the $\lambda$-calculus $$\tag{2} X =_\beta \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, X)$$ where $=_\beta$ is $\beta$-equivalence, that is (roughly), the unoriented version of $\beta$-reduction. If we can solve Equation $(2)$ (i.e. we find a $\lambda$-term $X$ such that $(2)$ holds), then such a $\lambda$-term represents the infinite list $[0,1,2,\dots]$. Since $(\lambda x.N)x \to_\beta N$ for any $\lambda$-term $N$, Equation $(2)$ can be equivalently rewritten as $$\tag{3} X =_\beta (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)) X $$ Equation $(3)$ is of interest because it says that the $\lambda$-term $X$ we are looking for is a fixed point of the $\lambda$-term $\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)$. This is where the fixpoint combinator $Y$ of the $\lambda$-calculus becomes relevant, as correctly suggested by @MJD in his comment. Indeed, $Y = \lambda f. (\lambda x. f(xx))(\lambda x. f(xx))$ is a "magic" $\lambda$-term such that, for every $\lambda$-term $M$, $$\tag{4} YM =_\beta M(YM)$$ that is, $YM$ is a fixed point of any $\lambda$-term $M$. Who cares? From Identity $(4)$, replace the generic $M$ with the $\lambda$-term $\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)$, so the following identity holds: $$ Y(\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)) =_\beta (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x)) \big( Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))\big) $$ This shows that $X = Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$ is a solution of Equation $(3)$: just rewrite $(3)$ by replacing $X$ with $Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$. And a solution of Equation $(3)$, and hence of Equation $(2)$, is what we are looking for!

Summing up, the infinite list $[0,1,2,\dots]$ is represented in the $\lambda$-calculus by the $\lambda$-term: $$ Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$$

---

Digression. There are different ways to define the $\lambda$-terms $\mathsf{cons}$ and $\mathsf{map}$, depending on the way lists are encoded in the $\lambda$-calculus.

According to the encoding of lists presented here, a list $[N_1, \dots, N_k]$ is represented by the $\lambda$-term $$\lambda c. \lambda n.c N_1 (c N_2 (\dots(c N_k n)\dots))$$ and the definitions of $\mathsf{cons}$ and $\mathsf{map}$ above work for this encoding.

An alternative encoding of lists is presented here, it requires other (just slightly different) definitions of $\mathsf{cons}$ and $\mathsf{map}$. Note that $Y (\lambda x. \mathsf{cons} \, \underline{0} \, (\mathsf{map} \, \mathsf{succ} \, x))$ always represents the infinite list $[0, 1, 2,\dots]$, provided that $\mathsf{cons}$ and $\mathsf{map}$ are suitable for the encoding of lists under consideration.