1
$\begingroup$

what is the difference between the below functions? $$\lambda x.\lambda y.f(x, y)$$ $$\lambda y.\lambda x.f(x, y)$$

And it appears that there is a $\texttt{reverse operation}$ in lambda calculus which can reverse the order of the arguments. So does the order actually matter?

I am asking this question because I am reading this paper, in which the author reverse the argument order in the 5th page: $$ [\![ R[b]]\!] = \lambda y.\lambda x.[\![b]\!](x, y) $$ Here $R$ is the ${reverse}$ $operator$. I am not sure why the author did this. And why it matters to change the order in which the arguments are taken.

Improve this question
$\endgroup$
3
  • $\begingroup$ Your question has the same answer as the following maths questions: are $f(x, y) = x - y$ and $f(y, x) = x - y$ the same function? Are $\int_a^b \int_c^d f(x,y) dx\ dy$ and $\int_a^b \int_c^d f(x,y) dy\ dx$ the same integrals? $\endgroup$ – Martin Berger Oct 21 '16 at 8:38
  • $\begingroup$ @MartinBerger I don't think so. The $\texttt{reverse operation}$ here means reversing the order the arguments are taken, but the function body does not change. $\endgroup$ – Zhao Oct 21 '16 at 8:47
  • $\begingroup$ I'm not sure how reversing the arguments changes the matter. $\lambda xy.f(x,y)$ and $\lambda yx.f(x,y)$ are different functions. Yes, you can obtain one from the other by 're-routing' the arguments, but they still remain different functions. $\endgroup$ – Martin Berger Oct 21 '16 at 8:49
2
$\begingroup$

You can compute either of them from the other, by using the aforementioned "reverse arguments" function.

However, they are very different as functions. For instance, the usual encoding of true is $\lambda xy.\, x$ while false is encoded as $\lambda yx.\, x$ ($\alpha$-equivalent to $\lambda xy.\, y$), which is the flipped version of true. True and false are meant to be different.

Indeed, if we had true and false equal then, for any $M,N$ $$ M =_\beta^2 (\lambda xy.\, x) M N =_{Hp} (\lambda yx.\, x) M N =_\beta^2 N $$ So, we would get that all $\lambda$-terms are equal, making the whole theory of lambda calculus trivial.

Improve this answer
$\endgroup$
3
  • $\begingroup$ But for some functions like $\lambda .xy.x+y$, the order does not matter. Am I right? $\endgroup$ – Zhao Oct 21 '16 at 8:43
  • $\begingroup$ $\lambda xy.x+y$ and $\lambda yx.x+y$ are equivalent, I think. $\endgroup$ – Zhao Oct 21 '16 at 8:44
  • $\begingroup$ In the untyped lambda calculus they might not be equivalent, since we can apply both to some non-numeral value which breaks the commutativity of plus. Plus commutes on numerals, but we can pass more complex terms than those. $\endgroup$ – chi Oct 21 '16 at 9:02

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.