Dipartimento di Informatica e Scienze dell'Informazione
Free Objects and Equational Deduction for Partial Conditional Specifications
E. Astesiano and M. Cerioli .
Theoretical Computer Science, 152(1):91--138, 1995.
Partial conditional specifications consist of conditional axioms, with
equalities in the (possibly infinite set of) premises and in the consequence,
which are interpreted in partial algebras.
Equalities may be existential (=e) or strong (=); t=e t'
holds in an algebra iff both t and t' are defined and equal, while t = t'
holds in an algebra iff either t =e t' holds or both t and t' are undefined.
Contrary to the well explored case of positive conditional axioms (only existential
equalities in the premises), general partial conditional specifications do not
always admit free models and the related theory is much more subtle.
In this paper we fully investigate and solve the problem of existence of
free and initial models, giving necessary and sufficient conditions, first from
a model theoretical and then from a logical deduction viewpoint.
In particular we present a deduction system which is complete wrt strong
equalities between open terms. Since positive conditional partial specifications
and conditional total specifications are special cases of the paradigm
investigated here, the presented theory generalizes the related results about
free models and the Birkhoff-like deduction theory.
The system we exhibit handles also the case of infinitary conjunctions
as premises of the axioms; it reduces to a classical one for the positive
conditional case by just dropping one rule, and finally it solves the empty-carrier
problem without using explicit quantification.
The theory presented here also gives the basis for solving, via the usual
first-order reduction, the problem of the existence of free and initial models
for partial higher-order specifications of term-generated extensional models.
The compressed postscript version of this paper is available through anonymous ftp
at ftp.disi.unige.it, in