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
相关论文
共 9 条
  • [1] 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
  • [2] CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
    Shintani, Kiraku
    Hirokawa, Nao
    AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 127 - 136
  • [3] 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
  • [4] Termination for direct sums of left-linear complete term rewriting systems
    Toyama, Y
    Klop, JW
    Barendregt, HP
    JOURNAL OF THE ACM, 1995, 42 (06) : 1275 - 1304
  • [5] First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
    Middeldorp, Aart
    Lochmann, Alexander
    Mitterwallner, Fabian
    JOURNAL OF AUTOMATED REASONING, 2023, 67 (02)
  • [6] Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems
    Kikuchi, Kentaro
    Aoto, Takahito
    Toyama, Yoshihito
    FRONTIERS OF COMBINING SYSTEMS (FROCOS 2017), 2017, 10483 : 115 - 131
  • [7] Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
    Dowek, Gilles
    Ferey, Gaspard
    Jouannaud, Jean-Pierre
    Liu, Jiaxiang
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2022, 32 (07) : 898 - 933
  • [8] First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
    Aart Middeldorp
    Alexander Lochmann
    Fabian Mitterwallner
    Journal of Automated Reasoning, 2023, 67
  • [9] Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite Systems
    Boichut, Yohan
    Pelletier, Vivien
    Rety, Pierre
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2016, 2016, 9942 : 64 - 81
1