Adapting Big-Step Semantics to Small-Step Style: Coinductive Interpretations and “Higher-Order” Derivations
Husain Ibraheem Hajji Ibraheem, David A. Schmidt · Electronic Notes in Theoretical Computer Science · 1998
We adapt Kahn-style (“big-step”) natural semantics to take on desirable aspects of small-step and denotational semantics forms, more precisely: (i) the ability to express divergent computations; (ii) the ability to reason about the (length of a) computation of a derivation; and (Hi) the ability to compute upon and reason about higher-order values. To accomplish these results, we extend the classical, inductive interpretation of natural semantics with coinduction mechanisms and use “negative” rules to express divergence. A simple reformatting of the syntax of derivations allows a simple description of the “length” of a derivation. Finally, the receding of closure values into denotational-semantics-like functions lets one embed derivations within closures that embed within derivations; in this sense, the semantics becomes “higher order.” Examples are given to support the definitional developments.