For reference, the $Y$-combinator is the expression

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

in the untyped lambda calculus. If $g$ is any lambda expression, then

\begin{align} Y g &= \lambda f . (\lambda x . f (xx)) (\lambda x . f (xx)) g \\ &\to_\beta (\lambda x . g (xx)) (\lambda x . g (xx)) \\ &\to_\beta g ((\lambda x . g (xx))(\lambda x . g (xx))), \end{align}

and the $\beta$-reductions used are at the top level (so this is possible using call-by-name evaluation). However, it is then claimed (see below) that

$$ g ((\lambda x . g (xx))(\lambda x . g (xx))) = g(Yg). $$

But this seems to be wrong, at least if we interpret equality as actual equality and not some sort of $\beta$-equivalence. Furthermore, the right-hand side reduces to the left-hand side, not vice-versa, and this reduction is not possible using call-by-name.

Nonetheless, the nLab claims that there is a multi-step reduction $Yg \to_\beta g(Yg)$, it is implicit on this Wikipedia page, it is stated on these lecture slides (pdf-warning; page 17), etc. So apparently it is supposed to be the case. Am I missing something, or is it actually false that $Yg \to_\beta g(Yg)$?

(Note: I mention call-by-name evaluation because $Y$ is used to construct recursive functions when using call-by-name. So presumably we should restrict ourselves to only perform reductions compatible with call-by-name for the reduction to be useful in that context?)


1 Answer 1


I think it is technically incorrect that $Y g →_β g(Yg)$ using the definitions you've given. However, the one step $β$ reduction of $Yg$ is a fixed point of $g$ under reduction. Since the things you've given names to give no easy way to refer to this one step reduction, people just write $Yg$ instead, and don't worry about this minor detail (and often they are working up to $β$ equivalence, where it is exactly true).

I can't think of any situation where it'd be important whether $Yg$ itself is a fixed point of $g$ or immediately reduces to a fixed point of $g$.


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.