1
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ In the last case, are the cases where $x = y$ and $x \notin FV ( L )$ handled by the induction somehow? $\endgroup$ – user695931 Feb 11 at 23:37
  • $\begingroup$ @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). $\endgroup$ – Taroccoesbrocco Feb 12 at 0:19
  • $\begingroup$ Why is $x \notin FV ( L )$ irrelevant? Is it not need to have $(\lambda y y) [x := y]$ be defined? $\endgroup$ – user695931 Feb 12 at 0:36
  • $\begingroup$ @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$. $\endgroup$ – Taroccoesbrocco Feb 12 at 1:23
  • $\begingroup$ Do we perhaps need $L [ x := N ]$ to be defined in the case of $x \notin FV ( M )$ as well? $\endgroup$ – user695931 Feb 12 at 2:29

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.