Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
On the Stability by Union of Reducibility Candidates
verfasst von : Colin Riba
Erschienen in: Foundations of Software Science and Computational Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We investigate some aspects of proof methods for the termination of (extensions of) the second-order
λ
-calculus in presence of union and existential types.
We prove that Girard’s reducibility candidates are stable by union iff they are exactly the non-empty sets of terminating terms which are downward-closed w.r.t. a weak observational preorder.
We show that this is the case for the Curry-style second-order
λ
-calculus. As a corollary, we obtain that reducibility candidates are exactly the Tait’s saturated sets that are stable by reduction. We then extend the proof to a system with product, co-product and positive iso-recursive types.