How can I study the nature of the structure of evaluation of function in lambda calculus?

Question

I am specifically focusing on lambda calculus, following this paper: A Tutorial Introduction to the Lambda Calculus.

Suppose we have three functions that represent the natural numbers 0 and 1, and a successor function:

$\lambda sz.z = 0$

$\lambda sz.s(z) = 1$

$\lambda wyx.y(wyx) = succ$

Suppose I were to evaluate $succ\ succ\ 1$. As I evaluate this expression, it is becoming clear to me that it's not 3 as I might naively expect, but I do not truly grasp "why." Even as I go through the motions of evaluating the expression, I do not understand the nature of the turn of events and why certain expressions produce a certain result due to their structure and construction.

A question I might ask would be something like, why does $succ$ have that form, and is there an alternative form for $succ$ that produces the same result? If it is unique, what makes it special? I don't know how to answer these questions well yet, so I am seeking guidance.

Is there a method by which I can better visualize or understand the evaluation of expressions and how it affects the "class" of their output? I am very new to lambda calculus, so please excuse me.

Edit: I think I understand the rules for evaluation of lambda calculus (substitution, prevention of name collisions, etc.), but I have a hard time understanding the arbitrary rules by which one can construct lambda calculus' equivalent forms for the natural numbers, the successor functions, and the addition and multiplication functions. It's how these parallels to these concepts were mapped over to lambda calculus that I am interested in.

For example, why are the functions for "choose second," "false," and "discard next argument," and "0" have the same form and thus equivalent? There exists systems in which applying the zero function to a list of object does not result in returning a list with the front-most argument removed. Even if it is a convention, is there a reason why it is structured as such?

For example, why is does the successor function work? One can say that it was discovered through trial and error, but this makes for poor understanding of the nature of a concept besides "it is so" and "it works." I hope this makes sense.

Answer 1

I'll try addressing only some of the questions.

Church numerals are defined to be functions (abstractions in $\lambda$-calculus speech) that take two arguments: a base argument $z$ (stands for zero), and a "successor" function $s$ which will be repeatedly applied to the base $z$. The number of times $n$ we apply $s$ corresponds to some natural number $n$.

The successor function $\mathsf{succ}$ takes a Church numeral corresponding to some $n \in \mathbb{N}$ (the numeral's canonical form is $\lambda sz. s^nz$), and returns a Church numeral corresponding to $n+1$, i.e. some term that behaves like $\lambda sz. s^{n+1}z$.

Notes:

• $s^n z$ means $s (s (s (... s z))...)$, where $s$ applied $n$ times to $z$;
• two abstractions are behaviorally equivalent if applied to the same arguments they yield the same result.

Let's obtain a $\lambda$-term representing $\mathsf{succ}$. In what follows I'm using Church numerals and corresponding natural numbers interchangeably, I hope that it won't cause confusion, since the current domain can be derived from the context.

1. $\mathsf{succ}$ is an abstraction that takes a Church numeral $n$, so $\mathsf{succ} = \lambda n. \textsf{<...>}$

2. $\mathsf{succ}$ returns a Church numeral, which must take 2 arguments, that's why $\mathsf{succ} = \lambda n. (\lambda sz. \textsf{<...>})$

3. After supplying some $s$ and $z$ to $(\mathsf{succ}\ n)$ we must have $s$ applied $n+1$ times to $z$. Notice that the Church numeral $n$ allows us to easily get $s$ applied $n$ times: we just apply $n$ to $s$ and $z$: $(n\ s\ z) = s^n z$. Then, using the fact $s^{n+1} z = s (s^n z)$, we get $s^{n+1} z = s (n\ s\ z)$. Finally, $\mathsf{succ} = \lambda n. (\lambda sz. s (n\ s\ z))$ or, sweetening with some more syntactic sugar, $\mathsf{succ} = \lambda nsz. s (n\ s\ z)$.

The term we've got for the successor function is not unique, one can use any form of $\mathsf{succ}$ as long as it fulfills its role: make "the next" Church numeral out of the current one. For instance, the following is a valid term for $\mathsf{succ}$ too: $\lambda nsz. n s (s z)$, and it can be obtained using the fact $s^{n+1} z = s^n (s z)$.

In fact, there are infinitely many syntactically different $\lambda$-terms for the successor function. We can invent many different (and silly) ways of "implementing" $\mathsf{succ}$: make a Church pair $(\lambda nsz. s (n\ s\ z), \text{<any-term>})$ and take its first component, i.e. $$ \mathsf{succ} = \mathsf{fst}\ (\mathsf{pair}\ (\lambda nsz. s (n\ s\ z))\ \text{<any-term>}), $$ or add $x+1$ to a number and subtract $x$, i.e. $$ \mathsf{succ} = \lambda n. \mathsf{minus}\ ((\mathsf{plus}\ n\ \mathsf{(x+1)})\ \mathsf{x}) $$

---

Now, let's address the $\mathsf{succ}\ (\mathsf{succ}\ 1)$ issue (I'm using the unrestricted evaluation strategy here): $$ \begin{array} \mathsf{succ}\ (\mathsf{succ}\ \mathsf{one}) &= \quad \text{(by definitions of succ and one)} \\ \mathsf{succ}\ ((\lambda nsz. s (n s z))\ (\lambda sz.s z)) &\to_{\beta} \\ \mathsf{succ}\ (\lambda sz. s ((\lambda sz.s z) s z)) &\to_{\beta}^{*} \\ \mathsf{succ}\ (\lambda sz. s (s z)) &= \quad \text{(by definition of succ)} \\ (\lambda nsz. s (n s z))\ (\lambda sz. s (s z)) &\to_{\beta} \\ (\lambda sz. s ((\lambda sz. s (s z))\ s z)) &\to_{\beta}^{*} \\ (\lambda sz. s (s (s z))) \end{array} $$ We've got a $\lambda$-term which clearly represents the number $3$ as was expected. If you try using $\lambda nsz. n s (s z)$ as the successor function you'll get the same result.

