Bluebirds and mockingbirds cannot produce a fixed-point combinator

Abstract

Let $B$ be the bluebird combinator with reduction rule $Bxyz{\to }_{w}x\left(yz\right)$, let $M$ be the mockingbird combinator with reduction rule $Mx{\to }_{w}xx$, and let $I$ be the identity bird combinator with reduction rule $Ix{\to }_{w}x$. A fixed-point combinator, called a sage bird by Smullyan, is a closed term $Y$ such that, for a fresh variable $x$, $Yx$ is equivalent to $x\left(Yx\right)$ under these reduction rules. For a fixed variable $x$, we construct an invariant ${\mathrm{Tr}}_x\left(u\right)$ of a $BMI$-term $u$ with respect to ${\to }_w$. This invariant traces the occurrences of $x$ in the leftmost-innermost reduction sequence of $u$. We then prove that ${\mathrm{Tr}}_x\left(Yx\right)\ne {\mathrm{Tr}}_x\left(x^r\left(Yx\right)\right)$ for every $x$-free $BMI$-term $Y$ and every $r\ge 1$. Consequently, there exists no fixed-point combinator in $BMI$-combinatory logic. This provides a negative answer to the problem posed by Smullyan in 1985.

arXiv commentRevised