research-article

Open access

A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL

Authors:

Bertram Felgenhauer,

Aart Middeldorp,

T. V. H. Prathamesh,

Franziska RappAuthors Info & Claims

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 132 - 143

https://doi.org/10.1145/3293880.3294098

Published: 14 January 2019 Publication History

Abstract

It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RR_n relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.

References

[1]

F. Baader and T. Nipkow. 1998. Term Rewriting and All That. Cambridge University Press.

Digital Library

[2]

S. Berghofer, L. Bulwahn, and F. Haftmann. 2009. Turning Inductive into Equational Specifications. In Proc. 22nd TPHOLs (LNCS), Vol. 5674. 131–146.

Digital Library

[3]

H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. 2008. Tree Automata Techniques and Applications. http://www.grappa.univ-lille3.fr/tata

[4]

H. Comon, G. Godoy, and R. Nieuwenhuis. 2001. The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. In Proc. 42nd FOCS. 298–307.

Digital Library

[5]

M. Dauchet, T. Heuillard, P. Lescanne, and S. Tison. 1990. Decidability of the Confluence of Finite Ground Term Rewriting Systems and of Other Related Term Rewriting Systems. I&C 88, 2 (1990), 187–201.

Digital Library

[6]

M. Dauchet and S. Tison. 1985. Decidability of Confluence for Ground Term Rewriting Systems. In Proc. 5th FCT (LNCS), Vol. 199. 80–84.

Digital Library

[7]

M. Dauchet and S. Tison. 1990. The Theory of Ground Rewrite Systems is Decidable. In Proc. 5th LICS. 242–248.

[8]

M. Dauchet, S. Tison, T. Heuillard, and P. Lescanne. 1987. Decidability of the Confluence of Ground Term Rewriting Systems. In Proc. 2nd LICS. 353–359.

[9]

B. Felgenhauer. 2012. Deciding Confluence of Ground Term Rewrite Systems in Cubic Time. In Proc. 23rd RTA (LIPIcs), Vol. 15. 165–175.

[10]

B. Felgenhauer, M. Avanzini, and C. Sternagel. 2013. A Haskell Library for Term Rewriting. CoRR abs/1307.2328 (2013). http://arxiv.org/abs/ 1307.2328

[11]

B. Felgenhauer, A. Middeldorp, T. V. H. Prathamesh, and F. Rapp. 2018. Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL. In Proc. 7th IWC. 46–50. Available at http://cl-informatik.uibk.ac.at/iwc/iwc2018.pdf .

[12]

B. Felgenhauer and F. Rapp. 2018. Layer Systems for Confluence – Formalized. In Proc. 15th ICTAC (LNCS), Vol. 11187. 1–19.

[13]

G. Godoy and A. Tiwari. 2005. Confluence of Shallow Right-Linear Rewrite Systems. In Proc. 14th CSL (LNCS), Vol. 3634. 541–556.

Digital Library

[14]

G. Godoy, A. Tiwari, and R. Verma. 2004. Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems. AAECC 15 (2004), 13–36.

[15]

F. Haftmann and T. Nipkow. 2010. Code Generation via Higher-Order Rewrite Systems. In Proc. 10th FLOPS (LNCS), Vol. 6009. 103–117.

Digital Library

[16]

L. Kaiser. 2005. Confluence of Right Ground Term Rewriting Systems is Decidable. In Proc. 8th FoSSaCS (LNCS), Vol. 3441. 470–489.

Digital Library

[17]

P. Lammich. 2013. Automatic Data Refinement. In Proc. 4th ITP (LNCS), Vol. 7998. 84–99.

Digital Library

[18]

M. Oyamaguchi. 1987. The Church-Rosser Property for Quasi-Ground Term Rewriting Systems. Technical Report. Faculty of Engineering, Mie University, Japan.

[19]

F. Rapp and A. Middeldorp. 2016. Automating the First-Order Theory of Left-Linear Right-Ground Term Rewrite Systems. In Proc. 1st FSCD (LIPIcs), Vol. 52. 36:1–36:12.

[20]

F. Rapp and A. Middeldorp. 2016. Confluence Properties on Open Terms in the First-Order Theory of Rewriting. In Proc. 5th IWC. 26–30. Available at http://cl-informatik.uibk.ac.at/iwc/iwc2016.pdf .

[21]

F. Rapp and A. Middeldorp. 2018. FORT 2.0. In Proc. 9th IJCAR (LNAI), Vol. 10900. 81–88.

[22]

R. Thiemann and C. Sternagel. 2009. Certification of Termination Proofs using CeTA. In Proc. 22nd TPHOLs (LNCS), Vol. 5674. 452–468.

Digital Library

[23]

Y. Toyama. 1987. On the Church-Rosser Property for the Direct Sum of Term Rewriting Systems. J. ACM 34, 1 (1987), 128–143.

Digital Library

Cited By

Middeldorp ALochmann AMitterwallner F(2023)First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, CertificationJournal of Automated Reasoning10.1007/s10817-023-09661-767:2Online publication date: 6-Apr-2023
https://doi.org/10.1007/s10817-023-09661-7
Lochmann AMiddeldorp AMitterwallner FFelgenhauer BHriţcu CPopescu A(2021)A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systemsProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439918(250-263)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439918
Mitterwallner FLochmann AMiddeldorp AFelgenhauer B(2021)Certifying Proofs in the First-Order Theory of RewritingTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72013-1_7(127-144)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72013-1_7
Show More Cited By

Index Terms

A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL
1. Theory of computation
  1. Formal languages and automata theory
    1. Tree languages
  2. Logic
    1. Equational logic and rewriting
    2. Logic and verification

Recommendations

Simultaneous checking of completeness and ground confluence for algebraic specifications

Algebraic specifications provide a powerful method for the specification of abstract data types in programming languages and software systems. Completeness and ground confluence are fundamental notions for building algebraic specifications in a correct ...
A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems
CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs

The first-order theory of rewriting is a decidable theory for finite left-linear right-ground rewrite systems, implemented in FORT. We present a formally verified variant of the decision procedure for the class of linear variable-separated rewrite ...
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
Abstract
The first-order theory of rewriting is decidable for linear variable-separated rewrite systems. We present a new decision procedure which is the basis of FORT, a decision and synthesis tool for properties expressible in the theory. The decision ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2019

261 pages

ISBN:9781450362221

DOI:10.1145/3293880

Program Chairs:
Assia Mahboubi
INRIA, France
,
Magnus O. Myreen
Chalmers University of Technology, Sweden

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution-NonCommercial International 4.0 License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CPP '19

Sponsor:

SIGPLAN

CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 14 - 15, 2019

Cascais, Portugal

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
314
Total Downloads

Downloads (Last 12 months)39
Downloads (Last 6 weeks)5

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Middeldorp ALochmann AMitterwallner F(2023)First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, CertificationJournal of Automated Reasoning10.1007/s10817-023-09661-767:2Online publication date: 6-Apr-2023
https://doi.org/10.1007/s10817-023-09661-7
Lochmann AMiddeldorp AMitterwallner FFelgenhauer BHriţcu CPopescu A(2021)A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systemsProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439918(250-263)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439918
Mitterwallner FLochmann AMiddeldorp AFelgenhauer B(2021)Certifying Proofs in the First-Order Theory of RewritingTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72013-1_7(127-144)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72013-1_7
Lochmann AMiddeldorp A(2020)Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of RewritingTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45237-7_11(178-194)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45237-7_11

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents