Layer Systems for Confluence—Formalized
Bertram Felgenhauer, Franziska Rapp · Lecture notes in computer science · 2018
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.