Journal of Logic and Computation, Volume 11, Issue 3, pp. 453-481: Abstract.
Algebraic Specifications, Higher-order Types and Set-theoretic Models
Hélène Kirchner1, and Peter D. Mosses2
1LORIA-CNRS, B.P. 239, F-54506 Vandoeuvre-lès-Nancy Cedex, France. E-mail: Helene.Kirchner@loria.fr
In most algebraic specification frameworks, the type system is restricted to sorts, subsorts, and first-order function types. This is in marked contrast to the so-called model-oriented frameworks, which provide higher-order types, interpreted set-theoretically as Cartesian products, function spaces, and power-sets. This paper presents a simple framework for algebraic specifications with higher-order types and set-theoretic models. It may be regarded as the basis for a Horn-clause approximation to the Z framework, and has the advantage of being amenable to prototyping and automated reasoning. Standard set-theoretic models are considered, and conditions are given for the existence of initial reducts of such models. Algebraic specifications for various set-theoretic concepts are considered.
Keywords: Algebraic specification, higher-, order types, set-, theoretic models, intensional set theory, Horn clause logic, initiality