Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Confluence in non-left-linear higher-order theories

Gaspard Férey 1 Jean-Pierre Jouannaud 1
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification
Abstract : 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Wednesday, March 3, 2021 - 6:00:29 PM
Last modification on : Friday, March 19, 2021 - 12:26:02 PM


Files produced by the author(s)


  • HAL Id : hal-03126115, version 3


Gaspard Férey, Jean-Pierre Jouannaud. Confluence in non-left-linear higher-order theories. 2021. ⟨hal-03126115v3⟩



Record views


Files downloads