0
$\begingroup$

I am reading "Type Theory and Formal Proof: An Introduction" by Rob Nederpelt.

On page 6, $M \equiv N$ is defined to mean that the $\lambda$-terms $M$ and $N$ are identical. On page 10, $\alpha$-equivalence is defined to be:

  1. $\lambda x. N =_\alpha \lambda y. N^{x \to y}$ if $y$ is not a variable in $N$
  2. Any other terms are lambda equivalent iff their subterms are $\alpha$-equivalent
  3. $M =_\alpha M$

On page 12, substitution is defined to be:

  1. $y[x := N] \equiv N$ if $x = y$ or $\equiv y$ otherwise
  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 $P^{y \to z}$ is an $\alpha$-variant of $P$ such that $z$ is not a free variable in $N$

But since $(\lambda a. M)[x := y] \equiv \lambda a. M[x := y]$ if $a \neq x$ but also $(\lambda a. M)[x := y] \equiv \lambda b. M[x := y]^{a \to b}$ and $M[x := y] \equiv M[x := y]$, this would mean that (because of transitivity of $\equiv$) for any term $N$, $\lambda a. N \equiv \lambda b. N^{a \to b}$. Since $\equiv$ also follows rules 2 and 3 of alpha equivalence, this would mean that any $\alpha$-equivalent terms would be identical.

Is this a mistake in the book (does substitution not work for $\lambda y. P$ when $N$ contains a free $y$, as Wikipedia seems to say) ? Or can we really say that two $\alpha$-equivalent terms are identical?

Also, even if this is right, shouldn't there also be a condition that $z \neq x$ in rule 3 of substitution?

$\endgroup$
  • $\begingroup$ Why would $(\lambda a. M)[x := y] \equiv \lambda a. M[y := x]$ be valid? $\endgroup$ – md2perpe Jun 22 '17 at 14:56
  • $\begingroup$ @md2perpe: Sorry, that was a mistake, it was supposed to be $[x := y]$ on both sides. I've fixed my question $\endgroup$ – Runemoro Jun 22 '17 at 15:05
  • $\begingroup$ From where do you get $(\lambda a. M)[x := y] \equiv \lambda a. M[x := y]$ and $(\lambda a. M)[x := y] \equiv \lambda b. M[x := y]^{a \to b}$? I don't see how they follow from the definitions. $\endgroup$ – md2perpe Jun 22 '17 at 16:48
  • $\begingroup$ @md2perpe: The first one is from rule 3 of substitution assuming that $a \neq y$ (so we can leave the same name for $a$ ($M^{a \to a} \equiv M$)) and the second is from rule 3 but renaming $a$ to $b$. I've swapped the substitution and the renaming because $a \neq y$ and $b \neq x$ so the order won't matter. $\endgroup$ – Runemoro Jun 22 '17 at 17:06
  • $\begingroup$ Then we say that the two right hand sides are equivalent (transitivity) and we can either say that $M[x := y] \equiv M[x := y]$ or that we've picked $x$ such that it doesn't appear in $M$ to get the final result. $\endgroup$ – Runemoro Jun 22 '17 at 17:11

Your Answer

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

Browse other questions tagged or ask your own question.