0

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?

  • Why would $(\lambda a. M)[x := y] \equiv \lambda a. M[y := x]$ be valid? – md2perpe Jun 22 '17 at 14:56
  • @md2perpe: Sorry, that was a mistake, it was supposed to be $[x := y]$ on both sides. I've fixed my question –  Jun 22 '17 at 15:05
  • 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. – md2perpe Jun 22 '17 at 16:48
  • @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. –  Jun 22 '17 at 17:06
  • 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. –  Jun 22 '17 at 17:11
  • I'm trying to follow your reasoning ... From $\lambda a. M[x:=y] \equiv \lambda b. M[x:=y]^{a\to b}$, do you draw the conclusion that $\lambda a. M \equiv \lambda b.M^{a\to b}$, i.e. that it's okay to remove $[x:=y]$? – md2perpe Jun 22 '17 at 18:42
  • @md2perpe: Yes, making the same substitution in the same term should produce the same term ($N$ in my answer)... And even if you disagree with that, you could say that you just pick an $x$ that doesn't appear in $M$ at all, in which case it remains $M$ after the substitution. –  Jun 23 '17 at 00:50
  • Making the same substitution in the same term should produce the same term, but if two terms result in the term after the same substitution, must really the two terms have been the same from the beginning? If $M[x:=y] = N[x:=y]$ must $M=N$? Take $M=x$ and $N=y$. Is $M[x:=y] = N[x:=y]$? Is $M=N$? – md2perpe Jun 23 '17 at 07:04
  • @md2perpe: What? That is not at all what I'm saying. I'm just defining $N$ to be the result of $M[x := y]$... I am not at all saying that $M[x:=y]\equiv N[x:=y]$, but rather that $M[x:=y] \equiv M[x:=y]$ (obviously, because both sides are identical!), and call the result "$N$". –  Jun 23 '17 at 16:56
  • And that doesn't even matter, because I could just say instead "I picked $x$ to be a variable that doesn't appear in $M$" and then $M[x := y] \equiv M$. –  Jun 23 '17 at 17:00
  • I can not see that you are defining $N$ somewhere. Anyway, obviously I don't follow your reasoning. Could you clarify? Take two non-identical terms, show that they are $\alpha$-equivalent, and that they are $\equiv$-equivalent (through substitution). Take for example $\lambda x.x$ and $\lambda y.y$. Please use equivalence chains, i.e. $M =\alpha N =\alpha P =_\alpha \cdots$. – md2perpe Jun 23 '17 at 20:56
  • @md2perpe: All I was saying was that for every $N$, there is some $M[x := y]$ that produces it. But forget about $N$ and just pretend that I've picked a variable $x$ that doesn't appear in $M$, such that $M[x := y] \equiv M$ on both sides. As an example: $(\lambda x. x)[a := b] \equiv \lambda x. x^{x\to x}[a := b] \equiv \lambda x. x$ (rule 3), and $(\lambda x. x)[a := b] \equiv \lambda y. x^{x\to y}[a := b] \equiv \lambda y. y$ (rule 3 again, but with a renaming of $x$ to $y$, as the book's definition allows doing. The left hand sides are equivalent, so so should the right hand sides: –  Jun 23 '17 at 21:22
  • $\lambda x. x \equiv \lambda y. y$. This logic can be used for any two $\alpha$-equivalent terms, which would mean that $\alpha$-equivalent terms are $\equiv$ (syntactically identical). –  Jun 23 '17 at 21:24
  • Basically what I'm saying is that if we're allowed to do renaming of variables while we're doing a substitution, and substitutions make $\equiv$-equivalent, then we can make any $\alpha$-equivalent terms (such as $\lambda x. x$ and $\lambda y. y$) to also be $\equiv$. –  Jun 23 '17 at 21:31
  • Now I get it and understand how you get for example $\lambda x.x \equiv \lambda y.y$. I think that you should contact the author about it: http://www.win.tue.nl/~wsinrpn/contact.htm – md2perpe Jun 24 '17 at 09:05

0 Answers0