Affordable Access

Publisher Website

Adapting Big-Step Semantics to Small-Step Style: Coinductive Interpretations and “Higher-Order” Derivations

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
10
Identifiers
DOI: 10.1016/s1571-0661(05)80692-9
Disciplines
  • Linguistics

Abstract

Abstract 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.

There are no comments yet on this publication. Be the first to share your thoughts.