Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa, Dohan Kim, Kiraku Shintani, René ThiemannProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), 2024.
Abstract
Parallel critical pairs (PCPs) have been used to design sufficient criteria for confluence of term rewrite systems. In this work we formalize PCPs and the criteria of Gramlich, Toyama, and Shintani and Hirokawa in the proof assistant Isabelle. In order to reduce the amount of bureaucracy we deviate from the paper-definition of PCPs, i.e., we switch from a position-based definition to a context-based definition. This switch not only simplifies the formalization task, but also gives rise to a simple recursive algorithm to compute PCPs. We further generalize all mentioned criteria from confluence to commutation and integrate them in the certifier CeTA, so that it can now validate confluence- and commutation-proofs based on PCPs. Because of our results, CeTA is now able to certify proofs by the automatic confluence tool Hakusan, which makes heavy use of PCPs. These proofs include term rewrite systems for which no previous certified confluence proof was known.
BibTeX
@inproceedings{DBLP:conf/cpp/HirokawaKST24,
author = {Nao Hirokawa and
Dohan Kim and
Kiraku Shintani and
Ren{\’{e}} Thiemann},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Certification of Confluence- and Commutation-Proofs via Parallel Critical
Pairs},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {147—161},
publisher = {{ACM}},
url = {https://doi.org/10.1145/3636501.3636949},
doi = {10.1145/3636501.3636949},
year = {2024}
}