1
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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.) $\endgroup$ – Daniel Schepler Dec 19 '18 at 23:20
  • $\begingroup$ The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution $\endgroup$ – user695931 Dec 20 '18 at 0:49
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ I thought it would hold by remark 1.6.3 (1)? $\endgroup$ – user695931 Dec 20 '18 at 1:05
  • 1
    $\begingroup$ @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]$. $\endgroup$ – Taroccoesbrocco Dec 20 '18 at 9:04
  • $\begingroup$ 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 $\endgroup$ – user695931 Dec 20 '18 at 15:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.