I have spent a couple of weeks programming an implementation of the untyped lambda calculus.
I believe that in doing so I may have formulated a recursive definition 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
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[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'.(M'[x := N]), if x ≠ y and y ∈ FV(N)
where
y' ∉ (FV(N) ∪ FV(M))
M' ≡ M[y:=y']
Your rule is correct.
It's not frequently used because it needs to keep track of free variable. It's really counterintuitive, in the sense that we all agree names never matter, while in this implementation, names play a central role.
You have not shown your operational semantics yet. If you do so, you will see that app rule requires to know if x is captured by N as in (λx.M) N. If so, alpha renaming needs to be triggered.
The problem here is there are too many(infinite) representations for essential one expression. One typical way to solve this, is via de Bruijin index, or a hybrid way called locally nameless.
https://en.wikipedia.org/wiki/De_Bruijn_index
https://www.chargueraud.org/research/2009/ln/main.pdf
The main idea is the same: both take quotient of a bound expression, such that one expression has exactly one canonical form.