Timeline for Are two $\alpha$-equivalent terms syntatically identical? (metalanguage)
Current License: CC BY-SA 4.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 28 at 10:48 | history | edited | Tankut Beygu | CC BY-SA 4.0 | edited title |
| May 28 at 10:16 | history | edited | Tankut Beygu | CC BY-SA 4.0 | edited title |
| May 28 at 10:10 | answer | added | Tankut Beygu | timeline score: 0 | |
| May 28 at 10:10 | history | edited | Tankut Beygu | CC BY-SA 4.0 | added 174 characters in body; edited tags; edited title |
| Jun 24, 2017 at 9:05 | comment | added | md2perpe | 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: win.tue.nl/~wsinrpn/contact.htm | |
| Jun 23, 2017 at 21:31 | comment | added | user80458 | 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, 2017 at 21:24 | comment | added | user80458 | $\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, 2017 at 21:22 | comment | added | user80458 | @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, 2017 at 20:56 | comment | added | md2perpe | 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$. | |
| Jun 23, 2017 at 17:00 | comment | added | user80458 | 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, 2017 at 16:56 | comment | added | user80458 | @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, 2017 at 7:04 | comment | added | md2perpe | 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$? | |
| Jun 23, 2017 at 0:50 | comment | added | user80458 | @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 22, 2017 at 18:42 | comment | added | md2perpe | 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]$? | |
| Jun 22, 2017 at 17:11 | comment | added | user80458 | 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, 2017 at 17:06 | comment | added | user80458 | @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, 2017 at 16:48 | comment | added | md2perpe | 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. | |
| Jun 22, 2017 at 15:05 | comment | added | user80458 | @md2perpe: Sorry, that was a mistake, it was supposed to be $[x := y]$ on both sides. I've fixed my question | |
| Jun 22, 2017 at 15:05 | history | edited | user80458 | CC BY-SA 3.0 | edited body |
| Jun 22, 2017 at 14:56 | comment | added | md2perpe | Why would $(\lambda a. M)[x := y] \equiv \lambda a. M[y := x]$ be valid? | |
| Jun 22, 2017 at 14:18 | history | edited | user80458 | CC BY-SA 3.0 | added 111 characters in body |
| Jun 22, 2017 at 14:00 | history | asked | user80458 | CC BY-SA 3.0 |