On the number of fixed points of a combinator in lambda calculus

The paper addresses the following question: how many solutions are there to an arbitrary fixpoint equation of a combinator, i.e. a closed lambda term? This appears to be a new question that has not yet been discussed in the literature. The authors name this question NFP (Number of Fixed Points) and give a partial answer to it: they show that for those (systems of) fixpoint equations that possess a solution in normal form, there is either a unique solution or there are infinitely many solutions. However, they leave general question unsolved. This result is similar to but distinct from the Range Theorem that was proved by \textit{H. Barendregt}, using recursion theoretic arguments, in ``Constructive proofs of the range property in lambda calculus [Theor. Comput. Sci. 121, 59-69 (1993; Zbl 0796.03020)]. In particular, the authors point out in an appendix that a recursion theoretic approach to proving their result does not appear to be feasible. They therefore use a constructive, purely syntactical approach to show their result. This constructive approach terminates after a finite number of transformations because the considered fixpoint equations possess a solution in normal form. The paper is clearly structured and guides the reader through the sometimes very syntactical parts by giving simple examples for each of the transformations of the main construction. Sections are typically introduced with a paragraph that informally describes the main argument of this section. The paper presupposes familiarity with the syntax of lambda calculus but is otherwise independent of the deeper results in this area.

Recommendations

Cited in

(7)

This page was built for publication: On the number of fixed points of a combinator in lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4526150)