Lambda Calculus: Recursive definition of capture avoiding substitution. I have spent a couple of weeks programming an implementation of the untyped lamdba calculus.
I believe that in doing so I have formulated a recursive deifnition for capture avoiding substitution (i.e. it uses substitution as a form of alpha conversion) which fits nicely into the definition of substitution given on Wikipedia.
I would really appreciate if someone could verify the correctness of it for me and, if it is correct, explain why this definition is rarely used because I find it to be very clear and simple.
Wikipedia's definition:
$x[x := N]       ≡ N$
$y[x := N]       ≡ y$, if $x ≠ y$
$(M_1 M_2)[x := N] ≡ (M_1[x := N]) (M_2[x := N])$
$(λx.M)[x := N]  ≡ λx.M$
$(λy.M)[x := N]  ≡ λy.(M[x := N])$, if $x ≠ y$, provided $y ∉ FV(N)$
My additional definition to enforce capture avoidance:
$(λy.M)[x := N]  ≡ λy_u.(M_u[x := N])$, if $x ≠ y$ and $y ∈ FV(N)$
where 
$y_u ∉ (FV(N) ∪ FV(M))$
$M_u ≡ M[y:=y_u]$
 A: What you propose is in fact done in some definitions of substituion, cf. for example Hindley & Seldin (2008): Lambda Calculus and Combinators.
The definition on Wikipedia is indeed unsatisfactory in that it is only a partial definition, providing the value of the substitution for the case where the freshness condition is not met only as an informal addendum; it is of course more elegant to have all cases defined formally as a full induction on the term structure.   
The additional clause e.g. Hindley & Selidn provide is almost identical to your proposal, with the minor difference that introducing the new notation $M_u$ can be avoided by stating the substitution of $[y := y_u]$ within $M$ straight away, then appending the actual substitution, i.e. $\lambda y_u.(M[y := y_u][x := N])$. With this notation, recursively applying the definitions will result in first reanaming every variable $y$ in $M$ to $y_u$, then performing the actual substitution of $x$ by $N$ in $M$.
Note that although this procedure does amount to alpha conversion, the result of the substitution where clashing variables have been converted is defined as the syntactically identical equivalent ($\equiv$, rather than $\equiv_\alpha$) to the term on the left-hand side - given that it is applied because the inductive definition enforces this conversion.
Note also that the Wikipedia definition is improvable in that one might want to impose an additional requirement to specify when alpha-conversion is necessary: In case $x$ does nowhere occur free in $M$, i.e. $x \not \in FV(M)$, nothing will be substituted, hence alpha-converting $y$ is not necessary as it won't accidentally bind anything in $N$ even if $y \in FV(N)$ - because $N$ is not inserted anywhere into $M$.
Hence, the condition on the last Wikipedia clause could be modified to "provided $y \not \in FV(N)$ or $x \not \in FV(M)$", and your additional definition correspondingly to "if $x \neq y$ and $y \in FV(N)$ and $x \in FV(M)$".  
To fancy it up some more, in addition to the inevitable requirement that $y_u ∉ (FV(N) ∪ FV(M))$, one might want to demand that $y_u$ be the first suitable variable in an assumed enumeration of all variables (which requires the ontological assumption that variables are given as a sequence rather than a set). Such a requirement has the advantage that the new variable is chosen systematically rather than arbitrarily, hence allowing terms $M_1, M_2$ where the same variables have undergone bound renaming to receive substitution results $M_1', M_2'$ that are syntactically identical to each other, rather than just alpha-congruent. But that already goes beyond the actual question; your definition is correct.
A: Your definition is not entirely correct. Consider for example $M = N = y$. Pick $y_u = x$ which is allowed because $x \notin (FV(N) ∪ FV(M))$. Then $M_u = x$ and thus $(λy.y)[x := y] ≡ λx.(M_u[x := y]) ≡ λx.y$. Picking $y_u \notin (FV(N) ∪ FV(M) ∪ \{ x \} )$ avoids this problem.
The definition of substitution in Hindley & Seldin '08 does not have this problem because it assumes $x \in FV(M)$ in the relevant case.
