Y combinator, function composition

I am trying to understand Y combinators. Could you please explain why the following are equivalent

(Y (f ∘ g))   
(f (Y (g ∘ f)))

(Y is a fixed point combination)

It depends on the notion of equivalence you are using.

Suppose we compare these terms according to their denotational semantics,
on $\omega$-CPO domains. Denote with $F,G$ the semantics of the terms $f,g$. Thus, $F,G$ are Scott-continuous functions. Then, we have that the semantics of $Y(f \circ g)$ is, according to the Kleene's fixed point theorem

$$
(1) = [\![ Y(f\circ g) ]\!] = \bigsqcup\{ \bot, F(G(\bot)),F(G(F(G(\bot)))),\ldots\}
$$
where $\bigsqcup$ denotes the supremum / least upper bound.

Similarly, we get

$$
(2) = [\![ f(Y(g\circ f) ]\!] = F(\bigsqcup\{ \bot, G(F(\bot)),G(F(G(F(\bot)))),\ldots\})
$$

By continuity, we get
$$
(2) = \bigsqcup\{ F(\bot), F(G(F(\bot))),F(G(F(G(F(\bot))))),\ldots\}
$$

One can then prove that $(1)=(2)$ by observing that any element of any one chain is bounded above by some element of the other chain. Indeed, we have
$$
\bot \sqsubseteq F(\bot), F(G(\bot)) \sqsubseteq F(G(F(\bot))), \ldots
$$
estabilishing that $(1)\sqsubseteq(2)$. Further,
$$
F(\bot) \sqsubseteq F(G(\bot)), F(G(F(\bot))) \sqsubseteq F(G(F(G(\bot)))), \ldots
$$
estabilishing that $(2)\sqsubseteq(1)$, concluding the proof.

Much less formally, the term $Y(f \circ g)$ expresses the infinite application
$$
f(g(f(g(\ldots))))
$$
and, similarly, $Y(g \circ f)$ expresses
$$
g(f(g(f(\ldots))))
$$
It is fairly natural, then, that applying a single $f$ on top of the second one results in the first one. The above domain-theoretic proof provides a formal justification of that.

StackExchange Computer Science Q#84721, answer score: 6