1
$\begingroup$

$\newcommand{\abstraction}[2]{\lambda #1. #2}$ $\newcommand{\application}[2]{\left(#1 #2\right)}$ $\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$ $\newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\closedlambdaset}{\Lambda^{0}}$ $\newcommand{\lambdaexprswithfreevars}[1]{\closedlambdaset\left(#1\right)}$ $\newcommand{\subterm}[1]{\operatorname{Sub}\left(#1\right)}$ $\newcommand{\vars}[1]{\operatorname{Var}\left(#1\right)}$ $\newcommand{\context}[2]{{#1}\left[#2\right]}$ $\newcommand{\hole}{\ }$

Barendregt defines a binary relation $R$ on the set of lambda terms $\Lambda$ to be compatible if $$\begin{align} \left(M,M'\right) \in R \implies &\left(\application{Z}{M}, \application{Z}{M'} \right) \in R,\\ & \left( \application{M}{Z}, \application{M'}{Z} \right) \in R, \text{ and }\\ &\left( \abstraction{x}{M}, \abstraction{x}{M'} \right) \in R \end{align} $$ for all $M,M',Z \in \Lambda$. Call this Statement 1.

I'm understanding that this condition is required to somehow "preserve" the syntactic structure of a (potentially complicated) term being reduced under a notion of reduction in the system.

The author later comments that a relation $R \subseteq \Lambda^2$ is compatible if $$\left(M,M'\right) \in R \implies \left( \context{C}{M}, \context{C}{M'} \right) \in R$$ for all $M,M' \in \Lambda$ and all contexts $\context{C}{}$ with one hole. Call this Statement 2.

The proofs that follow in the book all use induction over the structure of contexts using Statement 2 instead of the former. Indeed, all other references I found online use Statement 2 (with some minor variations) as the definition for a relation to be compatible. So I'm trying to prove they are equivalent statements: given one statement as a definition, the other follows.

My rational is as follows for given Statement 2 as a definition, it follows that Statement 1 is true.

The same reference defines a context inductively by:

  1. $x$ is a context — I have seem some controversy about this one on other answers here, but this is how it is defined in the reference;
  2. $\context{}{}$ is a context;
  3. if $\context{C_1}{}$ and $\context{C_2}{}$ are contexts, then so is $\application{\context{C_1}{}}{\context{C_2}{}}$.
  4. if $\context{C_1}{}$ is a context, then so is $\abstraction{x}{\context{C_1}{}}$.

The contexts with one hole can only be (*)

  1. $\context{}{}$;
  2. $\application{Z}{\context{}{}}$ — coming from case 3 above and choosing $\context{C_1}{} \equiv Z$ and $\context{C_2}{} \equiv \context{}{}$.
  3. $\application{\context{}{}}{Z}$ — coming from case 3 above and choosing $\context{C_1}{} \equiv \context{}{}$ and $\context{C_2}{} \equiv Z$.;
  4. $\abstraction{x}{\context{}{}}$ — coming from case 4 above and choosing $\context{C_1}{} \equiv \context{}{}$.;

because otherwise the inductive nature of the context definition as given would create more than one hole. Also, the case $x$ has no holes.

Then, the three implications follow immediately from the substitution of cases 2, 3, and 4 above, together with $(M,M') \in R \implies (M,M') \in R$ from the first case which is (obviously?) true from the structure of the statement.

The converse would be in the lines of:

Given $\left(M,M'\right) \in R \implies \left(\application{Z}{M}, \application{Z}{M'} \right) \in R$ choose $\context{C}{} \equiv \application{Z}{\context{}{}}$ and it follows that $\left(M,M'\right) \in R \implies \left( \context{C}{M}, \context{C}{M'} \right) \in R$. Similarly for the other cases. Together they would cover all cases of contexts with one hole and thus the condition of statement 2.

