English

Fixed point combinators as fixed points of higher-order fixed point generators

Logic in Computer Science 2023-06-22 v3

Abstract

Corrado B\"ohm once observed that if YY is any fixed point combinator (fpc), then Y(λyx.x(yx))Y(\lambda yx.x(yx)) is again fpc. He thus discovered the first "fpc generating scheme" -- a generic way to build new fpcs from old. Continuing this idea, define an fpc generator\textit{fpc generator} to be any sequence of terms G1,,GnG_1,\dots,G_n such that YFPCYG1GnFPC Y \in FPC \Rightarrow Y G_1 \cdots G_n \in FPC In this contribution, we take first steps in studying the structure of (weak) fpc generators. We isolate several robust classes of such generators, by examining their elementary properties like injectivity and (weak) constancy. We provide sufficient conditions for existence of fixed points of a given generator (G1,,Gn)(G_1,\cdots,G_n): an fpc YY such that Y=YG1GnY = Y G_1 \cdots G_n. We conjecture that weak constancy is a necessary condition for existence of such (higher-order) fixed points. This statement generalizes Statman's conjecture on non-existence of "double fpcs": fixed points of the generator (G)=(λyx.x(yx))(G) = (\lambda yx.x(yx)) discovered by B\"ohm. Finally, we define and make a few observations about the monoid of (weak) fpc generators. This enables us to formulate new a conjecture about their structure.

Cite

@article{arxiv.1810.02239,
  title  = {Fixed point combinators as fixed points of higher-order fixed point generators},
  author = {Andrew Polonsky},
  journal= {arXiv preprint arXiv:1810.02239},
  year   = {2023}
}
R2 v1 2026-06-23T04:28:32.888Z