Big-step and small-step Horn clause derivations applied to operational semantics
Provides a formal framework for unifying big-step and small-step semantics, benefiting programming language designers and formal methods researchers.
The authors prove equivalence between big-step and small-step derivations for Horn clauses, enabling transformation of big-step operational semantics into equivalent small-step semantics. Experiments across multiple programming languages validate the approach.
The concepts of big-step and small-step derivations are familiar from the operational semantics of programming languages. These concepts are applicable in the more general setting of Horn clause derivations. We prove equivalence between big-step derivations and two versions of small-step derivations for Horn clauses. By specialising interpreters for these derivation strategies, any set of Horn clauses can be transformed into a provably equivalent set of clauses that inherits the behaviour of a given (big- or small-step) Horn clause interpreter. As a special case of this transformation, big-step semantics for any programming language, expressed directly as Horn clauses, can be transformed into equivalent small-step semantics. Experiments with a variety of programming languages are reported.