1
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ $=_{\beta}$ and $\to_{\beta}$ and "\twoheadrightarrow_{\beta}" for $\twoheadrightarrow_{\beta}$... $\endgroup$ – Mauro ALLEGRANZA Dec 20 '17 at 14:15
  • 1
    $\begingroup$ 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. $\endgroup$ – arseniiv Dec 20 '17 at 14:55
  • $\begingroup$ "$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? $\endgroup$ – Mriganka Basu Roy Chowdhury Dec 20 '17 at 15:04
  • 1
    $\begingroup$ @Koyomi-chan It’s right, and yes I will quite soon, if you or someone else won’t write it earlier. :) $\endgroup$ – arseniiv Dec 20 '17 at 15:09
1
$\begingroup$

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.)

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Mriganka Basu Roy Chowdhury Dec 20 '17 at 19:26
  • 1
    $\begingroup$ Yes, the proof should have fiitely many steps (as is common to various other proofs :). $\endgroup$ – arseniiv Dec 20 '17 at 19:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.