$f$ is a fixed-point of $h$. $\Theta h$ is also a fixed-point of $h$. Can we conclude that $f$ equals $\Theta h$?

Solution 1:

For your referenced section from "Let us try to implement a function that returns the sum of the first", there's no principle issue as it's a standard application of fixed point combinators in untyped lambda calculus and functional programming. And you're absolutely right we find our named function $f$ now becomes a fixed point of the lambda abstraction $h=λg.λn.ifThenElse(isZero~n) \overline 0 (add~n(g(pred~n)))$, and we also know for any untyped lambda expression $h$ we always have some fixed point combinator $\Theta$ such that $\Theta h$ is a fixed point of $h$. So we have $f=hf, \Theta h=h \Theta h$, then we can obviously have $f=\Theta h$ as a possible solution for $f$. But by no means it's the only solution since as you said $h$ has many other famous combinators like $Y$ (actually infinitely many combinators per wikipedea source Bimbó, Katalin (27 July 2011). Combinatory Logic: Pure, Applied and Typed. p. 48. ISBN 9781439800010.). We may as well have $f=Yh$ since $Yh$ is also such a famous alternative fixed point of $h$. But whatever form we have we've already successfully applied fixed point combinator to transform the named recursive function $f$ to an equivalent lambda function $\Theta h$ (or $Yh$, etc), and the next section in your ref you see a concrete Haskell implementation of it.