Confluence in non-left-linear higher-order theories
Résumé
We develop techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs for higher-order rewrite rules extending betareduction on pure lambda-terms. We show that confluence is preserved for a large subset of terms that contains all pure lambda terms. Our results are applied to famous Klop's examples of non-confluent behaviours in lambda-calculi with convergent rewrite rules, on the one hand, and to fragments of an encoding in a dependent type theory augmented with rewrite rules of the Calculus of Constructions with polymorphic universes. on the other hand.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)