A Small-Step Operational Semantics for GP 2

TL;DR

This paper introduces a fully small-step operational semantics for GP 2, accurately modeling diverging computations and ensuring properties like non-blocking behavior and finite nondeterminism, improving upon previous semantics.

Contribution

It presents the first truly small-step semantics for GP 2, including divergence modeling and proof of key properties, aligning semantics with implementation details.

Findings

New semantics is non-blocking and has finite nondeterminism.

Previous semantics is neither non-blocking nor finitely nondeterministic.

Old semantics can be simulated by the new semantics for terminating programs.

Abstract

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.