Skip to Main content Skip to Navigation
Conference papers

Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories

Gaspard Férey 1 Jean-Pierre Jouannaud 1 
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03126115
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Tuesday, September 14, 2021 - 4:09:14 PM
Last modification on : Friday, August 5, 2022 - 2:58:08 PM

File

ppdp2021-9.pdf
Files produced by the author(s)

Identifiers

Citation

Gaspard Férey, Jean-Pierre Jouannaud. Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories. PPDP 2021 - 23rd International Symposium on Principles and Practice of Declarative Programming, Sep 2021, Tallin, Estonia. ⟨10.1145/3479394.3479403⟩. ⟨hal-03126115v6⟩

Share

Metrics

Record views

246

Files downloads

438