Partial Derivation in Modular Structural Operational Semantics

Casper Poulsen

(Swansea University)

The scientific study of programming languages requires a formal specification of their semantics. However, the incentives of applying formal specification frameworks during programming language design are often outweighed by more pragmatic concerns, such as developing and maintaining an executable interpreter for the language under design.

One way of bridging the gap between formal specification and pragmatic programming language design is by making formal specifications pragmatic for the language developer. Modular structural operational semantics (MSOS), a modular variant of structural operational semantics (SOS), is a formalism that supports incremental and scalable language design, e.g., by taking a component-based approach to semantic specification.

Interpreting the transitive closure of the transition function for a set of MSOS rules gives a prototype interpreter, where evaluation corresponds to proof derivation using the underlying MSOS rules. However, a naive implementation of such an interpreter has a worst-case interpretive overhead where each proof step requires a number of inferences that is linear in the depth of the input term. Furthermore, while small-step semantics have several declarative advantages, term reduction using small-step rules requires more inference steps than when using their big-step counterparts. For the programming language designer who is concerned with efficiency, the considerable interpretive overhead incurred by a naive interpretation may be unacceptable in practice.

Here, we explore how to reduce interpretive overhead of small-step MSOS rules through partial evaluation techniques which, in our modular structural proof system setting, we will call partial derivation. Combining ideas from partial evaluation in logic programming, bisimulation theory, and refocusing in reduction semantics we show how to derive rules whose proofs require fewer inferences (and hence, whose evaluation is more efficient). Applying partial derivation to a semantics is a fully mechanisable transformation that gives a provably semantically equivalent set of rules. Furthermore, the techniques are broadly applicable, being constrained by only a very mild set of conditions for correctness. The transformations result in rules with a big-step flavour, hinting at the inter-derivability of small-step and big-step style semantics.

As a proof of concept, we have prototyped semantic rules in Prolog, where we can observe a significant reduction in the running time of interpreters based on partially derived semantics in comparison with their naive counterparts. We conclude that partial derivation is a viable technique for reducing interpretive overhead in modular structural proof systems and practical interpreters derived from these, and that partial derivation is a viable tool for prototypical and pragmatic language design.
Thursday 21st March 2013, 14:00
Robert Recorde Room
Department of Computer Science