Dipartimento di Informatica e Scienze dell'Informazione
On the existence of initial models for
E. Astesiano and M. Cerioli .
partial (higher-order) conditional specifications
In Proceedings of TAPSOFT'89, number 351 in Lecture Notes in
Computer Science, pages 74--88, Berlin, 1989. Springer Verlag.
Partial higher-order conditional specifications may not admit initial models,
because of the requirement of extensionality, even when the axioms are positive
The main aim of the paper is to investigate in full this phenomenon.
If we are interested in term-generated initial models, then partial higher-order
specifications can be seen as special cases of partial conditional specifications,
i.e. specifications with axioms of the form D -> e, where D is a denumerable
set of equalities, e is an equality and equalities can be either strong or
Thus we first study the existence of initial models for partial conditional
The first result establishes that a necessary and sufficient condition for
the existence of an initial model is the emptiness of a certain set of closed
conditional formulae, which we call ``naughty''.
These naughty formulae can be characterized w.r.t. a generic inference system
complete w.r.t. closed existential equalities and the above condition amounts
to the impossibility of deducing those formulae within such a system.
Then we exhibit a (necessarily infinitary) inference system which we show to be
complete w.r.t closed equalities; the initial model exists if and only if no
naughty formula is derivable within this system and, when it exists, can be
characterized, as usual, by the congruence associated with the system.
Finally, applying our general results to the case of higher-order specifications
with positive conditional axioms, we obtain necessary and sufficient conditions
for the existence of term-generated initial models in that case.
The compressed postscript version of this paper is available through anonymous ftp
at ftp.disi.unige.it, in