Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination

Kento Takyu, Kazunori Ueda

TL;DR

The paper tackles designing a practical high-level declarative language for hierarchical graph rewriting by leveraging MELL proof nets as a canonical guide for managing box-structured graphs. It extends LMNtal with aggregates of process contexts and a mell library to support cloning and deletion of promotion boxes, enabling faithful encoding of MELL cut-elimination rules. It demonstrates the encoding of MELL proof nets and their reduction rules within the extended LMNtal framework and validates the approach with state-space exploration and a model-checking toolchain, including an example for Ambient Calculus to show generality. The result is a versatile workbench for proof nets and for experiments with box-based concurrency and hierarchical graph rewriting.

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 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.

Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination

TL;DR

The paper tackles designing a practical high-level declarative language for hierarchical graph rewriting by leveraging MELL proof nets as a canonical guide for managing box-structured graphs. It extends LMNtal with aggregates of process contexts and a mell library to support cloning and deletion of promotion boxes, enabling faithful encoding of MELL cut-elimination rules. It demonstrates the encoding of MELL proof nets and their reduction rules within the extended LMNtal framework and validates the approach with state-space exploration and a model-checking toolchain, including an example for Ambient Calculus to show generality. The result is a versatile workbench for proof nets and for experiments with box-based concurrency and hierarchical graph rewriting.

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 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.

Paper Structure

This paper contains 33 sections, 22 equations, 23 figures, 1 table.

Table of Contents

  1. Introduction
  2. LMNtal: A Hierarchical Graph Rewriting Language
  3. Overview of LMNtal
  4. Nonlinear membranes
  5. MELL Proof Nets
  6. Proof Structure and Proof Nets
  7. Cut Elimination
  8. Refining LMNtal's Box Constructs
  9. Extension of LMNtal Syntax: Aggregates of Process Contexts
  10. API rules supporting typical use cases
  11. Copying a membrane with a bundle of free links
  12. Deleting a membrane with a bundle of free links
  13. Implementation
  14. Examples of Encoding
  15. Encoding of MELL Proof Nets and Cut Elimination Rules
  16. ...and 18 more sections

Figures (23)

  • Figure 1: Syntax of LMNtal.
  • Figure 2: Rewriting an LMNtal graph using process contexts and bundles. An arrowhead of each non-unary atom indicates the first argument and the ordering of atoms.
  • Figure 3: Operations of the nlmem library.
  • Figure 4: The components of MELL proof structure.
  • Figure 5: Examples of MELL proof nets, where applying cut elimination to (a) results in (b) (See Sect.\ref{['subsection: example-beta-reduction']} also).
  • ...and 18 more figures

Theorems & Definitions (3)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition: MELL formula