The fixed point property and a technique to harness double fixed point combinators

摘要

The lambda-calculus enjoys the property that each lambda-term has at least one fixed point, which is due to the existence of a fixed point combinator. It is unknown whether it enjoys the 'fixed point property' stating that each lambda-term has either one or infinitely many pairwise distinct fixed points. We show that the fixed point property holds when considering possibly open fixed points. The problem of counting fixed points in the closed setting remains open, but we provide sufficient conditions for a lambda-term to have either one or infinitely many fixed points. In the main result of this paper we prove that in every sensible lambda-theory there exists a lambda-term that violates the fixed point property.We then study the open problem concerning the existence of a double fixed point combinator and propose a proof technique that could lead towards a negative solution. We consider interpretations of the lambda Y-calculus into the lambda-calculus together with two reduction extension properties, whose validity would entail the non-existence of any double fixed point combinators. We conjecture that both properties hold when typed lambda Y-terms are interpreted by arbitrary fixed point combinators. We prove reduction extension property I for a large class of fixed point combinators.Finally, we prove that the lambda Y-theory generated by the equation characterizing double fixed point combinators is a conservative extension of the lambda-calculus.