It took me quite some time to perceive the importance of the restriction with one hole in Statement 1 (Barendregt's original definition).

Is this a correct way to prove the equivalence between the mentioned statements or I am missing something here?

What bothers me is that in (*) there are actually infinitely many contexts with one hole that can be generated from the rules (e.g. $\application{Z}{\application{A}{\context{}{}}}$ or $\abstraction{x}{\application{Z}{\context{}{}}}$).

$\endgroup$
1
  • $\begingroup$ As an example of Statement 2 being used as the definition for a compatible relation: math.stackexchange.com/q/4337463 $\endgroup$ Commented Jan 19, 2023 at 22:38

1 Answer 1

Reset to default
-1
$\begingroup$

$\newcommand{\abstraction}[2]{\lambda #1. #2}$ $\newcommand{\application}[2]{\left(#1 #2\right)}$ $\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$ $\newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\closedlambdaset}{\Lambda^{0}}$ $\newcommand{\lambdaexprswithfreevars}[1]{\closedlambdaset\left(#1\right)}$ $\newcommand{\subterm}[1]{\operatorname{Sub}\left(#1\right)}$ $\newcommand{\vars}[1]{\operatorname{Var}\left(#1\right)}$ $\newcommand{\context}[2]{{#1}\left[#2\right]}$ $\newcommand{\hole}{\ }$

Your approach ("given Statement 2 as a definition, it follows that Statement 1 is true") is correct. But there are some mistakes in the way you "implemented".

The contexts with one hole can only be ($*$)

  1. $\context{}{}$;
  2. $\application{Z}{\context{}{}}$ — coming from case 3 above and choosing $\context{C_1}{} \equiv Z$ and $\context{C_2}{} \equiv \context{}{}$.
  3. $\application{\context{}{}}{Z}$ — coming from case 3 above and choosing $\context{C_1}{} \equiv \context{}{}$ and $\context{C_2}{} \equiv Z$.;
  4. $\abstraction{x}{\context{}{}}$ — coming from case 4 above and choosing $\context{C_1}{} \equiv \context{}{}$.

because otherwise the inductive nature of the context definition as given would create more than one hole.

This is false! As you noticed, $\application{Z}{\application{A}{\context{}{}}}$ or $\abstraction{x}{\application{Z}{\context{}{}}}$ are context with exactly one hole, and they do not fit in $(*)$. The correct definition of contexts with exactly one hole is the following:

The contexts with one hole can only be ($**$)

  1. $\context{}{}$;
  2. $\application{Z\,}{\context{C\!}{}}$ — coming from case 3 above and choosing $\context{C_1\!}{} \equiv Z$ and $\context{C_2\!}{} \equiv \context{C\!}{}$ with exactly one hole.
  3. $\application{\context{C\!}{}}{Z}$ — coming from case 3 above and choosing $\context{C_1\!}{} \equiv \context{C\!}{}$ with exactly one hole, and $\context{C_2\!}{} \equiv Z$.;
  4. $\abstraction{x}{\context{C\!}{}}$ — coming from case 4 above and choosing $\context{C_1\!}{} \equiv \context{C\!}{}$ with exactly one hole.

Note that $\application{Z}{\application{A}{\context{}{}}}$ or $\abstraction{x}{\application{Z}{\context{}{}}}$ fit in ($**)$. Barendregt's definition of compatibility uses the notion of context in ($**$) and not the one in ($*$). Hence, what you have to prove is that "given Statement 2 as a definition (based on ($**$) and not on ($*$)), it follows that Statement 1 is true". Do you see how to prove it?

[...] together with $(M,M') \in R \implies (M,M') \in R$ from the first case which is (obviously?) true from the structure of the statement.

This is false! Unless otherwise stated, a binary relation $R$ need not be symmetric. For instance, $\beta$-reduciton $\to_\beta$ (defined on Barendregt's textbook you cited) is the typical example of a non-symmetric binary relation. Indeed, $(\lambda x.xx) z \to_\beta zz$ but $zz \not \to_\beta (\lambda x.xx) z$.

$\endgroup$
2
  • $\begingroup$ Thanks. I see now that (*) has to be corrected as you pointed. I'm still stuck as Statement 2 seem to generate more general implications than Statement 1. For instance, case 2 of (**) would generate $(M,M') \in R \implies \left(Z C \left[ M \right], Z C \left[ M' \right] \right) \in R$ and I can't see how to reduce this to one of the claims in Statement 1 via the induction hypothesis or other way. Claiming that $C\left[M\right] \in \Lambda$ and $C\left[M'\right] \in \Lambda$ is sufficient to fit it in the first implication of Statement 1 and conclude this part of the argument? $\endgroup$ Commented Jan 20, 2023 at 14:49
  • $\begingroup$ For the second part of the comment, I thought $\left(M,M'\right) \in R \implies \left(M,M'\right) \in R$ would be a tautology. It's the same as $aRb \implies aRb$ and not $aRb \implies bRa$ which would be the case for symmetry. If it's not the case, I can't see also how to deal with case 1 of (**). Thanks for the help here. From my CS background I can "feel" the two presentations are equivalent but I'm studying to this realm of formal proofs and program verification which require well developed arguments. $\endgroup$ Commented Jan 20, 2023 at 15:06

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.