Big-step and small-step Horn clause derivations applied to operational semantics
The paper proves equivalence between big-step and small-step derivations for Horn clauses and transforms Horn clauses into equivalent sets of clauses based on the given derivation strategy.
The paper establishes the equivalence between big-step and small-step derivations for Horn clauses, which was not previously known.
Before reading this…
Applications
- →Programming languages semantics
- →Logic programming
To understand this paper, make sure you know these concepts first:
- Familiarity with Horn clauses and derivationsfind papers →
- Basic understanding of proof theoryfind papers →
Abstract
More Like ThisThe 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.