.png){kind=icon}
.png){kind=icon}
Return
Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
.png){kind=icon}
PRE
AI
DOI：10.1145/3779209.3779534.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Structural operational semantics (SOS) is one of the most common formalisms for specifying language semantics. There has been much interest in automatically deriving small-step SOS definitions from big-step definitions and vice versa, as well as towards extrapolating language implementations from these inductive, declarative definitions. This work presents Computation-Tree Semantics (CTS) in which semantic configurations are tree-structured, unlike standard SOS-configurations which are flat. This tree-structure is key in making our approach algorithmic, meaning it is able to describe how a transition is produced, contrary to the traditional declarative approach taken by SOS. We show how one can - in a straight-forward manner - obtain a CTS from the big-step semantics of a simple arithmetic language, a simple while language, and the call-by-need lambda-calculus as given by Launchbury. From the resulting CTS, we then obtain a small-step understanding of all these languages. The arithmetic language example is formalised in Coq/Rocq.
Keywords:
Structural operational semantics
structural relations
algorithmic
big-step semantics
small-step semantics
lambda calculus