Swinging data types: Syntax, semantics, and theory

Abstract

Initial structures are appropriate for modelling constructor-based data types because they fit the intuition and admit inductive theorem proving. In practice, the latter requires a distinction between constructors and denned functions and an axiomatization that complies with the constructor discipline. This badly suits non-free or permutative types such as sets, bags and maps and is yet less reasonable when infinite structures like streams or processes come into play. Instead, non-free as well as infinite structures should be regarded as dynamic objects and identified through observable reactions (observers, inquiries, attributes) upon received messages (transitions, actions, methods) rather than by constructors they are built of. The intended model is based on an exten-sional, contextual, behavioural, observational or bisimilarity relation and given by the final object in a category of conservative structures. This enforces a hierarchical approach because the nature of attributes is to map higher-level to lower-level objects. Data types with both constructor and action sorts are split into swinginy chains of specifications each of which extends its predecessor by either a constructor type or an action type. Constructor types are characterized by visible domains, inductively defined total functions, structural equality and safety conditions expressed as Horn clauses. Action types are given by hidden, but - via predecessors in the chain of specifications - observable domains, partial functions and coinductively defined behavioural equality and liveness conditions. The canonical model of a swinging specification is a chain of initial and final models. For proof-theoretical purposes action types are transformed into their Horn clause completions whereby the semantics of the whole specification reduces to a chain of initial models captured by uniform proof rules and induction principles.