Machine Semantics—From Causality to Computational Models
Peter Hines
This paper gives the theory of abstract machines and machine semantics. Abstract machines are simply sets of configurations with a discrete notion of causality — hence they describe a wide range of situations that are not usually thought of as ‘computational’. The ‘machine semantics’ program nevertheless aims to treat them as computational devices, by considering a range of different descriptions of how these machines behave, from ‘high-level’ to ‘low-level’ behaviour.
The comparison of high-level and low-level descriptions, as a partial ordering, gives several strongly computational structures. There are close connections to locales and intuitionistic logic [19], directed-complete partial orders and the Geometry of Interaction system [22], with applications to space-bounded Turing machines [18].
It is demonstrated that the relevant partial ordering gives Scott domains, as used in models of untyped lambda calculus. The data/control distinction for abstract machines is also considered. As a test, this distinction is used to derive the usual models of two-way automata as special cases of the space-bounded Turing machine models of [22].
Keywords: Abstract Machines, Semantics, Domain Theory, Lambda Calculus, State Machines