A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems

被引：3

作者：

Kohl, Christina ^{[1
]}

Middeldorp, Aart ^{[1
]}

机构：

[1] Univ Innsbruck, Dept Comp Sci, Innsbruck, Austria

来源：

PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2023 | 2023年

基金：

奥地利科学基金会;

关键词：

formalization; term rewriting; confluence; DECREASING DIAGRAMS; CONFLUENCE;

D O I：

10.1145/3573105.3575667

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Several critical pair criteria are known that guarantee confluence of left-linear term rewrite systems. The correctness of most of these have been formalized in a proof assistant. An important exception has been the development closedness criterion of van Oostrom. Its proof requires a high level of understanding about overlapping redexes and descendants as well as several intermediate results related to these concepts. We present a formalization in the proof assistant Isabelle/HOL. The result has been integrated into the certifier CeTA

引用

页码：197 / 210

页数：14

共 35 条

[1] CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
Shintani, Kiraku
Hirokawa, Nao
AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 127 - 136
[2] Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
Nagele, Julian
Middeldorp, Aart
INTERACTIVE THEOREM PROVING (ITP 2016), 2016, 9807 : 290 - 306
[3] A property of left-linear rewrite systems preserving recognizability
Gyenizse, P
Vágvölgyi, S
THEORETICAL COMPUTER SCIENCE, 2000, 242 (1-2) : 477 - 498
[4] Strong sequentiality of left-linear overlapping rewrite systems
Jouannaud, JP
Sadfi, W
CONDITIONAL AND TYPED REWRITING SYSTEMS, 1995, 968 : 235 - 246
[5] Generalizing Newman's lemma for left-linear rewrite systems
Gramlich, Bernhard
Lucas, Salvador
TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2006, 4098 : 66 - 80
[6] Within ARM's reach: Compilation of left-linear rewrite systems via minimal rewrite systems
Fokkink, W
Kamperman, J
Walters, P
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1998, 20 (03): : 679 - 706
[7] Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Kirk, Christina
Middeldorp, Aart
PROCEEDINGS OF THE 14TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2025, 2025, : 156 - 170
[8] Reduction strategies for left-linear term rewriting systems
Toyama, Y
PROCESSES, TERMS AND CYCLES: STEPS ON THE ROAD TO INFINITY: ESSAYS DEDICATED TO JAN WILLEM KLOP ON THE OCCASION OF HIS 60TH BIRTHDAY, 2005, 3838 : 198 - 223
[9] SIMULATION OF TURING-MACHINES BY A LEFT-LINEAR REWRITE RULE
DAUCHET, M
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 355 : 109 - 120
[10] Decidability for left-linear growing term rewriting systems
Nagaya, T
Toyama, Y
INFORMATION AND COMPUTATION, 2002, 178 (02) : 499 - 514

← 1 2 3 4 →