Y is a least fixed point combinator
Logic
2025-04-29 v1
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.
Keywords
Cite
@article{arxiv.2504.19379,
title = {Y is a least fixed point combinator},
author = {Joseph Helfer},
journal= {arXiv preprint arXiv:2504.19379},
year = {2025}
}