1

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?

user695931
  • 517
  • 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: https://en.wikipedia.org/wiki/Lambda_calculus#Substitution – user695931 Dec 20 '18 at 00:49

1 Answers1

1

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

Taroccoesbrocco
  • 16,964
  • I thought it would hold by remark 1.6.3 (1)? – user695931 Dec 20 '18 at 01:05
  • 1
    @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 09: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: https://en.wikipedia.org/wiki/Lambda_calculus#Substitution – user695931 Dec 20 '18 at 15:32