1

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$?

Ekesh Kumar
  • 3,500
topkek
  • 31
  • 4

1 Answers1

1

$(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)$.

lisyarus
  • 15,517
  • So in the example of $\lambda x.\lambda y.(xx)y$ one could do an $\alpha$-conversion to convert it to $\lambda a.\lambda b.(xx)y$ and then apply the $(xx)$ to $a$ and $y$ to b and result in $xy$? Then in the second one will be $\lambda x.(xx) = \lambda x.x$? Do I understand it correctly? – topkek Jun 13 '20 at 06:43
  • @beginner No, you cannot $\alpha$-convert $\lambda x.\lambda y.(xx) y$ to $\lambda a.\lambda b.(xx) y$, since $x$ and $y$ are bound variables: the $x$ in $\lambda x$ is the same $x$ as in $(xx)$. You can $\alpha$-convert it to e.g. $\lambda a.\lambda b.(aa) b$. Does it make things more clear? – lisyarus Jun 13 '20 at 06:47