Y is a least fixed point combinator
Joseph Helfer
TL;DR
The paper addresses whether the Curry fixed-point combinator $Y$ yields least fixed points of a term $F$ under a natural order on lambda terms defined by beta-normal-form behavior. It develops a constructive, parallel-reduction framework that uses a formal fixed point symbol and an extended language with fresh variables to simulate reductions of $Y F$ alongside arbitrary fixed points, via a gamma-mapping that preserves reduction structure. The main result shows that $Y F$ is minimal among fixed points for both $β$- and $beta$-eta reductions, and the method extends to other fixed-point combinators such as Theta. This clarifies the behavior of recursion in the lambda-calculus and informs semantics in models with a partial-order structure, suggesting broader applicability to fixed-point combinators.
Abstract
The theory of recursive functions is related in a well-known way to the notion of *least fixed points*, by endowing a set of partial functions with an ordering in terms of their domain of definition. When terms in the pure lambda-calculus are considered as partial functions on the set of reduced lambda-terms, they inherit such a partial order. We prove that Curry's well-known fixed point combinator Y produces least fixed points with respect to this partial order.