Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination
summary
Extends Elemental (LMNtal-based) with an M API that implements graph cloning/division inspired by MELL promotion boxes, including a concrete primitive M_Copy that preserves link consistency; encodes all six cut-elimination rules of MELL proof nets each as a single Elemental rule; integrates with the existing LMNtal toolchain to build and visualize full state spaces and to run model checking; reproduces confluence, stability and strong normalization, and shows a concrete counterexample where adding an unrestricted rule increases final states from one to four, demonstrating the platform works as a proof-net workbench.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:04Hierarchical graphs and Elemental
- 3:38Design contributions and M proof Nets
- 5:05Elemental syntax and constructs
- 8:28Subgraph cloning and membranes
- 10:17M proof Nets examination
- 14:20M API design and implementation
- 17:14Encoding M proof Nets in Elemental
- 20:07State space visualization
- 21:57Adding rules and confluence
- 22:17Encoding process calculi
- 23:03Conclusion
related talks
17mMu tilde (re)cycled
38mE-graphs and Automated Reasoning: Looking back to look forward
21mChecking Equivalence in a Non-strict Language
19mDestructive E-Graph Rewrites
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
15mA Semantic Framework for PEGs
15mHEC: Equivalence Verification Checking for Code Transformation via Equality...
21mVerifying term graph optimizations using Isabelle/HOL