Does it matter if I reverse the arguments order of a lambda calculus function?

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.

• 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? – Martin Berger Oct 21 '16 at 8:38
• @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. – Zhao Oct 21 '16 at 8:47
• 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. – Martin Berger Oct 21 '16 at 8:49

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.
• But for some functions like $\lambda .xy.x+y$, the order does not matter. Am I right? – Zhao Oct 21 '16 at 8:43
• $\lambda xy.x+y$ and $\lambda yx.x+y$ are equivalent, I think. – Zhao Oct 21 '16 at 8:44