Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
summary
Formalizes Okui’s 1998 sufficient condition for confluence of left‑linear term rewrite systems inside Isabelle/HOL, representing multisteps as proof terms, defining simultaneous critical pairs with unification restricted to linear left‑sides, and implementing an n‑ary join operation plus redex‑pattern extraction. The development is ~6,000 LOC, proves Oku’s criterion subsumes development‑closed critical pairs, and verifies algebraic properties (associativity, commutativity, identity). It is non‑executable so far (no verified algorithm to enumerate SCPs, so tool certification is not yet possible), AFP entry forthcoming, and heavy use of sledgehammer and locales simplifies proofs.
AI-written summary · about
chapters (13)
- 0:00Term rewriting basics
- 1:07Term rewriting examples
- 3:57Confluence in rewriting
- 6:43Uku’s criterion
- 8:54Simultaneous critical pairs
- 9:59Proof terms in Isabelle
- 12:13Join on proof terms
- 14:03Extending join operation
- 16:31Redex patterns
- 18:17Formalizing critical pairs
- 21:10Lessons from Isabelle
- 23:17Conclusion
- 24:53Q&A
related talks
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
17mFormalizing Determinacy of Concurrent Revisions
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
21mChecking Equivalence in a Non-strict Language
18mCompleteness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
15mCompiling with Continuations, Correctly
26mAlgorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
27mAugmenting Rewrite Rule Sets via Knuth-Bendix Completion