Introducing Quantification into a Hierarchical Graph Rewriting Language

TL;DR

This paper extends the hierarchical graph rewriting language LMNtal to QLMNtal by integrating quantifiers, enabling more expressive high-level modeling with logical constructs like universality and cardinality.

Contribution

Introduction of quantifiers into LMNtal's graph rewriting language, with a term-based syntax and integrated semantics for enhanced expressiveness.

Findings

Supports universal quantification, cardinality, and non-existence.

Allows nested and combined use of quantifiers in rewrite rules.

Semantics smoothly integrated into existing language framework.

Abstract

LMNtal is a programming and modeling language based on hierarchical graph rewriting that uses logical variables to represent connectivity and membranes to represent hierarchy. On the theoretical side, it allows logical interpretation based on intuitionistic linear logic; on the practical side, its full-fledged implementation supports a graph-based parallel model checker and has been used to model diverse applications including various computational models. This paper discuss how we extend LMNtal to QLMNtal (LMNtal with Quantification) to further enhance the usefulness of hierarchical graph rewriting for high-level modeling by introducing quantifiers into rewriting as well as matching. Those quantifiers allows us to express universal quantification, cardinality and non-existence in an integrated manner. Unlike other attempts to introduce quantifiers into graph rewriting, QLMNtal has term-based syntax, whose semantics is smoothly integrated into the small-step semantics of the base language LMNtal. The proposed constructs allow combined and nested use of quantifiers within individual rewrite rules.