Bluebird and mockingbird combinators cannot create fixed-point functions
Bluebirds and mockingbirds cannot produce a fixed-point combinator
Logic in Computer Science
Summary
This paper solves a long-standing question about certain building blocks of computer programs called combinators. The authors show that two particular combinators, known as bluebird and mockingbird, cannot be used together to create a fixed-point combinator, which is a tool that lets programs call themselves repeatedly. They developed a way to track variables during the program transformations to prove this. This means a class of programming tools has intrinsic limitations.
What this means in practice
- •For functional programmers: Recognize limitations when constructing recursion using only bluebird, mockingbird, and identity combinators to avoid dead-end design approaches.
- •For programming language designers: Avoid relying on fixed-point combinators in core calculi that only include bluebird, mockingbird, and identity combinators during language semantics design.
A theory result. No direct application yet.
Authors
Takuma Imamura
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 identitybird combinator with reduction rule $Ix \to_{w} x$. 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) \neq \mathrm{Tr}_{x}\left(x^{r}\left( Yx \right)\right)$ for every $x$-free $BMI$-term $Y$ and every $r\geq 1$. Consequently, there exists no fixed-point combinator in $BMI$-combinatory logic under weak equivalence. This provides a negative answer to the problem posed by Smullyan in 1985.