# Compatibility of $\beta$-reduction

In the Introduction to Lambda Calculus, on pages 23-24, the author introduces one-step $\beta$-reduction and $\beta$-reduction, which I write as $\to_1$ and $\to$ respectively (cannot find the symbols in the document on Detexify). In Definition 4.2(i), $\to_1$ is explicitly defined as a compatible (by 4.1) relation on $\Lambda$. Next $\to$ is defined, and below the author claims that "$\to$ is a compatible relation by definition".

But consider the requirement that $M \to N \implies ZM \to ZN$. How is this relation provable from the given definitions? For this, we would require to somehow use the similar property from $\to_1$, i.e., $X \to_1 Y \implies ZX \to_1 ZY$. The definitions for $A \to B$ provide no information of the form $(\ldots) \implies A' \to_1 B'$, so how is it possible for us to start from $M \to N$ and get back anything about $\to_1$ from just the definitions as axioms alone?

• $=_{\beta}$ and $\to_{\beta}$ and "\twoheadrightarrow_{\beta}" for $\twoheadrightarrow_{\beta}$... – Mauro ALLEGRANZA Dec 20 '17 at 14:15
• As $\twoheadrightarrow_{\beta}$ is defined inductively, use a proof by induction. Base cases are for $M\twoheadrightarrow_{\beta} M$ and $M\to_\beta N\implies M\twoheadrightarrow_{\beta} N$ parts of the definition; inductive step is for the last. In other words, “inductive definition” means $M\twoheadrightarrow_{\beta} N$ iff there is a proof of this from axioms 1, 2 with an inference rule 3. – arseniiv Dec 20 '17 at 14:55
• "$M \twoheadrightarrow_\beta N$ iff there is a proof of this from the axioms 1,2 and inference rule 3".-Okay, this explains it. I was confused because $M \twoheadrightarrow_\beta N$ was not properly defined in an "if and only if" sense, but only some properties were listed. I guess, based on your statement, I could write a proof like $M \twoheadrightarrow_\beta N \implies$ there is a proof of this from the axioms $\implies$ for some $n \geq 0$, there are $n$ arrows like $M \to_\beta M_1 \to_\beta \ldots \to_\beta N$, and do induction on $n$ right? Thanks! Could you please make this an answer? – Mriganka Basu Roy Chowdhury Dec 20 '17 at 15:04
• @Koyomi-chan It’s right, and yes I will quite soon, if you or someone else won’t write it earlier. :) – arseniiv Dec 20 '17 at 15:09

As I promote my comment to an answer, I’d considered it useful to digress into structural induction a bit in the middle.

So, if there is an inductive definition of some relation $R$ with a set of clauses of form $$\phi\wedge R(t_1)\wedge\ldots\wedge R(t_n)\Rightarrow R(t),\qquad{(*)}$$ where $\phi$ doesn’t contain any $R$s, then it means cases $R(x)$ holds are precisely those which could be obtained by a proof, using clauses of the definition as inference rules $\frac{\phi\quad R(t_1)\quad\cdots\quad R(t_n)}{R(t)}$.

With this, a structural induction comes in handy: to prove claim $\forall x.\;R(x)\Rightarrow A(x)$, it’s sufficient to prove, for each definition clause $(*)$, that $\phi\wedge A(t_1)\wedge A(t_2)\wedge\ldots\wedge A(t_n)\Rightarrow A(t)$, where $t_1,\ldots,t_n,t$ are exactly what they are in that clause.

This kind of induction is founded on ordinary mathematical induction for $\mathbb N$ applied with respect to proof length/depth, and it’s less verbose to justify it once somewhere, and then use it all the way instead—as I’ll do below.

In your case, we have clauses

C1. $M\twoheadrightarrow_{\beta} M$;

C2. $M\to_\beta N\Rightarrow M\twoheadrightarrow_{\beta} N$;

C3. $M\twoheadrightarrow_{\beta} N\wedge N\twoheadrightarrow_{\beta} L\Rightarrow M\twoheadrightarrow_{\beta} L$.

The structural induction proof of compatibility of $\twoheadrightarrow_{\beta}$ then is as follows:

1. Show that $ZM\twoheadrightarrow_{\beta} ZM$, $MZ\twoheadrightarrow_{\beta} MZ$, $(\lambda x.M)\twoheadrightarrow_{\beta} (\lambda x.M)$.

C1 three times, done.

2. Show that, if $M\to_\beta N$, then $ZM\twoheadrightarrow_{\beta} ZN$, $MZ\twoheadrightarrow_{\beta} NZ$, $(\lambda x.M)\twoheadrightarrow_{\beta} (\lambda x.N)$.

By compatibility of $\to_\beta$, we’ve got $ZM\to_\beta ZN$, $MZ\to_\beta NZ$, $(\lambda x.M)\to_\beta (\lambda x.N)$. Applying C2 to these, we’re done with this case.

3. (Now we actually have premises with $\twoheadrightarrow_{\beta}$ in them, hooray!) Show that, if

(a) $ZM\twoheadrightarrow_{\beta} ZN$, $MZ\twoheadrightarrow_{\beta} NZ$, $(\lambda x.M)\twoheadrightarrow_{\beta} (\lambda x.N)$, and

(b) $ZN\twoheadrightarrow_{\beta} ZL$, $NZ\twoheadrightarrow_{\beta} LZ$, $(\lambda x.N)\twoheadrightarrow_{\beta} (\lambda x.L)$, then

(c) $ZM\twoheadrightarrow_{\beta} ZL$, $MZ\twoheadrightarrow_{\beta} LZ$, $(\lambda x.M)\twoheadrightarrow_{\beta} (\lambda x.L)$.

Here we apply C3 for corresponding statements of (a) and (b) to get each statement of (c).

And that’s it, now we know for sure $\beta$-reduction is compatible! (Well, I liked a sketch in your comment more, but for the sake of clarity, this all had to be done.)

• I like this answer very much, as it contains a lot of details the text skips. I have a question. Does the fact that $R(x)$ is satisfied for precisely those $x$ for which it can demonstrated by a proof using the inference rules, implicitly assume that the proof consists of finitely many steps ? Otherwise, my assumption about the existence of $n$ steps of $\to_\beta$ fails. – Mriganka Basu Roy Chowdhury Dec 20 '17 at 19:26
• Yes, the proof should have fiitely many steps (as is common to various other proofs :). – arseniiv Dec 20 '17 at 19:40