Abstract

Toyama’s theorem states that the union of two confluent term rewrite systems with disjoint signatures is again confluent. This is a fundamental result in term rewriting, and several proofs appear in the literature. The underlying proof technique has been adapted to prove further results like persistence of confluence (if a many-sorted term rewrite system is confluent, then the underlying unsorted system is confluent) or the preservation of confluence by currying.

In this paper we present a formalization of modularity and related results in Isabelle/HOL. The formalization is based on layer systems, which cover modularity, persistence, currying (and more) in a single framework. The persistence result has been integrated into the certifier CeTA and the confluence tool CSI, allowing us to check confluence proofs based on persistent decomposition, of which modularity is a special case.

BibTeX

@inproceedings{BFFR-ICTAC18,
 author    = "Bertram Felgenhauer and Franziska Rapp",
 title     = "Layer Systems for Confluence---Formalized",
 booktitle = "Proceedings of the 15th International Colloquium on Theoretical
              Aspects of Computing -- ICTAC 2018",
 editor    = "Bernd Fischer and Tarmo Uustalu",
 series    = "Lecture Notes in Computer Science",
 volume    = 11187,
 oages     = "173--190",
 year      = 2018,
 doi       = "10.1007/978-3-030-02508-3_10"
}