[FOM] many/multi-sorted logic
J.V.Tucker at swansea.ac.uk
Sun Mar 19 11:31:15 EST 2006
Many-sorted or multi-sorted first-order logic has been extensively
applied and further developed in computer science. One reason is
obvious: algorithms and programs invariably use different kinds of
data in computations. For example, gaussian elimination might need
constructions from reals, integers, booleans, characters etc. So, in
reasoning about data and programs, one uses many-sorted logics. Some
basic textbooks introduce the subject (as Arnon mentioned earlier
e.g.: V Sperschneider, G Antoniou, "Logic: a foundation for computer
science", Addison-Wesley, 1991) and there collections of papers that
give a bit of a survey:
K Meinke and J V Tucker (eds.), "Many sorted logic and its
applications", J Wiley & Sons, pp. vii+391.
Many-sorted or multi-sorted first-order logic has also been used in
logic programming to improve on efficiency and program quality: e.g.,
see the early paper
A G Cohn, A more expressive formulation of many sorted logic, Journal
of Automated Reasoning, 3 (1987) 113-200.
1: Reduction to First-order
The reduction of many-sorted logic to the single-sorted case is a
nice little fact that can be put to use. But its use as a reason for
the dismissal of many-sorted logic in a footnote is long out of date.
This is because most of the things we want to study are many-sorted.
In particular, in computer science, we want to model (say) computing
systems as they are (i.e., many sorted) and ask questions about the
properties of the different sorts and how they are related. In
mathematics, work with matrix and polynomial rings, modules and
vector spaces, metric and normed spaces is many-sorted. "Standard"
technical questions in logic, e.g. about interpolation, have to be
viewed in this wider context.
For many years, Jan Bergstra, Jeff Zucker and I have used many-sorted
logic and, indeed, worked on some of the mathematical developments,
all of which are motivated by clear problems in computation.
2: Theory of Data
In the theory of data, the data types on which programs are based are
modelled by many-sorted signatures and structures, usually algebras.
The interfaces to the data, operations and tests are modelled by
signatures. The implementation of the data are modelled by algebras.
The Birkoff-Malc'cev theory of equations and conditional equations (=
varieties and quasi-varieties) has been extended to solve the problem
of specifying the properties of data - and indeed computing systems,
in general - by simple axioms. These axioms describe the data in a
machine independent way, i.e., up to isomorphism of algebras. The
mathematical extensions involve partial operations, sub-sorts, higher-
type equational logic, ... The important thing to note is that these
logical theories are applied in the world's work: A wealth of
software tools and practical applications have been created over the
past 30 years and a wealth of new theoretical problems have been
To get an impression, for high-type equational logic, see say,
K Meinke, Universal algebra in higher types, Theoretical Computer
Science, 100 (1992) 385-417.
and the new specification language CASL:
Bidoit, M. and Mosses, P. D. "Casl User Manual", volume 2900 (IFIP
Series) of LNCS. Springer, 2004.
Mosses, P. D., editor. Casl Reference Manual, volume 2960 (IFIP
Series) of LNCS. Springer, 2004.
Computable Data Types:
Sorts play an essential role in these characterisations of computable
and semi-computable many-sorted algebras modelling data types.
J A Bergstra and J V Tucker, The completeness of the algebraic
specification methods for data types, Information and Control, 54
J A Bergstra and J V Tucker, Equational specifications, complete term
rewriting systems, and computable and semicomputable algebras,
Journal of ACM, 42 (1995) 1194-1230
Recently, I have given a lecture on the history of the algebraic
theory for the British Computer Society, if interested please contact
me for the slides.
3. Program Verification:
We have worked on logics for program verification based on many-
sorted algebras, for example:
J V Tucker and J I Zucker, Program correctness over abstract data
types with error-state semantics, North-Holland, Amsterdam, 1988, pp.
Here is a simple paper that is about the distinction with the single-
J A Bergstra and J V Tucker, Hoare's logic for programming languages
with two data types, Theoretical Computer Science, 28 (1984) 215-221.
4: Abstract Models of Computability on Many Sorted Algebras
Computability theory needs to be generalised to many sorted algebras:
J. V. Tucker and J. I. Zucker, Computable functions and
semicomputable sets on many sorted algebras, in S. Abramsky, D.
Gabbay and T Maibaum (eds.), Handbook of Logic for Computer Science.
Volume V Logic and Algebraic Methods, 2000, Oxford University Press,
J V Tucker and J I Zucker, Origins of our theory of computation on
abstract data types at the Mathematical Centre, Amsterdam, 1979-80,
in F de Boer et al, Liber Amicorum: J W de Bakker, CWI Amsterdam, 2002.
I hope that you find this informative.
J V Tucker
Department of Computer Science
University of Wales Swansea
Swansea SA3 2HN
More information about the FOM