# Is it actually the case that $Yg \to_\beta g(Yg)$?

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

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