= Solution
By assumption the set of <combinator>[combinators] is <recursively enumerable set>[recursively enumerable]. Finite <beta reduction> sequences, and hence finite certificates of <beta equivalence>, are also recursively enumerable.
For a closed term $Y$, choose a fresh variable $f$. The term $Y$ is a fixed-point combinator exactly when
$$
Yf\equiv_\beta f(Yf).
$$
Indeed, substitution then gives the required equivalence for every $F$, and the forward direction follows by taking $F=f$. <Dovetailing>[Dovetail] the enumeration of closed terms with all finite beta-equivalence certificates. Whenever a certificate of the displayed equivalence is found, output $Y$. This enumerates exactly the fixed-point combinators, proving <recursively enumerable fixed-point combinators>.
Back to article page
