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

Question

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

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