0
$\begingroup$

I am going through Lemma 1.2.11 of "Lectures on the Curry-Howard Isomorphism" by Morten Heine Sørensen and Pawel Urzyczyn. There is a free sample that includes this lemma here: https://play.google.com/store/books/details?id=_mtnm-9KtbEC

1.2.11 Lemma. If $M =_{\alpha} M'$ and $N =_{\alpha} N'$ then $M [ x := N ] =_{\alpha} M' [ x := N' ]$, provided that both sides are defined.

PROOF. By induction on the definition of $M =_{\alpha} M'$. If $M = M'$ then proceed by induction on $M$. The only other interesting case is when we have $M = \lambda z P$ and $M' = \lambda y . P [ z := y ]$, where $y \notin FV ( P )$, and $P [ z := y ]$ is defined. If $x = z$, then $x \notin FV ( M ) = FV ( M' )$ by Lemma 1.2.10. Hence $M [ x := N ] = M =_{\alpha} M' = M' [ x := N' ]$ by Lemma 1.2.5. The case $x = y$ is similar. So assume $x \notin \{ y, z \}$. Since $M [ x := N ]$ is defined, $x \notin FV ( P )$ or $z \notin FV ( N )$. In the former case $M [ x := N ] = \lambda z P$ and $x \notin FV ( P [ z := y ] )$, so $M' [ x := N' ] = \lambda y . P [ z := y ] =_{\alpha} \lambda z . P$.

It remains to consider the case when $x \in FV ( P )$ and $z \notin FV ( N )$. Since $M' [ x := N' ] = ( \lambda y . P [ z := y ] ) [ x := N' ]$ is defined, we have $y \notin FV ( N' )$, and thus also $y \notin FV ( P [ x := N' ] )$. By Lemma 1.2.6 it then follows that $M' [ x := N' ] = \lambda y . P [ z := y ] [ x := N' ] = \lambda y . P [ x := N' ] [ z := y ] =_{\alpha} [ z . P [ x := N' ]$. By the induction hypothesis $\lambda z . P [ x := N' ] =_{\alpha} \lambda z . P [ x := N ] = M [ x := N ]$.

I believe that $[ z . P [ x := N' ]$ is a misprint of $\lambda z . P [ x := N' ]$.

Referenced lemmas:

1.2.5. Lemma.

(i) If $x \notin FV ( M )$ then $M [ x := N ]$ is defined, and $M [ x := N ] = M$.

(ii) If $M [ x := N ]$ is defined then $y \in FV ( M [ x := N ] )$ if and only if either $y \in FV ( M )$ and $x \neq y$ or both $y \in FV ( N )$ and $x \in FV ( M )$.

(iii) The substitution $M [ x := x ]$ is defined and $M [ x := x ] = M$.

(iv) If $M [ x := y ]$ is defined, then $M [ x := y ]$ is of the same length as $M$.

1.2.6 Lemma. Assume that $M [ x := N ]$ is defined, and both $N [ y := L ]$ and $M [ x := N ] [ y := L ]$ are defined, where $x \neq y$. If $x \notin FV ( L )$ or $y \notin FV ( M )$ then $M [ y := L ]$ is defined, $M [ y := L ] [ x := N [ y := L ] ]$ is defined, and $M [ x := N ] [ y := L ] = M [ y := L ] [ x := N [ y := L ] ]$.

1.2.10 Lemma. If $M =_{\alpha} N$ then $FV ( M ) = FV ( N )$.

Substitution is defined as in this question: Formal definition of substitution being defined in type free lambda calculus

Alpha conversion is defined as:

The relation $=_{\alpha}$ ($\alpha$-conversion) is the least (i.e. smallest) transitive and reflexive relation on $\Lambda^{-}$ satisfying the following.

  • If $y \notin FV ( M )$ and $M [ x := y ]$ is defined then $\lambda x M =_{\alpha} \lambda y . M [ x := y ]$.

  • If $M =_{\alpha} N$ then $\lambda x M =_{\alpha} \lambda x N$, for all variables $x$.

  • If $M =_{\alpha} N$ then $MZ =_{\alpha} NZ$.

  • If $M =_{\alpha} N$ then $ZM =_{\alpha} ZN$.

I think that the case in question can be stated as:

H1. Let $P \in \Lambda^{-}$.

H2. Let $y$ be any variable.

H3. Let $z$ be any variable.

H4. Let $y \notin FV ( P )$.

H5. Let $P [ z := y ]$ be defined.

H6. Let $x$ be any variable.

H7. Let $N \in \Lambda^{-}$.

H8. Let $N' \in \Lambda^{-}$.

H9. Let $N =_{\alpha} N'$.

H10. Let $( \lambda z . P ) [ x := N ]$ be defined.

H11. Let $( \lambda y. P [ z := y ] ) [ x := N' ]$ be defined.

Prove: $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N']$.

If this is the case then I have:

T1. $( \lambda z . P ) =_{\alpha} ( \lambda y. P [ z := y ] )$ by H1 - H5 and the definition of $\alpha$-conversion.

T2. $FV ( ( \lambda z . P ) ) = FV ( ( \lambda y. P [ z := y ] ) )$ by T1 and Lemma 1.2.10.

T3. $FV ( N ) = FV ( N' )$ by H9 and Lemma 1.2.10.

A1. Let $x = z$.

A1-T1. $z \notin FV ( P ) - \{ z \}$.

A1-T2. $FV ( P ) - \{ z \} = FV ( ( \lambda z . P ) )$.

A1-T3. $x \notin FV ( ( \lambda z . P ) )$ by A1, A1-T1, and A1-T2.

A1-T4. $x \notin FV ( ( \lambda y . P [ z := y ] ) )$ by A1-T3 and T2.

A1-T5. $( \lambda z . P ) [ x := N ] = ( \lambda z . P )$ by A1-T3 and Lemma 1.2.5 (i).

A1-T6. $( \lambda y. P [ z := y ] ) [ x := N' ] = ( \lambda y. P [ z := y ] )$ by A1-T4 and Lemma 1.2.5 (i).

A1-T7. $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N' ]$ by T1, A1-T5, and A1-T6.

A2. Let $x = y$.

A2-T1. $y \notin FV ( P [ z := y ] ) - \{ y \}$.

A2-T2. $FV ( P [ z := y ] ) - \{ y \} = FV ( ( \lambda y . P [ z := y ] ) )$.

A2-T3. $x \notin FV ( ( \lambda y . P [ z := y ] ) )$ by A2, A2-T1, and A2-T2.

A2-T4. $x \notin FV ( ( \lambda z . P ) )$ by A2-T3 and T2.

A2-T5. $( \lambda y. P [ z := y ] ) [ x := N' ] = ( \lambda y. P [ z := y ] )$ by A2-T3 and Lemma 1.2.5 (i).

A2-T6. $( \lambda z . P ) [ x := N ] = ( \lambda z . P )$ by A2-T4 and Lemma 1.2.5 (i).

A2-T7. $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N' ]$ by T1, A2-T5, and A2-T6.

A3. Let $x \neq y$ and $x \neq z$.

A3-T1. $x \neq y$ by A3.

A3-T2. $x \neq z$ by A3.

A3-T3. $P [ x := N ]$ is defined by H10, A3-T2, and (e) of the definition of substitution.

A3-T4. $( \lambda z . P ) [ x := N ] = ( \lambda z . P [ x := N ] )$ by H10, A3-T2, and (e) of the definition of substitution.

A3-T5. $x \notin FV ( P )$ or $z \notin FV ( N )$ by H10, A3-T2, and (e) of the definition of substitution.

A3-T6. $P [ z := y ] [ x := N' ]$ is defined by H11, A3-T1, and (e) of the definition of substitution.

A3-T7. $( \lambda y . P [ z := y ] ) [ x := N' ] = ( \lambda y . P [ z := y ] [ x := N' ] )$ by H11, A3-T1, and (e) of the definition of substitution.

A3-T8. $x \notin FV ( P [ z := y ] )$ or $y \notin FV ( N' )$ by H11, A3-T1, and (e) of the definition of substitution.

A3-A4. Let $x \notin FV ( P )$.

A3-A4-T1. $P [ x := N ] = P$ by A3-A4 and Lemma 1.2.5 (i).

A3-A4-T2. $( \lambda z . P [ x := N ] ) = ( \lambda z . P )$ by A3-A4-T1.

A3-A4-T3. $x \notin FV ( y )$ by A3-T1.

A3-A4-T4. $x \notin FV ( P [ z := y ] )$ by H5, A3-A4, A3-A4-T3, and Lemma 1.2.5 (ii).

A3-A4-T5. $P [ z := y ] [ x := N' ] = P [ z := y ]$ by A3-A4-T4 and Lemma 1.2.5 (i).

A3-A4-T6. $( \lambda y. P [ z := y ] [ x := N' ] ) = ( \lambda y . P [ z := y ] )$ by A3-A4-T5.

A3-A4-T7. $( \lambda y. P [ z := y ] ) [ x := N' ] = ( \lambda y . P [ z := y ] )$ by A3-T7 and A3-A4-T6.

A3-A4-T8. $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N' ]$ by A3-T4, A3-A4-T2, T1, and A3-A4-T7.

A3-A5. Let $x \in FV ( P )$.

A3-A5-T1. $z \notin FV ( N )$ by A3-A5 and A3-T5.

A3-A5-T2. $x \in FV ( P [ z := y ] )$ by H5, A3-A5, A3-T2, and Lemma 1.2.5 (ii).

A3-A5-T2. $y \notin FV ( N' )$ by A3-T8 and A3-A5-T2.

I do not understand the remaining part of the proof. It consists of:

and thus also $y \notin FV ( P [ x := N' ] )$. By Lemma 1.2.6 it then follows that $M' [ x := N' ] = \lambda y . P [ z := y ] [ x := N' ] = \lambda y . P [ x := N' ] [ z := y ] =_{\alpha} [ z . P [ x := N' ]$. By the induction hypothesis $\lambda z . P [ x := N' ] =_{\alpha} \lambda z . P [ x := N ] = M [ x := N ]$.

Is there a further induction on $P$ at this point?

$\endgroup$
  • $\begingroup$ Could you add the statement of the lemma? Otherwise it is impossible to understand your question. $\endgroup$ – Taroccoesbrocco Feb 25 at 4:24
  • $\begingroup$ @Taroccoesbrocco Added. $\endgroup$ – user695931 Feb 25 at 4:29
  • $\begingroup$ The case you refer to is the one where $M = \lambda z.P$, isn't it? $\endgroup$ – Taroccoesbrocco Feb 25 at 4:45
  • $\begingroup$ @Taroccoesbrocco Yes. $\endgroup$ – user695931 Feb 25 at 4:58
  • $\begingroup$ It seems to me that you are putting together several questions (there are three different occurrences of "not certain why", referring to different problems). Please, could you be more precise? What is exactly unclear? $\endgroup$ – Taroccoesbrocco Feb 25 at 14:21

Your Answer

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

Browse other questions tagged or ask your own question.