An action semantics based on two combinators

Abstract

We propose a naive version of action semantics that begins with a selection of transient and persistent facets, each characterized as a partial monoid. Yielders are defined as operations on the monoids' values, and actions extract values from the facets, give them to yielders, and place the results into facet output. Actions are composed with a primary combinator, andthen, which can be specialized for multiple facet flows, and the choice combinator, or. Using big-step-style deduction rules, we give the semantics of yielders and actions, and we introduce a weakening rule and a strengthening rule, which let us compose actions with different facet domain-codomains. We also introduce Mosses abstraction, a lambda-abstraction variant that improves the readability of action-semantics definitions. Finally, we exploit the subsort (subtype) structure within Mosses's unified algebras to use the deduction rules as both a typing definition as well as a semantics definition. Partial evaluation techniques are applied to type check and compile programs. © 2009 Springer Berlin Heidelberg.