On the Existence of Initial Models for Partial (Higher-Order) Conditional Specifications

Partial higher-order conditional specifications may not admit initial models, because of the requirement of extensionality, even when the axioms are positive conditional. 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 existential. Thus we first study the existence of initial models for partial conditional specifications. 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.