I'm trying to understand fixpoints in the Lambda Calculus with the example of computing the fixpoint of $\lambda xy.xy$. I might have a vague intuition what $\lambda x.(\lambda xy.xy)(xx)$ means/does but I cannot go any further. What does $\lambda x.(\lambda xy.xy)(xx)$ or $\lambda x.\lambda y(xx)y$ mean/do?
I understand what $\lambda x.x$ or $(\lambda x.x)y$ mean (and do) but the $(xx)$ with or without the extra $y$ completely confuses me. Does it mean that $x=x$?
Best Answer
$(xx)$ means that the term $x$, whatever it is, is applied to the term $x$. Here, both the function and its argument are $x$, and there's nothing wrong with that (until you try to introduce types, but that's another story).
$\lambda x.\lambda y. (xx) y$ is a function that takes two arguments, applies the first of them to itself, and applies the result to the second argument.
$\lambda x.(\lambda xy.xy)(xx)$ takes an argument $x$ and applies $\lambda xy.xy$ (here the $x$ is another $x$; we can $\alpha$-convert the term to $\lambda ab.ab$) to the result of evaluating $(xx)$.