In the lambda expression (λx. (λy. y z)(λw. w) z x)[z→y], I'm inclined to change y to another variable, then perform the substitution. Is this the correct way to approach this problem? Also, if that's the case, and you can just alpha-reduce back, couldn't (λx. (λy. y z)(λw. w) z x) be an appropriate answer (y => w, z => y, y => z, w => y, where they are all alpha-reductions)? Thanks!
Asked
Active
Viewed 628 times
1
-
Please improve the typesetting of your mathematics using latex. (See http://math.stackexchange.com/editing-help for this and other useful information on typing your posts.) – Mårten W Mar 06 '13 at 23:20
1 Answers
1
I take it that you are writing $t[x {\rightarrow} s]$ for the result of substituting $s$ for $x$ in $t$. When you substitute $s$ for $x$ in a $\lambda$-expression $t$, you may use $\alpha$-conversion to rename bound variables in $t$ to avoid clashes, but you must not rename the free variables of $s$. In your example $s$ is $y$ and when you substitute $y$ for $z$ in $\lambda x.(\lambda y. y z) (\lambda w.w) z x$, you must get (something $\alpha$-equivalent to) $\lambda x. (\lambda y'. y' y) (\lambda w.w) y x$.
Rob Arthan
- 48,577
-
Wow, thank you. I guess in my example I couldn't have actually used "w", but I guess you got what I was saying. I was over-thinking it, and apparently didn't take adequate notes in class, and just wanted to be sure. I really appreciate the thorough response. – Ross Verry Mar 07 '13 at 02:39