This is the first post in the PLT section. It is concerning the Untyped/Simply-Typed Lambda Calculus, and an important result stemming from a foundational Theorem in $\lambda$ and $\lambda \to$.

I already assume the reader has knowledge of the syntax of the Untyped Lambda Calculus and Simply-Typed Lambda Calculus. I also assume that the reader is familiar with the notions of $\beta$-reduction, $\alpha$-equivalence and substitution.

The post is (unfortunately for the reader), a very lengthy post about an alternative proof of a Corollary to the Church-Rosser Theorem, that I thought of.

NOTE : I shall use ${\to }_{\beta }$ to refer to both, chained AND singular $\beta$-reductions.

Let’s just begin by stating the Church-Rosser Theorem and the definition of ${=}_{\beta }$. It’s elegant to see that the Church-Rosser Theorem holds for $\lambda$ and $\lambda \to$.

Church-Rosser Theorem : Given a legal-term $M\in \Lambda$, $\ni ,\left(M{\to }_{\beta }{M}_0\right)\wedge \left(M{\to }_{\beta }{M}_1\right)$, $\exists N\in \Lambda$, $\ni ,\left(M_0{\to }_{\beta }N\right)\wedge \left(M_1{\to }_{\beta }N\right)$.

Proof : Various proofs for this Theorem have been presented over the years. The most succinct one I know of is presented by Takahashi in 1995, using an Algebraic basis. A more standard proof is presented by Barendregt in his book : The Lambda Calculus. Its Syntax and Semantics (Studies in Logic).

I shall not discuss the proof here, and we shall assume that the Theorem is already true for future reference in this post.

Definition (${=}_{\beta }$) : Two terms $M,N$ are said to be $M{=}_{\beta }N$, if :

i) $M_0\equiv M$, $M_n\equiv N$

ii) $\exists n\in \mathbb{N},\ni ,\left(M_i{\to }_{\beta }{M}_{i+1}\right)\vee \left(M_i{\leftarrow }_{\beta }{M}_{i+1}\right),\forall i\in [1,n]$

All this definition is saying is that if two terms can reach some common Lambda-Term by some sequence of bi-directional $\beta$-reductions, they are equivalent.

The Corollary to this theorem (the main concern of this post), is actually a very important statement.

Corollary : Given two terms $M,N\in \Lambda ,\ni ,M{=}_{\beta }N$, we have that, $\exists L\in \Lambda ,\ni ,\left(M{\to }_{\beta }L\right)\wedge \left(N{\to }_{\beta }L\right)$.

Plan : The proof to the Corollary presented by Nederpelt & Geuvers in their text Type Theory And Formal Proof in Chapter 1, Pg 22-23 uses Induction.

While the proof is succinct (as with most proofs using induction), I feel it does not really give a full understanding of how exactly the $L$ term is constructed. Nor does it, in my opinion, allow us to get an intuitive grasp on the structure of evaluation paths for two terms that are $\beta$-equivalent. Nonetheless, I shall first briefly expose their proof, and then move on to mine.

Proof (Nederpelt & Geuvers) : The Theorem is essentially saying that if two terms are $\beta$-equivalent, then we can find a common redex for them. As stated, the text takes the inductive approach, which goes as follows :

Base Case : Assume $i=0$. Then, $M=M_0=N$, and the Theorem is true.

Inductive Hypothesis : Assume that, $\forall i<n$, the Theorem holds true.

Inductive Case : There are actually 2 cases we need to prove here.

Case 1 : $M_{n-1}{\to }_{\beta }{M}_n$

In this case, the Evaluations look as follows :

$M\equiv M_0$ .... $M_{n-1}{\to }_{\beta }{M}_n\equiv N$

