The Coverage of Operational Semantics
Scott F. Smith · 1998
Techniques of operational semantics do not apply universally to all language varieties: techniques that work for simple functional languages may not apply to more realistic languages with features such as objects and memory effects. We focus mainly on the characterization of the so-called finite elements. The presence of finite elements in a semantics allows for an additional powerful induction mechanism. We show that in some languages a reasonable notion of finite element may be defined, but for other languages this is problematic, and we analyse the reasons for these difficulties. We develop a formal theory of language embeddings and establish a number of properties of embeddings. More complex languages are given semantics by embedding them into simpler languages. Embeddings may be used to establish more general results and avoid reproving some results. It also gives us a formal metric to describe the gap between different languages. Dimensions of the untyped programming language design space addressed here include functions, injections, pairs, objects, and memories. 1