Under more restricted reduction strategy, viz. the call-by-value strategy, we sometimes get a term which doesn't look like a Church numeral at all, but behaves like one. A classical example is $$ \begin{array} \mathsf{succ}\ 1 &= \\ (\lambda nsz. s (n s z)) (\lambda sz. s z) &\to_{\beta} \\ \lambda sz. s ((\lambda sz. s z) s z) \end{array} $$

The result is behaviorally equivalent to $\lambda sz. s (s z)$.

---

Now I'm going to show that $(\mathsf{succ}\ \mathsf{succ})\ N$ is equivalent to Church numeral corresponding to $N(N+1)$. Then somewhat unintuitive term $(\mathsf{succ}\ \mathsf{succ})\ 1$ indeed evaluates to $2$.

$$\begin{array} \mathsf{succ}\ \mathsf{succ}\ N &= &\text{unfold the 1st succ}\\ (\lambda nsz. s (n s z))\ \mathsf{succ}\ N &\to_{\beta} \\ (\lambda sz. s (\mathsf{succ}\ s\ z))\ N &\to_{\beta} \\ \lambda z. N\ (\mathsf{succ}\ N\ z) &\to_{\beta}^{*} &\text{(apply succ to N)}\\ \lambda z. N\ (\{N+1\}\ z) &=_{\alpha} &\text{(rename z → s)} \\ \lambda s. N\ (\{N+1\}\ s) &= &\text{unfold {N+1}} \\ \lambda s. N\ ((\lambda tz'. t^{N+1}\ z')\ s) &\to_{\beta} \\ \lambda s. N\ (\lambda z'. s^{N+1}\ z') &= &\text{(unfold N)} \\ \lambda s. (\lambda tz. t^{N}\ z)\ (\lambda z'. s^{N+1}\ z') &\to_{\beta} \\ \lambda s. (\lambda z. (\lambda z'. s^{N+1}\ z')^{N}\ z) &= &\text{(syntactic sugar)} \\ \lambda sz. (\lambda z'. s^{N+1}\ z')^{N}\ z &\to_{\eta} &\text{(η-reduction)} \\ \lambda sz. (s^{N+1})^{N}\ z &= \\ \lambda sz. s^{N(N+1)}\ z &= \\ N(N+1) \end{array}$$