Confluence in (Un)Typed Higher-Order Theories by means of Critical Pairs
Gaspard Férey, Jean-Pierre Jouannaud · HAL (Le Centre pour la Communication Scientifique Directe) · 2019
In a series of papers, we develop techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending β-reduction on pure λ-terms. The present paper concentrates on the case of left-linear rewrite rules, assuming that critical pairs can be joined without explicit beta-reduction steps.