Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination
arXiv:2411.14802
The paper extends the LMNtal declarative language for hierarchical graph rewriting to support operations on promotion boxes from MELL proof nets, enabling implementation of cut elimination and providing a practical workbench for modeling concurrency.
Abstract
Hierarchical graph rewriting is a highly expressive computational formalism that manipulates graphs enhanced with box structures for representing hierarchies. It has provided the foundations of various graph-based modeling tools, but the design of high-level declarative languages based on hierarchical graph rewriting is still a challenge. For a solid design choice, well-established formalisms with backgrounds other than graph rewriting would provide useful guidelines. Proof nets of Multiplicative Exponential Linear Logic (MELL) is such a framework because its original formulation of cut elimination is essentially graph rewriting involving box structures, where the so-called promotion boxes with an indefinite number of non-local edges may be cloned, migrated and deleted. This work builds on LMNtal (pronounced "elemental") as a declarative language based on hierarchical (port) graph rewriting, and discusses how it can be extended to support the above operations on promotion boxes of MELL proof nets. LMNtal thus extended turns out to be a practical graph rewriting language that has a strong affinity with MELL proof nets. The language features provided are general enough to encode other well-established models of concurrency. Using the toolchain of LMNtal that provides state-space search and model checking, we implemented cut elimination rules of MELL proof nets in extended LMNtal and demonstrated that the platform could serve as a useful workbench for proof nets.
Extended version of the PADL 2025 paper (LNCS, Springer, 2025). This version incorporates into the main text details omitted from the conference version and includes some additional material