Notice that, as the IH applies to $M_{n-1}$ (because $n-1<n$, and, $M_0{=}_{\beta }{M}_{n-1}$), we have that, $\exists L^{{}^{\text{'}}},\ni ,\left(M{\to }_{\beta }{L}^{{}^{\text{'}}}\right)\wedge \left(M_{n-1}{\to }_{\beta }{L}^{{}^{\text{'}}}\right)$.

This now tells us that $\exists$ 2 terms that $M_{n-1}$ $\beta$-reduces to ($M_{n-1}{\to }_{\beta }{L}^{{}^{\text{'}}}$ and $M_{n-1}{\to }_{\beta }N$), lending itself vulnerable to the Church-Rosser Theorem.

This implies, $\exists L\in \Lambda ,\ni ,\left(L^{{}^{\text{'}}}{\to }_{\beta }L\right)\wedge \left(M_n{\to }_{\beta }L\right)$.

And this is all we need, as we can use the transitivity of $\beta$-reductions to compose the reduction from $M_0$ as : $M_0{\to }_{\beta }{L}^{{}^{\text{'}}}{\to }_{\beta }L$.

So, $\left(M_0{\to }_{\beta }{L}^{{}^{\text{'}}}{\to }_{\beta }L\right)\wedge \left(M_n{\to }_{\beta }L\right)$.

Case 2 : $M_{n-1}{\leftarrow }_{\beta }{M}_n$

In this case, the Evaluations look as follows :

$M\equiv M_0$ .... $M_{n-1}{\leftarrow }_{\beta }{M}_n\equiv N$

This case is actually even easier to see.

By IH on $M_{n-1}$, we construct:

$L^{{}^{\text{'}}},\ni ,\left(M{\to }_{\beta }{L}^{{}^{\text{'}}}\right)\wedge \left(M_{n-1}{\to }_{\beta }{L}^{{}^{\text{'}}}\right)$. This actually completes the proof, because, now we have :

$\left(M_0{\to }_{\beta }{L}^{{}^{\text{'}}}\right)\wedge \left(L^{{}^{\text{'}}}{\leftarrow }_{\beta }{M}_{n-1}{\leftarrow }_{\beta }{M}_n\right)$.

Clearly, in this case, $L^{{}^{\text{'}}}=L$.

Q.E.D.

Proof 2 : Now, we move on to the method that I thought of, which is more tedious, yet far more informative. It also does not rely on induction. This method only requires the assumption of the Church-Rosser Theorem.

Let us first eliminate the 2 trivial cases, so that we can focus on the most generic case.

Case 1 : $M\equiv M_0{\to }_{\beta }{M}_1{\to }_{\beta }....{\to }_{\beta }$ $M_{n-1}{\to }_{\beta }{M}_n\equiv N$

This is the case in which all reductions are right-arrows. So, $M{\to }_{\beta }N\equiv L$

Case 2 : $M\equiv M_0{\leftarrow }_{\beta }{M}_1{\leftarrow }_{\beta }....{\leftarrow }_{\beta }$ $M_{n-1}{\leftarrow }_{\beta }{M}_n\equiv N$

This is the case in which all reductions are left-arrows. So, $L\equiv M{\leftarrow }_{\beta }N$

Case 3 : This is the final, and most generic case. While, technically, there are 4 of these that we should deal with, we’ll only deal with 2, as it will become apparent that symmetry will deal with the others the same as we deal with the first two. So, let’s first try to express $\beta$-equivalence in a way that is useful diagrammatically. As $\beta$-equivalence has a switching between right-arrows and left-arrows, there are terms that "switch" the direction in the Equivalence Set. Such terms are either sources of sinks (with the terms having the standard Graph-Theoretic meaning).

Therefore, one may rewrite a general equivalence diagram for $M{=}_{\beta }N$ in one of two ways (assuming that the first reduction on $M_0$ is a right-arrow) :

i) $M\equiv M_0{\to }_{\beta }$ ... ${\to }_{\beta }{M}_{i_1}{\leftarrow }_{\beta }$ ... ${\leftarrow }_{\beta }{M}_{i_2}{\to }_{\beta }$ ... ${\to }_{\beta }{M}_{i_{k_1}}{\leftarrow }_{\beta }$ ... ${\leftarrow }_{\beta }{M}_n\equiv N$

ii) $M\equiv M_0{\to }_{\beta }$ ... ${\to }_{\beta }{M}_{i_1}{\leftarrow }_{\beta }$ ... ${\leftarrow }_{\beta }{M}_{i_2}{\to }_{\beta }$ ... ${\leftarrow }_{\beta }{M}_{i_{k_2}}{\to }_{\beta }$ ... ${\to }_{\beta }{M}_n\equiv N$

Proof (i) : We can see that $\forall j\in {\mathbb{Z}}_{\mathrm{𝕖𝕧𝕖𝕟}}$, $M_{i_j}$ is a source. While, $\forall j\in {\mathbb{Z}}_{\mathrm{𝕠𝕕𝕕}}$, $M_{i_j}$ is a sink. As $M_{k_1}$ is a sink, we have that, $k_1$ is odd. As $M_{i_{even}}$ are sources, their neighboring sinks form 2 redexes that reduce to a common term by virtue of the Church-Rosser Theorem. More specifically :

$\forall (M_{i_{k-1}},M_{i_k},M_{i_{k+1}})$, where, $k$ is even (and $M_k$ a source), $\exists L_k^{{}^{\text{'}}}$, $\ni \left(M_{i_{k-1}}{\to }_{\beta }{L}_k^{{}^{\text{'}}}\right)\wedge \left(M_{i_{k+1}}{\to }_{\beta }{L}_k^{{}^{\text{'}}}\right)$.

This creates a set of terms ${\Lambda }^{{}^{\text{'}}}=\{L{{}^{\text{'}}}_2,L_4^{{}^{\text{'}}},..,L_{k_1-1}^{{}^{\text{'}}}\}$.

Now, because of the "sliding-window" that creates these terms, each of these has 2 parents, and each of the parents (excluding the first sink ($M_{i_1}$) and last sink ($M_{i_{k_1}}$)), have 2 children.

NOTE : $M_{i_1}$ and $M_{i_{k_1}}$ only have 1 children, the first and last term in ${\Lambda }^{{}^{\text{'}}}$.

As a result, we can apply the Church-Rosser Theorem again to all these parents. More precisely :

$\forall M_{i_{2p+1}}$, for $p\in \{1,\frac{(k_1-1)}{2}\}$ , $\exists ,L_{2p}^{{}^{\text{'}}}$ and $L_{2(p+1)}^{{}^{\text{'}}}$ , $\ni \left(M_{i_{2p+1}}{\to }_{\beta }{L}_{2p}^{{}^{\text{'}}}\right)\wedge \left(M_{i_{2p+1}}{\to }_{\beta }{L}_{2(p+1)}^{{}^{\text{'}}}\right)$. Therefore, by the Church-Rosser Theorem, we have that :

There is a set of terms ${\Lambda }^{{}^{\text{'}\text{'}}}=\{L_2^{{}^{\text{'}\text{'}}},L_4^{{}^{\text{'}\text{'}}},...,L_{k_1-3}^{{}^{\text{'}\text{'}}}\}$, where,

$\left(L_j^{{}^{\text{'}}}{\to }_{\beta }{L}_j^{{}^{\text{'}\text{'}}}\right)\wedge \left(L_{j+2}^{{}^{\text{'}}}{\to }_{\beta }{L}_j^{{}^{\text{'}\text{'}}}\right)$, where, $j\in \{2,4,...,(k_1-1)\}$

As one can see ${\Lambda }^{{}^{\text{'}\text{'}}}$ has 1 term less than ${\Lambda }^{{}^{\text{'}}}$.

We can continue to apply the Church-Rosser Theorem recursively, as now, the terms in ${\Lambda }^{{}^{\text{'}}}$ have 2 children each (except for $L_2^{{}^{\text{'}}}$ and $L_{k_1-1}^{{}^{\text{'}}}$).

In fact, this general pattern will hold, where, each ${\Lambda }^{{}^{\text{'}}\left(j\right)}$ set will continue to collapse by one, until at last there is only term in there. This term is the redex we are looking for. This redex is : $L_2^{{}^{\text{'}}\left(\frac{k_1}{2}\right)}$, where the notation of ${}^{{}^{\text{'}}\left(m\right)}$ indicates the term belongs to the $m-th$ Lambda Set on the way down. So, we have :

$(M\equiv M_0{\to }_{\beta }{M}_{i_1}{\to }_{\beta }{L}_2^{{}^{\text{'}}}{\to }_{\beta }{L}_2^{{}^{\text{'}\text{'}}}$ ... ${\to }_{\beta }{L}_2^{{}^{\text{'}}\left(\frac{k_1}{2}\right)})\wedge (N\equiv M_n{\to }_{\beta }{M}_{k_1}{\to }_{\beta }{L}_{k_1-1}^{{}^{\text{'}}}{\to }_{\beta }{L}_{k_1-3}^{{}^{\text{'}\text{'}}}$ ... ${\to }_{\beta }{L}_2^{{}^{\text{'}}\left(\frac{k_1}{2}\right)})$.

Proof (ii) : The second case is similar, differing in only that :

a) $k_2$ is even, as it is a source.

b) The last term in the equivalence-set, $M_n$ has a direct redex that takes it to the final term : ($N\equiv M_n{\to }_{\beta }{L}_{k_2}^{{}^{\text{'}}}{\to }_{\beta }{L}_{k_2-2}^{{}^{\text{'}\text{'}}}$ ... ${\to }_{\beta }{L}_2^{{}^{\text{'}}\left(\frac{k_1}{2}\right)}$).

The path from the first term remains the same.

It is also easy to see that in the 2 cases that follow when the first reduction is a ${\leftarrow }_{\beta }$, we can use symmetry to invert the paths and construct the redex we want.

Q.E.D.

As one can see, this proof is constructive as it explicitly creates this term (without using induction). Furthermore, this proof is better because it also gives an idea of the Complexity of evaluating this term given the ability to compute chained $\beta$-reductions.

- The height of the "Diamond" Graph is : $1+{\sum }_{h=1}^{\frac{k}{2}}(\frac{k}{2}-h)=1+\frac{k}{2}$

- In the formula above (and below), k is the number of "switches" in the Equivalence Set. Furthermore, this graph is not a Tree, it is a DAG.

- Also, in the worst case, the number of nodes in this Graph are :

$\left|V\right|=\left({\sum }_{h=1}^{\frac{k}{2}}(1+h)\right)+n=\left(\frac{k}{2}\right)(\frac{k}{2}-1)+n$

So, there you have it, a constructive proof to a very important corollary to the Church-Rosser Theorem.