On the Stability by Union of Reducibility Candidates

Colin Riba (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

We investigate some aspects of proof methods for the termination of (extensions of) the second-order lambda-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 wrt a weak observational preorder. We show that this is the case for the Curry-style second-order lambda-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.

Mots clés: lambda-calcul; types unions; types existentiels; normalisation forte

Domaines: Logique en informatique [cs.LO]

Colin Riba. On the Stability by Union of Reducibility Candidates. 10th International Conference on Foundations of Software Science and Computational Structures - FoSSaCS 2007, 2007, Braga, Portugal. pp.317-331, ⟨10.1007/978-3-540-71389-0⟩. ⟨hal-00123116v2⟩