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

I’m following along to a derivation of the function that returns the sum of the first $$n$$ natural numbers in this brilliant.org article on Lambda Calculus. To get to the derivation, either

• Go to Fixed Points and Recursion section > Recursion subsection > the first Example in that subsection.
• Or, if it is collapsed, expand the Fixed Points and Recursion section, then search (Ctrl-F or Cmd-F) for the following

Let us try to implement a function that returns the sum of the first

It seems to me like they make the following argument:

1. $$f$$ is a fixed point of some function $$h$$, i.e. $$f = hf$$. (See footnote $$^1$$)
2. Hey, you know what else is a fixed-point of $$h$$? ($$\Theta h$$) is a fixed-point of $$h$$ (where $$\Theta$$ is Turing’s fixed-point combinator)
3. Conclude from 1. and 2. that $$f = \Theta h$$.

I’m wondering if that’s a valid conclusion. It seems like it doesn’t necessarily have to follow from the premises (1. and 2.). It seems to assume something - it seems to assume either:

• $$h$$ has only one fixed-point, so if we find two things that are each a fixed-point of $$h$$, then the two things must be the same thing, or
• more strongly, that all fixed-points of a function $$h$$ are equal to each other.

$$^1$$: In the article’s derivation, $$h$$ is

$$(\lambda g. \lambda n.\textsf{ifThenElse}\ (\textsf{isZero}\ n)\ \bar 0\ (\textsf{add}\ n\ (g\ (\textsf{pred}\ n))))$$

where $$\textsf{ifThenElse}$$, $$\textsf{isZero}$$, $$\textsf{add}$$, and $$\textsf{pred}$$ are functions defined earlier in the article.

• I don't find your quoted section starting from "We've established that f is a fixed point of" in your linked source, can you clarify? Dec 11, 2021 at 2:18
• Sorry about that. I clarified. Should I transcribe their derivation here? Dec 11, 2021 at 12:41
• Notation: if f as point then g denotes a functional? Don't see a context free base for a fixpoint being unique. May there are some constraints in "Lambda Calculus". Dec 11, 2021 at 12:54
• It's definitely not unique, see also nlab article on same topic with a similar concrete example here... Dec 12, 2021 at 1:00
• This article contains nothing new and I only referenced for confirmation evidence in case you're not completely certain, since now seems you completely understand you don't need it any more... Dec 12, 2021 at 5:23

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.
• Thanks! Phrasing it as “f = $\Theta h$ is a solution (but not necessarily the only solution) to $f = hf$“ really helped me understand the situation. So $f = hf$ Is a constraint, but does not necessarily uniquely define $f$. It just says that if $f$ exists, then it must be a fixed-point of $h$. Dec 12, 2021 at 1:37