# Ambiguity of definition of substitution in lambda calculus

From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:

Definition 1.6.1 (Substitution)

(1a) $$x[x := N] \equiv N$$,

(1b) $$y[x := N] \equiv y$$ if $$x \not \equiv y$$,

(2) $$(PQ)[x := N] \equiv (P[x := N])(Q[x := N])$$,

(3) $$(\lambda y . P)[x := N] \equiv \lambda z . (P^{y \to z} [x := N])$$, if $$\lambda z . P^{y \to z}$$ is an $$\alpha$$-variant of $$\lambda y . P$$ such that $$z \notin FV(N)$$.

If I look at $$(\lambda y . y)[y := a]$$ then it seems that I can have either:

$$(\lambda y . y)[y := a] = \lambda y . (y[y := a]) = \lambda y . a$$

or

$$(\lambda y . y)[y := a] = \lambda z . (z[y := a]) = \lambda z . z$$

These are very different. Have I missed something in the definition?

• Maybe (3) is missing the condition that you should have $z \not\equiv x$ which would invalidate the first substitution? (Not sure, not being completely familiar with the notation being used here - but the first result is definitely the suspect one.) – Daniel Schepler Dec 19 '18 at 23:20
• The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution – user695931 Dec 20 '18 at 0:49

Clearly, $$\lambda y. a$$ and $$\lambda z.z$$ are different (in the sense of not $$\alpha$$-equivalent) terms.
Actually, $$(\lambda y. y)[y := a] = \lambda z. z = \lambda y. y\,$$ (up to $$\alpha$$-equivalence) and there is no ambiguity. Indeed, according to definition 1.6.1 in Nederpelt' and Geuvers' handbook, $$(\lambda y.y)[y:=a] \neq \lambda y.(y[y:=a])$$ because in general $$\lambda z . P^{y \to z}$$ is defined provided that $$z \notin FV(P)$$ (see definition 1.5.1) and this condition does not hold in $$\lambda y.y$$ (where $$z = y = P$$).
• @user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x \neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = \lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(\lambda y.P)[x := N]) = \lambda y.P$ (no substitution is performed): this is exactly what happens for $(\lambda y.y)[y:=a]$. – Taroccoesbrocco Dec 20 '18 at 9:04
• I guess this makes sense. It seems confusing that they made the condition $x \not \equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution – user695931 Dec 20 '18 at 15:32