[FOM] many/multi-sorted logic

[John Tucker]

Dear Colleagues,

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  
discovered.

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  
(1982) 186-200.

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.  
vii+212.

Here is a simple paper that is about the distinction with the single- 
sorted:

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,  
317-523.

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.



John



J V Tucker
Department of Computer Science
University of Wales Swansea
Singleton Park
Swansea SA3 2HN
UK


http://www-compsci.swan.ac.uk/~csjvt/