Lambda Calculus functions that are fixed-points of themselves

In general, a fixed-point of a function, $f$, is a point $x$ in the domain of $f$ such that $f(x) = x$.

In lambda calculus, a function can take a function, including itself, as input, so we can even ask: “is there a function that is its own fixed-point? That is, is there a function $f$ such that $f(f) = f$?”

So far we have found three sets/classes of functions that meet this criteria:

  1. $S_I = \{I\}$ where $I$ is the identity function, $(\lambda x.x)$
  2. $S_p = \{Pp\ |\ P \text{ is a fixed-point combinator and }$
    • $p = T = \lambda ab.a\}$
    • $p = T’ = \lambda ab.b\}$ (contributed by @mohottnad)

Since $Y$ (the $Y$-combinator) and $\Omega$ (Turing’s combinator) are each a fixed-point combinator, then $(YT) \in S_2$ and $(\Omega T) \in S_2$, meaning that $(YT)$ is its own fixed-point and $(\Omega T)$ is its own fixed-point.

Are there other classes of functions that are fixed-points of themselves?


Proof: $I$ is a fixed-point of itself

$$I(I) = I$$

Proof: $(PT)$ is a fixed-point of itself where $P$ is a fixed-point combinator and $p = T = (\lambda ab.a)$

\begin{align} (PT)(PT) &= (T(PT))(PT) \\ &= ((\lambda ab.a)(PT))(PT) \\ &= (\lambda b.PT)(PT) \\ &= (PT) \end{align}

Proof: $(PT’)$ is a fixed-point of itself where $P$ is a fixed-point combinator and $p = T’ = (\lambda ab.b)$

(contributed by @mohottnad)

\begin{align} (PT')(PT') &= (T'(PT'))(PT') \\ &= ((\lambda ab.b)(PT'))(PT') \\ &= (\lambda b.b)(PT') \\ &= (PT') \end{align}


At least I can think of another class following your line of reasoning where $T' = \lambda ab.b$, then we have: \begin{align} (PT')(PT') &= (T'(PT'))(PT') \\ &= ((\lambda ab.b)(PT'))(PT') \\ &= (\lambda b.b)(PT') \\ &= (PT') \end{align}

Please note besides Y-combinator and Turing combinator, we also have many other combinators as referenced here. Finally your requirement of fixed-point function $f$ here has the idempotent property, which can be intuitively the identity function $I$ and projection functions like the examples $T$ and $T'$ above...