3
$\begingroup$

I am reading Lectures on the Curry-Howard Isomorphism by Sorensen and Urzyczyn, and I got stuck when trying to fill in the details of Lemma 1.2.12(2). Below is the statement of Lemma 1.2.12.

Lemma 1.2.12.

  1. For all pre-terms $M,N$ and all variable $x$, there exists a pre-term $M'$ such that $M =_\alpha M'$ (i.e., $M$ is $\alpha$-equivalent to $M'$) and the substitution $M'[x := N]$ is defined.
  2. For all pre-terms $M,N,P$ and all variables $x,y$, there exist $M',N'$ such that $M =_\alpha M'$, $N =_\alpha N'$, and the substitutions $M'[x := N']$ and $M'[x := N'][y := P]$ are defined.

The proof of Lemma 1.2.12(1) is a simple induction on $M$. However, Lemma 1.2.12(2) seems much more complicated. Sorensen and Urzyczyn claim that Lemma 1.2.12(2) can also be easily solved by a straightforward induction on $M$, but I do not see how this works for application.

Let us assume that $M = AB$, where $A,B$ are pre-terms. By the induction hypothesis on $A$, there exist $A',N_1'$ such that $A =_\alpha A'$, $N =_\alpha N_1'$, and the substitutions $A'[x := N_1']$ and $A'[x := N_1'][y := P]$ are defined. Similarly, by the induction hypothesis on $B$, there exist $B',N_2'$ such that $B =_\alpha A'$, $N =_\alpha N_2'$, and the substitutions $B'[x := N_2']$ and $B'[x := N_2'][y := P]$ are defined. If $N_1' = N_2'$, then we could define $M' = A'B'$ and $N' = N_1' = N_2'$, and we would be done. But it is clear that one can construct an example here where $N_1' \ne N_2'$.

What elements should we add to the proof to ensure that $N_1' = N_2'$, or more generally, what is the correct way to prove Lemma 1.2.12(2)?

$\endgroup$
1
  • $\begingroup$ What is the definition of a pre-term? What does it mean that "the substitution $M[N/x]$ is defined"? $\endgroup$ Commented Dec 31, 2024 at 6:05

1 Answer 1

Reset to default
1
$\begingroup$

An alternative solution goes as follows. Let $\mathcal V$ be the (infinite) set of all variables, and $V \subset \mathcal V$ a finite subset. Define $B_V(-)$ by induction on pre-terms: $$\begin{aligned} B_V(x) & := x \\ B_V(MN) & := B_V(M) B_V(N) \\ B_V(λx.M) & := λy.B_{V \cup \{y\}}(M[x \leftarrow y]) \end{aligned}$$ where, in the last case, $y$ is a fresh variable (i.e. it appears neither in $V$ nor in $M$), and the renaming $M[x \leftarrow y]$ is well-defined because $y$ is fresh — in particular it does not appear bound in $M$.

We have $M =_α B_V(M)$ and $V \cap \mathrm{bv}(B_V(M)) = \emptyset$. In particular, $B_{\mathrm{fv}(M)}(M)$ satisfies Barendregt's convention: it has disjoint sets of free and bound variables.

You can use this in your lemma, by setting $V := \mathrm{fv}(N) \cup \mathrm{fv}(P)$, and then $M' := B_V(M)$ and $N' := B_V(N)$. You get:

  • $\mathrm{fv}(N') \cap \mathrm{bv}(M') = \emptyset$, so the substitution $M'[N'/x]$ is defined.
  • $\mathrm{fv}(P) \cap \mathrm{bv}(M'[N'/x]) \subseteq \mathrm{fv}(P) \cap (\mathrm{bv}(M') \cup \mathrm{bv}(M')) = \emptyset$, so the substitution $M'[N'/x][P/y]$ is defined.

This technique is more general than an ad hoc induction, because Barendregt's convention allows to define substitution in general (see Berendregt's book).

Yet another option is to use Krivine's definition of α-equivalence, which makes many things easier in the end. It seems weird at first, but in my opinion it is the most canonical definition (because it is tightly related to the abstract presentation of α-equivalence via nominal sets).

$\endgroup$

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.