The contribution of this paper is twofold.

First, we derive a complete characterization of all *simply-typed* **fixed-point combinator (fpc) generators** using *Barendregt's Inhabitation Machines*.
A fpc generator is a lambda term \( G \) such that \( Y G \) is a fpc whenever \( Y \) is.
The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan's Owl, is a famous fpc generator.
For instance, Turing's fpc \( Y_1 \) can be obtaind from Curry's fpc \( Y_0 \) by postfixing \( \delta \): \[ Y_1 = Y_0 \delta \]

Second, we present a conjecture that vastly generalises Richard Statman's question on the existance of double fixed-point combinators. Statman asked whether there is a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \). This question remains open as the proof by Benedetto Intrigila contains a gap. We have the following conjecture about the relation of the \( \mu \)-opertator and fixed-point combinators:

Conjecture

We conjecture that for any fixed-point combinator \( Y \) and simply-typed \( \lambda\mu \)-terms \( s,t \) it holds that
\[ s =_{ \beta \mu } t \iff s_Y =_{ \beta } t_Y \]
where \(s_Y, t_Y\) are the *untyped* lambda terms obtained from \(s,t\), respectively, by replacing all occurrences of \( \mu \)-operators with the fixed-point combinator \( Y \).

See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

} }