2

In "Lectures on the Curry-Howard Isomorphism" by Morten Heine Sørensen and Pawel Urzyczyn, it is stated that:

The substitution of $N$ for $x$ in $M$, written $M [ x := N ]$, is defined iff no free occurrence of $x$ in $M$ is in a part of $M$ with form $\lambda y L$, where $y \in FV ( N )$.

I am trying to find a more mechanically formal corresponding statement to use in proofs of a given substitution being defined. For example, for use in a proof of Lemma 1.2.7:

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

Is there a more mechanically formal corresponding statement?

EDIT:

Possible equivalent definition from Taroccoesbrocco's answer:

Let $M$ and $N$ be any lambda terms. Let $x$ be any variable.

(a) If $M = x$ then $M [ x := N ]$ is defined and $M [ x := N ] = N$.

(b) If there exists a variable $y$ such that $M = y$, and $x \neq y$, then $M [ x := N ]$ is defined and $M [ x := N ] = M$.

(c) If there exist lambda terms $P$ and $Q$ such that $M = ( P Q )$, then $M [ x := N ]$ is defined if and only if $P [ x := N ]$ is defined and $Q [ x := N ]$ is defined. Then $M [ x := N ] = ( P [ x := N ] Q [ x := N ] )$.

(d) If there exists a lambda term $P$ such that $M = ( \lambda x . P )$ then $M [ x := N ]$ is defined and $M [ x := N ] = M$.

(e) If there exists a variable $y$ and a lambda term $P$ such that $M = ( \lambda y . P )$, and $x \neq y$, then $M [ x := N ]$ is defined if and only if $P [ x := N ]$ is defined, and either $y \notin FV ( N )$ or $x \notin FV ( P )$. Then $M [ x := N ] = ( \lambda y . P [ x := N ] )$.

Note that by Lemma 1.2.5 (i), $x \notin FV ( P )$ implies $P [ x := N ]$ is defined, and hence the last case can be changed to:

(e) If there exists a variable $y$ and a lambda term $P$ such that $M = ( \lambda y . P )$, and $x \neq y$, then $M [ x := N ]$ is defined if and only if either $x \notin FV ( P )$ or both $P [ x := N ]$ is defined and $y \notin FV ( N )$. Then $M [ x := N ] = ( \lambda y . P [ x := N ] )$.

Note that if $x \notin FV ( P )$, then $x \notin FV ( \lambda y . P )$, and if $x \neq y$, then if $x \notin FV ( \lambda y . P )$, then $x \notin FV ( P )$. Hence the last case can be changed again to:

(e) If there exists a variable $y$ and a lambda term $P$ such that $M = ( \lambda y . P )$, and $x \neq y$, then $M [ x := N ]$ is defined if and only if either $x \notin FV ( M )$ or both $P [ x := N ]$ is defined and $y \notin FV ( N )$. Then $M [ x := N ] = ( \lambda y . P [ x := N ] )$.

user695931
  • 517

1 Answers1

2

The word "mechanical" is slightly ambiguous, it could be interpreted in several (more or less restrictive) ways. Maybe, a definition of the property "The substitution of $N$ for $x$ in $M$ is defined" by structural induction on $M$ is what you are looking for.

We say that "the substitution of $N$ for $x$ in $M$ (written $M [x := N]$) is defined" when:

  • either $M$ is a variable and then there are two sub-cases: if $M = x$, then we set $M[x := N] = N$; otherwise $M = y \neq x$ and then we set $M [x:= N] = y$;
  • or $M = M_1M_2$ and then $M[x:=N]$ is defined if and only if $M_1[x:= N]$ and $M_2[x:=N]$ are so; in this case, we set $M[x:=N] = M_1[x:=N] M_2[x:=N]$;
  • or $M = \lambda y L$ and then $M[x :=N]$ is defined if and only if either $x \notin FV(M)$, or $L[x:= N]$ is defined and $y \notin FV(N)$; in these cases, we set $M [x:= N] = \lambda y (L[x:=N])$ if $x \neq y$, otherwise $M [x:= N] = M$.

The idea is that $(\lambda y \, x)[x := y]$ is not defined because otherwise, according to the definition above, $(\lambda y \, x)[x := y] = \lambda y \, y$. Why would it be problematic? Because $\lambda y \, x$ represents a constant function associating $x$ with every argument, hence $(\lambda y \, x)[x := y]$ (the constant function for $x$ where $x$ is replaced by $y$) should represent a constant function associating $y$ with every argument; but $\lambda y \, y$ is not such a function, it represents the identity function instead.

Taroccoesbrocco
  • 16,964
  • In the last case, are the cases where $x = y$ and $x \notin FV ( L )$ handled by the induction somehow? – user695931 Feb 11 '19 at 23:37
  • @user695931 - Yes, I forgot the case $M = \lambda x L$, I edited my answer. The fact whether $x \notin FV (L)$ or $x \in FV(L)$ is irrelevant (it is subsumed in the other cases). – Taroccoesbrocco Feb 12 '19 at 00:19
  • Why is $x \notin FV ( L )$ irrelevant? Is it not need to have $(\lambda y y) [x := y]$ be defined? – user695931 Feb 12 '19 at 00:36
  • @user695931 - Indeed, $(\lambda y , y)[x:=y]$ is defined according to the definition I gave (I rewritten the last case to be more explicit): $(\lambda y , y)[x:=y] = \lambda y (y[x:=y]) = \lambda y , y$. – Taroccoesbrocco Feb 12 '19 at 01:23
  • Do we perhaps need $L [ x := N ]$ to be defined in the case of $x \notin FV ( M )$ as well? – user695931 Feb 12 '19 at 02:29
  • Did you mean $x \notin FV ( L )$ in your last edit? Then my last comment would be irrelevant, since that would imply $L [ x := N ]$ is defined by Lemma 1.2.5 (i) of the text. – user695931 Feb 12 '19 at 05:10
  • @user695931 - No, we don't need $L[x:=N]$ to be defined when $x \notin FV(M)$. For instance, $(\lambda x \lambda y , x)[x:=y]$ is defined, even though $(\lambda y , x)[x:=y]$ is not: $(\lambda x \lambda y , x)[x:=y] = \lambda x \lambda y , x$. The case $x \notin FV(M)$ means that there are no free occurrences of $x$ in $M$, and hence the condition "no free occurrence of $$ in $$ is in a part of $$ with form $$, where $∈()$" is vacuously true. – Taroccoesbrocco Feb 12 '19 at 06:04
  • @user695931 - The condition $x \notin FV(M)$ is equivalent to $x \notin FV(L) \cup {y}$. Sorry, I don't have the the text you mention, so I don't know what Lemma 1.2.5 (i) is. – Taroccoesbrocco Feb 12 '19 at 06:08
  • The part of the book this is in is available as a free sample from the link in the question. – user695931 Feb 12 '19 at 06:24
  • I think I might see. So in the case that $x \neq y$, $x \notin FV ( M ) = x \notin FV ( L )$. – user695931 Feb 12 '19 at 06:32
  • @user695931 - Exactly! – Taroccoesbrocco Feb 12 '19 at 06:34
  • I hope you don't mind. I added what I think is an equivalent definition to my question. Is this equivalent? – user695931 Feb 12 '19 at 06:46
  • @user695931 - It's perfectly equivalent. – Taroccoesbrocco Feb 12 '19 at 07:11
  • Added one more explanation to show why. Thank you! – user695931 Feb 12 '19 at 07:13
  • I think that last explanation makes sense? – user695931 Feb 12 '19 at 07:17
  • @user695931 - Yes, it does. – Taroccoesbrocco Feb 12 '19 at 07:34