Home  Online Resources  Table of Contents

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
2BRICS & Department of Computer Science, University of Aarhus, Ny Munkegade bldg. 540, DK-8000 Aarhus C, Denmark. E-mail: pdmosses@brics.dk

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

  Full-Text PDF  (294 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.