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

fixed points-lambda-calculus

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.

Best Answer

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

Related Question