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.

  • 1
    $\begingroup$ 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? $\endgroup$ Dec 11, 2021 at 2:18
  • $\begingroup$ Sorry about that. I clarified. Should I transcribe their derivation here? $\endgroup$
    – joseville
    Dec 11, 2021 at 12:41
  • $\begingroup$ 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". $\endgroup$ Dec 11, 2021 at 12:54
  • 2
    $\begingroup$ It's definitely not unique, see also nlab article on same topic with a similar concrete example here... $\endgroup$ Dec 12, 2021 at 1:00
  • 1
    $\begingroup$ 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... $\endgroup$ Dec 12, 2021 at 5:23

1 Answer 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.

So in summary your reference here is somewhat confusing by not mentioning this result is not unique...

  • $\begingroup$ 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$. $\endgroup$
    – joseville
    Dec 12, 2021 at 1:37

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .