Bluebirds and mockingbirds cannot produce a fixed-point combinator

Abstract

Let B be the bluebird combinator with reduction rule Bxyz →_w x(yz), let M be the mockingbird combinator with reduction rule Mx →_w xx, and let I be the identity bird combinator with reduction rule Ix →_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(Yx) under these reduction rules. For a fixed variable x, we construct an invariant Tr_x(u) of a BMI-term u with respect to →_w. This invariant traces the occurrences of x in the leftmost-innermost reduction sequence of u. We then prove that Tr_x(Yx) ≠ Tr_x(x^r( Yx )) for every x-free BMI-term Y and every r≥ 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.

Lens spaces that cannot be obtained by two integral surgeries
Marco Golla, Marc Kegel
arXiv19 Oct 2026PreprintCC BY 4.0Full textGeometry & topologyarXivHAL
Bayesian Hierarchical Modeling Approaches for Combining Information From Multiple Data Sources to Produce Annual Estimates of National Immunization Coverage.
C Edson Utazi, Warren C Jochem, M Carolina Danovaro-Holliday +4
Biometrical journal. Biometrische Zeitschrift1 Oct 2026Peer-reviewedCC BYFull textStatisticsEurope PMC
Families of knots that cannot be made Legendrian parametrically
Javier Martínez-Aguinaga
arXiv16 Sep 2026PreprintarXiv licenceFull textGeometry & topologyarXiv
A diameter-one set in ℝ⁵ that cannot be covered by six diameter-one balls
A. Arman, A. Bondarenko, A. Prymak +1
arXiv5 Nov 2026PreprintarXiv licenceFull textGeometry & topologyarXiv
Sequential and distributive dual futile cycle: Hopf bifurcation can occur under parameter-rich kinetics but cannot occur under mass action kinetics
Nicola Vassena
arXiv14 Sep 2026PreprintarXiv licenceFull textSystems & synthetic biology Dynamical systemsarXiv

Cite

BibTeX RIS

BibTeX

@misc{imamura2026bluebirds,
  title = {{Bluebirds and mockingbirds cannot produce a fixed-point combinator}},
  author = {Takuma Imamura},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2609.21765},
  eprint = {2609.21765},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.21765},
  note = {CC BY 4.0},
}

RIS

TY  - UNPB
TI  - Bluebirds and mockingbirds cannot produce a fixed-point combinator
AU  - Takuma Imamura
PY  - 2026
DA  - 2026/10/14
PB  - arXiv
DO  - 10.48550/arxiv.2609.21765
UR  - https://arxiv.org/abs/2609.21765
AB  - Let B be the bluebird combinator with reduction rule Bxyz →_w x(yz), let M be the mockingbird combinator with reduction rule Mx →_w xx, and let I be the identity bird combinator with reduction rule Ix →_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(Yx) under these reduction rules. For a fixed variable x, we construct an invariant Tr_x(u) of a BMI-term u with respect to →_w. This invariant traces the occurrences of x in the leftmost-innermost reduction sequence of u. We then prove that Tr_x(Yx) ≠ Tr_x(x^r( Yx )) for every x-free BMI-term Y and every r≥ 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.
ER  -

Abstract

Related

Cite