Formal definition of substitution being defined in type free lambda calculus

Question

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

Answer 1

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.