Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2022

Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Résumé

User-de ned higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. is raises the question of proving that they preserve the properties of β-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom's decreasing diagrams that reduce con uence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, con uence of a terminating set of le-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. e present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pars. e rewrite relation used for analyzing con uence, called orthogonal, gives rise to critical pairs, called nested, that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. is second paper terminates our investigation of con uence in the case of le-linear rules.
Fichier principal
Vignette du fichier
confluence-of-left-linear-higher-order-rewrite-theories-by-checking-their-nested-critical-pairs.pdf (844.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03126111 , version 1 (02-02-2021)
hal-03126111 , version 2 (21-07-2021)
hal-03126111 , version 3 (21-03-2022)

Licence

Paternité

Identifiants

Citer

Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Mathematical Structures in Computer Science, 2022, pp.1-36. ⟨10.1017/S0960129522000044⟩. ⟨hal-03126111v3⟩
260 Consultations
366 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More