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 so-called Promotion Boxes with an indefinite number of non-local edges may be cloned, migrated and deleted. This work builds on LMNtal 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 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.

翻译：分层图重写是一种高表达力的计算形式体系，通过增强图结构中的盒状机制来表示层级关系。该体系为多种基于图的建模工具提供了理论基础，然而设计基于分层图重写的高层声明式语言仍是一项挑战。为确保设计选择的可靠性，具有非图重写背景的成熟形式体系能提供有益指导。乘法指数线性逻辑（MELL）的证明网正是这样一种框架，其原始cut elimination形式本质上涉及包含盒状结构的图重写操作——其中具有不定数量非局部边的所谓提升盒（Promotion Boxes）可被克隆、迁移和删除。本研究以基于分层（端口）图重写的声明式语言LMNtal为基础，探讨如何扩展该语言以支持上述MELL证明网中提升盒的操作。扩展后的LMNtal成为与MELL证明网具有高度亲和性的实用图重写语言，其提供的语言特性足以编码其他成熟的并发模型。我们利用提供状态空间搜索与模型检查功能的LMNtal工具链，在扩展后的LMNtal中实现了MELL证明网的cut elimination规则，并验证了该平台可作为证明网研究的有用工作台。