Big Steps in Higher-Order Mathematical Operational Semantics

TL;DR

This paper develops a categorical framework for relating small-step and big-step operational semantics, providing a general method to derive one from the other and proving their abstract equivalence.

Contribution

It introduces an abstract categorical notion of big-step SOS and a construction to derive it from higher-order GSOS, establishing their equivalence.

Findings

Provides a categorical framework for operational semantics

Introduces a method to derive big-step semantics from GSOS

Proves an abstract equivalence between small-step and big-step semantics

Abstract

Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two.