2
$\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 Answer 1

2
$\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$
16
  • $\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, 2019 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$ Feb 12, 2019 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, 2019 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$ Feb 12, 2019 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, 2019 at 2:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .