Showing 1–1 of 1 results for author: Mishina, H

Introducing Quantification into a Hierarchical Graph Rewriting Language

Authors: Haruto Mishina, Kazunori Ueda

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… ▽ More 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. △ Less

Submitted 17 September, 2024; originally announced September 2024.

Comments: Extended version (with Appendix) of the paper presented at the 34th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2024), Milano, Italy, September 2024, LNCS 14919, Springer-Verlag, pp.220-239. 26 pages