I'm just getting started with lambda calculus and I see that the fixed-point $Y$ combinator is defined as:

$Y = \lambda f . (\lambda x . f(x x))(\lambda x . f(x x))$ (*)

I read here that something like $t s$ (where $t, s$ are both terms) represents an application of a function $t$ to the input $s$, so in (*) I suppose that $x x$ represents the application of $x$ to the input $x$.

The problem I have with that interpretation is that it supposes that $x$ is itself a function (or an abstraction, as defined in the article).

However, in general $x$ seems to just denote a variable so how should I understand $x x$?


2 Answers 2


You're right: $xx$ is the application of $x$ to $x$. But this is not a problem as long as you remember that you're only dealing with syntax here: $x$ is a term, $x$ is another term, so $xx$ is a term. In particular, to form an application term $MN$, you do not suppose that $M$ is an abstraction.

Another way to put this is that in λ-calculus, everything is a function, not only the abstractions. $x$, in particular, is a function that you can apply to any argument.

Of course, in a typed setting terms like $Y$ raise typing issues. But you're doing untyped λ-calculus here, so you don't need to find a well-formed type for $x$.

By the way, having this kind of weird (at first sight...) behaviour is precisely what makes λ-calculus interesting as a computation model.


in $\lambda x . f(xx)$, you are correct to say that $x$ is the variable of a lambda abstraction. However, a variable is simply a placeholder for the substitution that happens when the lambda abstraction is applied to some argument. Consider the following application: $$ (\lambda x . f(x\,x))\,y \;\to_\beta\; f(y\, y) $$ The way you evaluate any application $(\lambda x.t)s$ is by substituting every instance of $x$ in $t$ with $s$.

In the example above $t$ is $f(x\,x)$, and $s$ is $y$, therefore you substitute all the $x$'s in $f(x\,x)$ with $y$'s, obtaining $f(y\,y)$. In this case $y$ is a free variable, but in the case of he $Y$ combinator it's bounded, therefore $y$ could be substituted with any possible $\lambda$-term.

Now that the semantics is clearer, you may ask what would it mean to "feed a function to itself" as its own input. Consider the following combinator (combinator is just a name for a $\lambda$-term with no free variables): $$ \Omega = \lambda x. x x $$ What would it mean to apply this term to itself? $$ \begin{aligned} \Omega\,\Omega &= (\lambda x. x x)(\lambda x. x x)\\ &\to_\beta (\lambda x. x x)(\lambda x. x x) \\ &\to_\beta \;... \end{aligned} $$ Since every time we substitute the two $x$'s in the expression $x\,x$ with the term $(\lambda x . xx)$ we obtain a new term: $(\lambda x . xx)(\lambda x . xx)$. This happens to be precisely what we started with, and therefore if we keep applying the beta-reduction rule we will always end up where we started; the evaluation never terminates.

If we now come to the $Y$ combinator, we can show that it has a similar property. Notice what happens when we apply $Y$ to a lambda-term $F$.

$$ \begin{aligned} Y F &= (\lambda f . (\lambda x . f(x x)) (\lambda x . f(x x)))F \\ &\to_\beta (\lambda x . F (x x)) (\lambda x . F (x x)) & (1) \\ &\to_\beta F (\lambda x . F (x x)) (\lambda x . F (x x)) & (2) \\ &= F(YF) & (3) \end{aligned} $$ In (1) we simply substitute the $f$ variable for the term $F$. In (2) we substitute the $x$'s in $F(x x)$ with $(\lambda x . F (x x))$, and (3) follows from the fact that we are obtaining line (1) with an $F$ applied to it.

The fact that $YF = F(YF)$ (i.e. $YF$ is a fixed point of $F$) implies that: $$YF = F(YF) = F(F(YF)) = F(F(...F(YF)))$$ And therefore applying the $Y$ combinator to any term $F$ basically applies the term to itself forever. This can be used to write "recursive functions" in the lambda calculus.

Sorry if that was a bit long, I just thought that taking it step by step would help you better understand what is meant by $x\,x$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.