A Small-Step Operational Semantics for GP 2

Brian Courtehoute
(University of York, United Kingdom)
Detlef Plump
(University of York, United Kingdom)

The operational semantics of a programming language is said to be small-step if each transition step is an atomic computation step in the language. A semantics with this property faithfully corresponds to the implementation of the language. The previous semantics of the graph programming language GP 2 is not fully small-step because the loop and branching commands are defined in big-step style. In this paper, we present a truly small-step operational semantics for GP 2 which, in particular, accurately models diverging computations. To obtain small-step definitions of all commands, we equip the transition relation with a stack of host graphs and associated operations. We prove that the new semantics is non-blocking in that every computation either diverges or eventually produces a result graph or the failure state. We also show the finite nondeterminism property, viz. that each configuration has only a finite number of direct successors. The previous semantics of GP 2 is neither non-blocking nor does it have the finite nondeterminism property. We also show that, for a program and a graph that terminate, both semantics are equivalent, and that the old semantics can be simulated with the new one.

In Berthold Hoffmann and Mark Minas: Proceedings Twelfth International Workshop on Graph Computational Models (GCM 2021), Online, 22nd June 2021, Electronic Proceedings in Theoretical Computer Science 350, pp. 89–110.
Published: 21st December 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.350.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org