Formal definition of substitution being defined in type free lambda calculus

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

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.

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