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.

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

ASTESIANO, EGIDIO;CERIOLI, MAURA
1989

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11567/201183
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 14
  • ???jsp.display-item.citation.isi??? 4
social impact