An Operational Semantics Framework Supporting the Incremental Construction of Derivation Trees
✍ Scribed by Allen Stoughton
- Publisher
- Elsevier Science
- Year
- 1998
- Tongue
- English
- Weight
- 638 KB
- Volume
- 10
- Category
- Article
- ISSN
- 1571-0661
No coin nor oath required. For personal study only.
✦ Synopsis
We describe the current state of the design and implementation of Dops, a framework for Deterministic OPerational Semantics that will support the incremental construction of derivation trees, starting from term/input pairs. This process of derivation tree expansion may terminate with either a complete derivation tree, explaining why a term/input pair evaluates to a particular output, or with a blocked incomplete derivation tree, explaining why a term/input pair fails to evaluate to an output or the process may go on forever, yielding, in the limit, an in nite incomplete derivation tree, explaining why a term/input pair fails to evaluate to an output.
The Dops metalanguage is a typed lambda calculus in which all expressions converge. Semantic rules are speci ed by l a m bdaterms involving resumptions, which are used by a r u l e t o consume the outputs of sub-evaluations and then resume the rule's work. A rule's type describes the numberandkinds of sub-evaluations that the rule can initiate, and indicates whether the rule can block. The semantics of Dops is de ned in an object language-independent manner as a small-step semantics on concrete derivation trees: trees involving resumptions. These concrete derivation trees can then beabstracted into ordinary derivation trees by forgetting the resumptions.
1 The incremental construction of derivation trees
We begin by de ning the operational semantics that we will use as an example throughout the rest of the paper: a big-step, environment-based semantics of the untyped, call-by-value lambda calculus.