Initial semantics in logics with constructors
Daniel Găină1 and Kokichi Futatsugi1
1 Japan Advanced Institute of Science and Technology{daniel,futatsugi}@jaist.ac.jp
November 6, 2012

Abstract
The constructor-based logics constitute the logical foundation of the so-called OTS/CafeOBJ method, amodeling, specification and verification method of the observational transition systems. It is well known
the important role played in algebraic specifications by the initial algebras semantics. Free models
along presentation morphisms provide semantics for the modules with initial denotation in structured
specification languages. Following Goguen and Burstall, the notion of logical system over which webuild specifications is formalized as an institution. The present work is an institution-independent
study of the existence of free models along sufficient complete presentation morphisms in logics withconstructors in the signatures.

1

Introduction

Algebraic specification represents one of the most important classes of formal methods assisting the development of more reliable and efficient software systems. The fundamental
mathematical structure underlying the theory of algebraic specifications is that of institution [20], a formal concept of logical system which arose within computing science with theambition of covering the population of logics used in practice and working as much as possible at the abstract level, independent of any particular institution. In the present paper westudy the existence of initial models for theories and free models along theory morphisms inarbitrary constructor-based institutions. The logics with constructors constitute the foundation of the OTS/CafeOBJ method, a modeling, specification and verification method of theobservational transition systems, which has been previously explored in many case studies[27, 17, 26, 16].
Constructor-based institutions [3, 4, 19] are obtained from a base institution basicallyby enhancing the syntax with a sub-signature of constructor operators and by restricting thesemantics to reachable models which consist of constructor-generated elements. The sentences and the satisfaction condition are preserved from the base institution and the signaturemorphisms are restricted such that the reducts of models which are reachable in the target
signature are again reachable in the source signature. The result sorts of the constructors arecalled constrained and a sort that is not constrained it is called loose.
1

By introducing the constructor operators in the signatures we gain more expressivity forthe specifications but some of the basic important properties are lost. For example, theconstructor-based variants of Horn institutions 1 are not complete. However, in [19] we
obtained a ω-completeness 2 result that depends on sufficient completeness. Intuitively, a presentation (Σ, Γ), where Σ is a signature and Γ a set of formulas, is sufficient complete if every
term can be reduced to a term formed with constructors and operators of loose sorts using
the equations in Γ. We argued that a complete and compact system of proof rules cannot beprovided due to the Gödel’s famous incompleteness result.
Firstly, we study the existence of pushouts in a concrete category of constructor-based
signature morphisms (see Section 3). The method of constructing the pushouts can be usedin other cases as well. As a main result it is shown that the existence can be guaranteed by imposing certain conditions on the signature morphisms. This result is important as the pushout
construction is one of the most used approaches to combine specifications. A property closely
related to combining specifications coherently with respect to the semantics is semi-exactness.
The institution theoretic concept of semi-exactness is a basic property of institutions that has
been intensively used by various works in algebraic specification [29, 15, 8, 30]. In thepresent work we conduct an institution dependent study of the semi-exactness property thatis used later on to prove the existence of free models.
Secondly, we investigate the existence of initial and free models in arbitrary constructorbased institutions.
1. ‘Reachable’ institutions are obtained from constructor-based institutions by restricting
the category of signatures such that all operators of constrained sorts are constructors.
In Section 4, we prove in arbitrary ‘reachable’ institutions
the existence of initial mod^els of any set of Horn sentences of the form (∀X) H ⇒ C, where H is a set of atoms,
and C is an atom. Our hypothesis are natural and easy to check in concrete examples of
institutions. Our results are much general than the ones obtained within the frameworkof factorization systems [2, 33, 1] or inclusion systems [10]. In ‘reachable’ institutions
the class of models of a set of Horn sentences do not form a quasi-variety, and therefore
the initiality results derived from preservation (i.e. the model class of a set of Horn sentences forms a quasi-variety, and quasi-varieties have initial objects) such as [2, 33, 1]
or [10] cannot be applied. Initiality is then easily extended to the constructor-based
institutions via sufficient completeness.
2. The existence of left adjoints of the forgetful functors gives the free models along
the presentation morphisms which constitute the semantic of the modules with initialdenotation of the structured algebraic specification languages. This was studied in theliterature under the name of liberality and it has played a central role in institution
theory from its beginning [20] (see also [23, 31]). In Section 5 we apply the results in[10] to extend the existence of initial models of sufficient complete presentations to theexistence of free models along sufficient complete presentation morphisms in arbitrary
constructor-based institutions.

1 Horn institutions are obtained from a base institution, for example first-order logic, by restricting the sentencesVto the so-called Horn sentences of the form (∀X) H ⇒ C, where H is a set of atoms in the base institution, and C
is an atom.
2 Some proof rules contain infinite premises which can only be checked with induction schemes. As a consequence, the resulting entailment system is not compact.

2

We assume that the reader is familiar with the basic notions of category theory. See [25]for the standard definitions of category, functor, pushout, etc., which are omitted here.

2

Institutions

An institution I = (SigI , SenI , Mod I , |=I ) consists of
1. a category SigI , whose objects are called signatures,
2. a functor SenI : SigI → Set, providing for each signature a set whose elements arecalled (Σ-)sentences,
3. a functor Mod I : SigI → Cat op , providing for each signature Σ a category whose objects
arecalled(Σ-)models
and
whose
arrowsarecalled(Σ-)morphisms,
4. a relation |=IΣ ⊆ |Mod I (Σ)|×SenI (Σ) for each signature Σ ∈ |SigI |, called (Σ-)satisfaction,such that for each morphism ϕ : Σ → Σ0 in SigI , the following satisfaction condition
holds:
M 0 |=IΣ0 SenI (ϕ)(e) iff Mod I (ϕ)(M 0 ) |=IΣ e
for all M 0 ∈ |Mod I (Σ0 )| and e ∈ SenI (Σ).
We denote the reduct functor Mod I (ϕ) by ϕ and the sentence translation SenI (ϕ) by
ϕ( ). When M = M 0 ϕ we say that M is the ϕ-reduct of M 0 and M 0 is a ϕ-expansion of
M. When there is no danger of confusion, we omit the superscript from the notations of theinstitution components; for example SigI may be simply denoted by Sig.
Example 1 (First Order Logic (FOL) [20]) The signatures are triplets (S, F, P), where S is
the set of sorts, F = {Fw→s }(w,s)∈S∗ ×S is the (S∗×S -indexed) set of operation symbols, andP = {Pw }w∈S∗ is the (S∗ -indexed) set of relation symbols. If w = λ, an element of Fw→s iscalled aSconstant symbol, or S
a constant. By a slight notational abuse, we let F and P also
denote (w,s)∈S∗ ×S Fw→s and w∈S∗ Pw respectively. A signature morphism between (S, F, P)
and (S0 , F 0 , P0 ) is a triplet ϕ = (ϕst , ϕop , ϕrl ), where ϕst : S → S0 , ϕop : F → F 0 , ϕrl : P →P0 such that ϕop (Fw→s ) ⊆ Fϕ0 st (w)→ϕst (s) and ϕrl (Pw ) ⊆ Pϕ0 st (w) for all (w, s) ∈ S∗ × S. When
there is no danger of confusion, we may let ϕ denote each of ϕst , ϕrl and ϕop . Given asignature Σ = (S, F, P), a Σ-model A is a triplet A = ({As }s∈S , {Aw,s (σ)}(w,s)∈S∗ ×S,σ∈Fw→s ,{Aw (R)}w∈S∗ ,R∈Pw ) interpreting each sort s as a set As , each operation symbol σ ∈ Fw→s as
a function Aw,s (σ) : Aw → As (where Aw stands for As1 × . . . × Asn if w = s1 . . . sn ), and eachrelation symbol R ∈ Pw as a relation Aw (R) ⊆ Aw . When there is no danger of confusion we
may let Aσ and AR denote Aw,s (σ) and Aw (R) respectively. Morphisms between models are
the usual Σ-morphisms, i.e., S-sorted functions that preserve the structure. The Σ-sentences
are obtained from• equality atoms t1 = t2 , where t1 ,t2 ∈ (T(S,F) )s and T(S,F) is the (S, F)-algebra of groundterms, or• relational atoms R(t1 , . . . ,tn ), where R ∈ Ps1 ...sn and ti ∈ (T(S,F) )si for all i ∈ {1, . . . , n},
by applying for a finite number of times:3• negation, conjunction, disjunction,• universal or existential quantification over finite sets of constants (variables).
Satisfaction is the usual first-order satisfaction and is defined using the natural interpretationsof ground terms t as elements At in models A. The definitions of functors Sen and Mod onmorphisms are the natural ones: for any signature morphism ϕ : Σ → Σ0 , Sen(ϕ) : Sen(Σ) →Sen(Σ0 ) translates sentences symbol-wise, and Mod(ϕ) : Mod(Σ0 ) → Mod(Σ) is the forgetful
functor.
Example 2 (Constructor-based First Order Logic (CFOL)) The signatures are of the form
(S, F, F c , P), where (S, F, P) is a first-order signature, and F c ⊆ F (for all (w, s) ∈ S∗ × S wechave Fw→s⊆ Fw→s ) is a distinguished subfamily of sets of operation symbols called constructors. The constructors determine the set of constrained sorts Sc ⊆ S: s ∈ Sc iff there exists ac . We call the sorts in Sl = S − Sc loose. The (S, F, F c , P)-sentences areconstructor σ ∈ Fw→sthe FOL sentences for the signature (S, F, P).
The (S, F, F c , P)-models are the usual first-order structures M with the carrier sets for theconstrained sorts consisting of interpretations of terms formed with constructors and elementsof loose sorts, i.e. there exists a S-sorted set Y = {Ys }s∈S of variables of loose sorts (i.e. for/ and a S-sorted function f = { fs : Ys → Ms }s∈S such that for every
all s ∈ Sc we have Ys = 0)
constrained sort s ∈ Sc , the function fs# : (T(S,F c ) (Y ))s → Ms is a surjection, where T(S,F c ) (Y )is the (S, F c )-algebra of terms with variables from Y and f # : T(S,F c ) (Y ) → M (S,F c ) is theunique extension of f to a (S, F c )-morphism.
A signature morphism ϕ : (S, F, F c , P) → (S0 , F 0 , F 0c , P0 ) in CFOL is a first-order signature morphism ϕ : (S, F, P) → (S0 , F 0 , P0 ) such that the constructors are preserved along thesignature morphisms (i.e. if σ ∈ F c then ϕ(σ) ∈ F 0c ) and no ‘new’ constructors are introducedcfor ‘old’ constrained sorts (i.e. if s ∈ Sc and σ0 ∈ (F 0c )w0 →ϕ(s) then there exists σ ∈ Fw→ssuch0
that ϕ(σ) = σ ).
Lemma 3 [18] For every CFOL signature morphism ϕ : (S, F, F c , P) → (S0 , F 0 , F 0c , P0 ), andany (S0 , F 0 , F 0c , P0 )-model M 0 , we have M 0 (S,F,P) ∈ Mod(S, F, F c , P).
Variants of constructor-based first-order logic were studied in[4] and [3].
Example 4 (Horn Clause Logic(HCL)) A Horn sentence for a FOL signature (S, F, P) isV
a sentence of the form (∀X)( H) ⇒ C, where X is a finite set of variables, H is a finite setof (relational or equational) atoms, and C is a (relational or equational) atom. Classically,
Horn clauses are Horn sentences in first-order logic without equality. Here, we call Hornclauses all Horn sentences of FOL. Thus HCL has the same signatures and models as FOL
but only Horn clauses as sentences. One can define the constructor-based variant of HCL(i.e. Constructor-based Horn Clause Logic (CHCL)) as the restriction of CFOL to Hornsentences.
Example 5 (Preorder algebra (POA) [14, 13]) The POA signatures are just the ordinary
algebraic signatures. The POA models are preordered algebras which are interpretations of
the signatures into the category of preorders Pre rather than the category of sets Set. Thismeans that each sort gets interpreted as a preorder, and each operation as a preorder functor,
which means a preorder-preserving (i.e. monotonic) function. A preordered algebra morphism is just a family of preorder functors (preorder-preserving functions) which is also an
algebra morphism.
4The sentences have two kinds of atoms: equations and preorder atoms. A preorder atomt ≤ t 0 is satisfied by a preorder algebra M when the interpretations of the terms are in thepreorder relation of the carrier, i.e. Mt ≤ Mt 0 . Full sentences are constructed from equational
and preorder atoms by using Boolean connectives and first-order quantification.
Horn preorder algebra (HPOA) and its constructor-based variant (CHPOA) are obtained
as the restrictions of POA and CPOA, respectively, to Horn sentences.
Below we introduce a less refined class of constructor-based institutions that is used to importinitiality and liberality to constructor-based institutions.
Example 6 (Reachable First Order Logic(RFOL)) This institution is obtained from CFOL
by restricting the signatures such that all operation symbols of constrained sorts are construcc
tors, i.e. for each (S, F, F c , P) we have F c = F S where
Fw→s : s ∈ Sc
Sc
Fw→s =
0/ : s 6∈ Sc
By restricting the sentences to Horn sentences we obtain RHCL. A similar construction canalso be done for preorder algebra.

2.1

Substitutions
χ1

χ2

In CFOL, consider Σ ,→ Σ(X1 ) and Σ ,→ Σ(X2 ) two inclusion signature morphisms, whereΣ = (S, F, F c , P) is a CFOL signature, Xi is a set of non-constructor constant symbols disjoint
from the constants of F, and Σ(Xi ) = (S, F ∪ Xi , F c , P). A substitution between χ1 and χ2 in
CFOL can be represented by a function θ : X1 → TF (X2 ). One can easily notice that θ can beextended to a function
Sen(θ) : Sen(Σ(X1 )) → Sen(Σ(X2 ))that replaces all the symbols in X1 by the corresponding F ∪ X2 -terms according to θ. On thesemantics side, θ determines a functor
Mod(θ) : Mod(Σ(X2 )) → Mod(Σ(X1 ))such that for all Σ(X2 )-models M we have
• Mod(θ)(M)z = Mz , for each sort z ∈ S, or operation symbol z ∈ F, or relation symbolz ∈ P, and• Mod(θ)(M)z = Mθ(z) for each z ∈ X1 .
Proposition 7 For every CFOL signature Σ and each substitution θ : X1 → Σ(X2 )Mod(θ)(M) |= ρ iff M |= Sen(θ)(ρ)
for all Σ(X2 )-models M and all Σ(X1 )-sentences ρ.
The proof is the same as the one for FOL, which can be found in [11].
Assumption 8 Throughout this paper, for all institutions above, we assume that the signaturemorphisms allow mappings of constants to ground terms.
5This makes it possible to treat first-order substitutions in the comma category 3 of signaturemorphisms.
χ1

χ2

Definition 9 Consider two signature morphisms Σ → Σ1 and Σ → Σ2 of an institution. A
signature morphisms θ : Σ1 → Σ2 such that χ1 ; θ = χ2 is called a Σ-substitution between χ1and χ2 .

2.2

Presentations

Let I = (Sig, Sen, Mod, |=) be an institution. A presentation (Σ, E) consists of a signature Σ
and a set E of Σ-sentences. A presentation morphism ϕ : (Σ, E) → (Σ0 , E 0 ) is a signature morphism ϕ : Σ → Σ0 such that E 0 |= φ(E). The presentation morphisms form a category denoted
Sig pres with the composition inherited from the category of signatures. The model functor
Mod can be extended from the category of signatures Sig to the category of presentations
Sig pres , by mapping a presentation (Σ, E) to the full subcategory 4 Mod(Σ, E) of Mod(Σ)
consisting of models that satisfy E. The correctness of the definition of the overloaded model
functor Mod : Sig pres → Cat op is guaranteed by the satisfaction condition of the base institution. This leads to the institution of presentations I pres = (Sig pres , Sen, Mod, |=) over thebase institution I , where the sentence functor Sen and the satisfaction condition |= of thebase institution I are overloaded such that
• Sen(Σ, E) = Sen(Σ), and• for all M ∈ Mod(Σ, E) and sentences ρ ∈ Sen(Σ, E), M |=(Σ,E) ρ iff M |=Σ ρ.

2.3

Basic set of sentences

A set of sentences B ⊆ Sen(Σ) is called basic [9] if there exists a Σ-model MB such that, forall Σ-models M, M |= B iff there exists a morphism MB → M. We say that MB is a basicmodel of B. If in addition the morphisms MB → M is unique then the set B is called epi basic.
Remark 10 Any set of epi basic sentences has an initial model.
It is well-known that any set of atoms in FOL and POA is epi basic (see for example [9] or[12]). In the followings we lift this result to reachable institutions.
Lemma 11 Any set of atoms in RFOL and RPOA is epi basic.
P ROOF. Let (S, F, F c , P) be a a RFOL-signature. Since all operators of constrained sorts areconstructors we have T(S,F,P) ∈ Mod(S, F, F c , P), where T(S,F,P) is the term model interpreting
each relation symbol as empty set. Moreover, for any congruence relation ≡⊆ T(S,F,P) ×
T(S,F,P) we have that (T(S,F,P) )≡ ∈ Mod(S, F, F c , P).
Let B be a set of atomic (S, F, F c , P)-sentences. The basic model MB it is the initial modelof B and it is constructed as follows: on the quotient (T(S,F,P) )≡B of the term model T(S,F,P)
f
3 Given a category C and an object A ∈ |C |, the comma category A/C has arrows A →B ∈ C as objects, andh ∈ C (B, B0 ) with f , h = f 0 as arrows.
4 C 0 is a full subcategory of C if C 0 is a subcategory of C such that C (A, B) = C 0 (A, B) for all objects A, B ∈ |C 0 |.

6

by the congruence generated by the equational atoms of B, we interpret each relation symbolπ ∈ P by (MB )π = {(t1 /≡B , . . . ,tn /≡B ) | π(t1 , . . . ,tn ) ∈ B}.
By defining a notion of congruence compatible with the preorder (see [13] or [7]) one
may obtain the same result for RPOA.
A direct consequence of Lemma 11 is the following corollary.
Corollary 12 In RFOL and RPOA, any set of atoms has an initial model.
Given a CFOL signature (S, F, F c , P), the model (S, F, P)-model T(S,F,P) is not reachable
by the constructors in F c , i.e. T(S,F,P) ∈ |Mod(S, F, F c , P)| does not hold, in general. It follows
that in CFOL not all sets of sentences are epi basic, and hence, not all sets of atoms have an
initial model.

2.4

Reachable models

Below, we give an institution-independent characterization of the models with elements thatconsist of interpretations of terms.
Definition 13 Let D be a broad subcategory 5 of signature morphisms of an institution I =(Sig, Sen, Mod, |=). We say that a Σ-model M is D -reachable if for each span of signature
χ1χ
morphisms Σ1 ←− Σ0 −→ Σ in D , each χ1 -expansion M1 of M χ determines a substitutionθ : χ1 → χ such that M θ = M1 .
The proof of the following proposition can be found in [18].
Proposition 14 In FOL and POA assume that D is the class of signature extensions witha finite number of constants. A model M is D -reachable iff its elements are exactly theinterpretations of ground terms.
In concrete institutions underlying the algebraic specification languages, D consists of signature extensions with a finite number of constants. Since D -reachable models have elements
which consist of interpretations of ground terms, we may refer to D -reachable models as
ground reachable models.
Remark 15 In FOL and POA, the models defining a set of atoms as basic set of sentences
are ground reachable.
For each RFOL Σ-model M there exists a signature extension Σ ,→ Σ0 with constants of loose
sorts, and a ground reachable Σ0 -model M 0 such that the reduct of M 0 to the signature Σ is M.
Note that Σ0 can be the extension of Σ with the elements of loose sorts of the model M. In thiscase M 0 is just like M but interpreting each element of loose sort by itself. The RFOL models
are called reachable. The CFOL models are reachable in the sub-signature of constructors.
Actually, there is an abstract characterization of reachable models (see [19, 18]) which may
be applied to a base institution in order to obtain the constructor-based variant.

5 C 0 is a broad subcategory of C if C 0 is a subcategory of C and |C 0 | = |C |.

7

2.5

Internal logic

The following institutional notions dealing with logical connectives and quantifiers were defined in [32].
Let Σ ∈ |Sig| be a signature of an institution I = (Sig, Sen, Mod, |=).
• A Σ-sentence ¬e is a (semantic) negation of the Σ-sentence e when for every Σ-model
M we have M |=Σ ¬e iff M 2Σ e.
• A Σ-sentence e1 ∧ e2 is a (semantic) conjunction of the Σ-sentences e1 and e2 when forevery Σ-model M we have M |=Σ e1 ∧ e2 iff M |=Σ e1 and M |=Σ e2 .
χ

• A Σ-sentence (∀χ)e0 , where Σ → Σ0 ∈ Sig and e0 ∈ Sen(Σ0 ), is a (semantic) universal
χ-quantification of e0 when for every Σ-model M we have M |=Σ (∀χ)e0 iff M 0 |=Σ0 e0
for all χ-expansions M 0 of M.
VWe will use the symbol to denote the conjunction of a set of sentences even if it isinfinite. Very often quantification is considered only for a restricted class of signature morphisms. For example, quantification in FOL considers only the signature extensions with afinite number of constants.

3

Pushouts of constructor-based signatures

There is a difference between the signature morphisms in [3] and the signature morphisms in
CFOL. The signature morphisms in [3] do not allow ‘new’ constructors of ‘old’ sorts, andthey are too restrictive for applications as one can see below. We allow constructors of ‘old’sorts that are loose, but the signature morphisms in CFOL do not have pushouts, in general.
We will study here the conditions when the pushouts do exist.

3.1

Pushouts

Let ϕ : (S, F, F c , P) → (S0 , F 0 , F 0c , P0 ) be a signature morphism in CFOL. We say that ϕop
op
is injective if for all arities w ∈ S∗ and sorts s ∈ S, ϕw→s is injective. The same applies toct
rl
ϕ , the constructor symbols component, and ϕ , the relation symbols component. ϕop is
encapsulated means that no ‘new’ operation symbol, i.e. outside the image of ϕ, is allowed
to have the sort in the image of ϕ. More precise, if σ0 ∈ Fw0 0 →s0 then for all s ∈ S such thats0 = ϕst (s) there exists σ ∈ Fw→s such that ϕop (σ) = σ0 . Same applies to ϕct .
Definition 16 ((xyzt)-signature morphisms) A CFOL signature morphism
ϕ : (S, F, F c , P) → (S0 , F 0 , F 0c , P0 )is a (xyzt)-morphism, with x,t ∈ {i, ∗} and y, z ∈ {i, e, ∗}, where i stands for ‘injective’, e for‘encapsulated’, and ∗ for ‘all’, when
1. it does not map constants to terms different from constants,
2. the sort component ϕst : S → S0 has the property x,
op

3. the operation component ϕop = (ϕw→s : Fw→s → Fϕ0 st (w)→ϕst (s) )w∈S∗ has the property y,
s∈S

8

c
0c
4. the constructor component ϕct = (ϕctw→s : Fw→s → Fϕst (w)→ϕst (s) )w∈S∗ has the property z,
s∈S

and

0
5. the relation component ϕrl = (ϕrlw : Pw → Pϕst (w) )w∈S∗ has the property t.

This notational convention can be extended to other institutions too, such as, for example,
FOL or CPOA. In case of FOL, because there are no constructor symbols, the third component is missing. In case of CPOA, because there are no relation symbols, the last componentis missing.
Proposition 17 [3] The subcategory of CFOL signature (∗ ∗ e∗)-morphisms has pushouts.
Consider the following example of parameterized specification.
Example 18 Consider the following parameterized specification of lists of arbitrary elements:
sorts Triv, Listχ{constr}sort Triv ⊆ / op nil : List
op con : Triv → List {constr}
If we want to obtain lists of natural numbers then we need to construct the pushout of thefollowing span of signature morphisms:
sorts Triv, List
op nil : List
{constr} oop con : Triv → List {constr}

χ⊇

sort Trivϕ
Triv7→Nat

sort Nat/ op 0 : Nat{constr}
op s Nat → Nat {constr}

Note that χ is a signature morphism in the sense of [3] but ϕ is not.
We will investigate the existence of pushouts of constructor-based signature morphisms inorder to cover the example above.
Proposition 19 The category of CFOL signature morphisms has ((∗∗∗∗), (i∗e∗))-pushouts 6 .
χ
χ1
ϕ
ϕ2
Moreover, if {Σ2 ← Σ → Σ1 , Σ1 → Σ0 ← Σ2 } is a pushout of CFOL signature morphisms suchthat ϕ is a (∗ ∗ ∗∗)-morphism and χ is a (i ∗ e∗)-morphism then ϕ2 is (∗ ∗ ∗∗)-morphism andχ1 is a (i ∗ e∗)-morphism.
P ROOF. Consider the following pushout of FOL signature morphisms.
(S2 , F2 , P2 )
O

ϕ2

χ

(S, F, P)/ (S0 , F 0 , P0 )Oχ1ϕ/ (S1 , F1 , P1 )Remark 20 By the pushout construction in the category of sets, the above pushout has thefollowing properties:
6 We say that a category C has (L , R )-pushouts for two subcategories L , R ⊆ C , if for each span of morphisms
v1
u2
v
u
v
u
A2 ← A0 → A1 such that u ∈ L and v ∈ R there exists a pushout {A2 ← A0 → A1 , A1 →
A←
A2 }.

9

1. χ1 is injective on sorts,
2. for all s1 ∈ S1 and s2 ∈ S2 such that χ1 (s1 ) = ϕ2 (s2 ) there exists s ∈ S such that ϕ(s) = s1
and χ(s) = s2 , and3. ϕ2 is injective on S2 − χ(S).
Also note that χ1 and ϕ2 map constants to constants only.
Let F 0c = χ1 (F1c ) ∪ ϕ2 (F2c ), where• F 0c = {Fw0c0 →s0 }w0 ∈S0∗ , ands0 ∈S0• Fw0c0 →s0 = (∪χ1 (w1 ,s1 )=(w0 ,s0 ) χ1 ((F1c )w1 →s1 )) ∪ (∪ϕ2 (w2 ,s2 )=(w0 ,s0 ) ϕ2 ((F2c )w2 →s2 )).
We prove that
(S2 , F2 , F2c , P2 )O

ϕ2

/ (S0 , F 0 , F 0c , P0 )Oχ(S, F, F c , P)

χ1ϕ

/ (S1 , F1 , F c , P1 )1

is a pushout of CFOL signature morphisms.
Firstly, we show that χ1 is a (i∗e∗)-morphism. By the definition of F 0c all the constructors
in F1c are preserved by χ1 . Now let σ0 ∈ Fw0c0 →χ (s ) , where s1 ∈ S1 . There are two cases:
11

1. There exists σ1 ∈ (F1c )w1 →st1 such that χ1 (σ1 ) = σ0 . Note that χ1 (s1 ) = χ1 (st1 ) andsince χ1 is injective on sorts, s1 = st1 . Therefore χ1 (σ1 : w1 → s1 ) = σ0 : w0 → χ1 (s1 ).
2. There exists σ2 ∈ (F2c )w2 →st2 such that ϕ2 (σ2 ) = σ0 . We have ϕ2 (st2 ) = χ1 (s1 ). By
Remark 20 there exists s ∈ S such that ϕ(s) = s1 and χ(s) = st2 . Since χ is a (i ∗ e∗)cmorphism there exists σ ∈ Fw→ssuch that χ(σ) = σ2 . Now take σ1 : w1 → st1 = ϕ(σ :w → s). We have χ1 (st1 ) = χ1 (s1 ) and by the injectivity of χ1 we get s1 = st1 . Thereforeχ1 (σ1 : w1 → s1 ) = σ0 : w0 → χ1 (s1 ).
Secondly, we show that ϕ2 is a CFOL signature morphism. Again by the definition of
F 0c all the constructors in F2c are preserved by ϕ2 . Let σ0 ∈ Fw0c0 →ϕ (s ) , where s2 ∈ S2c . We
2 2have two cases:
1. s2 ∈ χ(Sc ). Let s ∈ Sc such that χ(s) = s2 . Since χ1 is a (i ∗ e∗)-morphism and ϕ(s) ∈S1c , there exists σ1 ∈ (F1c )w1 →ϕ(s) such that χ1 (σ1 ) = σ0 . Because s ∈ Sc , there existscsuch that ϕ(σ) = σ1 . Take σ2 = χ(σ) and we have ϕ2 (σ2 : χ(w) → s2 ) = σ0 :σ ∈ Fw→s0
w → ϕ2 (s2 ).
2. s2 ∈ S2c − χ(Sc ). Since χ is a (i ∗ e∗)-morphism we have s2 ∈ S2 − χ(S). By the definition of F 0c we have two subcases:(a) There exists σ1 ∈ (F1c )w1 →st1 such that χ1 (σ1 ) = σ0 . Because χ1 (st1 ) = ϕ2 (s2 )there is s ∈ S such that χ(s) = s2 and ϕ(s) = st1 which is a contradiction withs2 ∈ S2 − χ(S).

10

(b) There exists σ2 ∈ (F2c )w2 →st2 such that ϕ2 (σ2 ) = σ0 . We have s2 ∈ S2 − χ(S) andϕ2 (s2 ) = ϕ2 (st2 ) which by Remark 20 implies s2 = st2 . Therefore ϕ2 (σ2 : w2 →s2 ) = σ0 : w0 → ϕ2 (s2 ).
Now we show that for all vi : (Si , Fi , Fic , Pi ) → (S00 , F 00 , F 00c , P00 ), where i ∈ {1, 2}, such thatϕ; v1 = χ; v2 there exists a unique v : (S0 , F 0 , F 0c , P0 ) → (S00 , F 00 , F 00c , P00 ) such that χ1 ; v = v1
and ϕ2 ; v = v2 . A unique v exists as a FOL signature morphism. We need to prove that v isa CFOL signature morphism. Let σ00 ∈ Fw00c00 →v(s0 ) , where s0 ∈ S0c . By the definition of F 0c ,either there is s1 ∈ S1c such that χ(s1 ) = s0 or there is s2 ∈ S2c such that ϕ(s2 ) = s0 . Assume
that there exists s1 ∈ S1c such that χ1 (s1 ) = s0 (the other case is similar). Since v1 is a CFOL
signature morphism there is σ1 ∈ (F1c )w1 →s1 such that v1 (σ1 ) = σ00 . Now take σ0 = χ1 (σ1 )and we have v(σ0 : χ1 (w1 ) → s0 ) = σ00 : w00 → v(s0 ).
The condition χ is a (i ∗ e∗)-morphism is necessary for Proposition 19 as one can see in theexamples below.
Example 21 Consider the following pushout in FOL:
sortO sχ

ϕ2⊆

sort s/ op a : s {constr}
op b : s{constr}
O

s17→s
s27→s

sort s1
sort s2

χ1

ϕ
⊆

s17→s
s27→s
(a:s1)7→(a:s)(b:s2)7→(b:s)

sorts s1,s2/ op a : s1 {constr}
op b : s2{constr}

Note that χ is not injective on sorts, and since there is no constructor (c : s1) such that χ1 (c :s1) = (b : s), χ1 is not a CFOL signature morphisms.
Example 22 Consider the following pushout in FOL:
sort sop b : s{constr}O

ϕ2⊆

sort s/ op a : s {constr}
op b : s {constr}Oχ ⊆sort s

χ1 ⊆
ϕ
⊆

/

sort sop a : s {constr}

Note that the condition “no constructors of ‘old’ sorts” is not fulfilled by χ and ϕ, and since χ1adds the constructor b of the ‘old’ constrained sort s, χ1 is not a CFOL signature morphism.
Proposition 19 provides a method of constructing pushouts of signatures in other constructor-based institutions such as CPOA. Initially, the construction is done in the base institution, for example in POA, and then it is extended to the constructor-based variant, such as
CPOA.
11

3.2

Pushouts of presentation morphisms

The pushouts of presentation morphisms have been playing a very important role in algebraic
specifications [20, 15] as it constitutes the basis of constructing large specifications out ofsmaller ones.
Proposition 23 [20] Let I = (Sig, Sen, Mod, |=) be an institution, and L , R ⊆ Sig two subcategories of signature morphisms. If Sig has (L , R )-pushouts then the presentation morphisms have (L pres , R pres )-pushouts, where
ϕ

ϕ

χ

χ

• L pres consists of presentation morphisms (Σ, E) → (Σ0 , E 0 ) such that Σ → Σ0 ∈ L ,• R pres consists of presentation morphisms (Σ, E) → (Σ0 , E 0 ) such that Σ → Σ0 ∈ R .
Parameterization is one of the most important technique used in structuring formal specifications. A parameterized presentation is a presentation morphism χ : (P, EP ) → (B[P], EB [EP ]),where (P, EP ) is the parameter and (B[P], EB [EP ]) the body, such that χ : P → B[P] is
1. an inclusive signature morphism, and
2. a (∗ ∗ e∗)-morphism (it does not add new constructors to the parameter).
Parameterization allows to abstract away the elements of a system that are not part of theessence, and can be obtained at a later time by instantiation. The pushout construction constitutes the basis of the instantiation mechanism. To instantiate (P, EP ) with (T, ET ) requires aparameter mapping ϕ : (P, EP ) → (T, ET ), and the result of the instantiation is the vertex of the
χ
χ1
ϕ
ϕ2
pushout {(B[P], EB [EP ]) ← (P, EP ) → (T, ET ), (B[P], EB [EP ]) → (B[T ], EB [ET ] ← (T, ET )},where EB [ET ] = ϕ2 (EB [EP ]) ∪ χ1 (ET ).

3.3

Semi-exactness

A basic institutional property that is necessary for combining specifications coherently withrespect to the semantics is the semi-exactness property.
Definition 24 An institution I = (Sig, Sen, Mod, |=) is (L , R )-semi-exact, where L , R ⊆Sig are two subcategories of signature morphisms, if for each (L , R )-pushout of signaturemorphisms
ϕ2
/ Σ0
ΣO 2
O
χ

χ1

Σ

ϕ

/ Σ1

the following diagram
Mod(ϕ2 )Mod(Σ2 ) oMod(χ1 )Mod(χ)

Mod(Σ) oMod(Σ0 )Mod(ϕ)

Mod(Σ1 )is a pullback in Cat. The institution I is semi-exact if L = R = Sig.
12

Proposition 25 [30] FOL is semi-exact.
We lift up the semi-exactness property from the base institution FOL to its constructor-based
variant CFOL.
Proposition 26 CFOL is ((∗ ∗ ∗∗), (i ∗ e∗))-semi-exact.
P ROOF. Assume a pushout of CFOL signature morphisms/ (S0 , F 0 , F 0c , P0 )O

ϕ2

(S2 , F2 , F2c , P2 )Oχχ1(S, F, F c , P)

/ (S1 , F1 , F c , P1 )1

ϕsuch that χ is a (i ∗ e∗)-morphism and ϕ is a (∗ ∗ ∗∗)-morphism. Since FOL is semi-exact
and for all CFOL signatures (Si , Fi , Fic , Pi ), Mod(Si , Fi , Fic , Pi ) is the full subcategory of
Mod(Si , Fi , Pi ), it suffices to prove that for all models M1 ∈ Mod(S1 , F1 , F1c , P1 ) and M2 ∈Mod(S2 , F2 , F2c , P2 ) such that M1 ϕ = M2 χ there exists M 0 ∈ Mod(S0 , F 0 , F 0c , P0 ) such thatM 0 χ1 = M1 and M 0 ϕ2 = M2 .
0
By Proposition 25, there exists a model M 0 ∈ Mod(S0 , F 0 , P0 ) such that
 M0 χ1 =0 M1 and
Ms0 if s ∈ S0l
M 0 ϕ2 = M2 . Let M 0l be the S0 -sorted set such that for all s0 ∈ S0 , Ms0l0 =.
0/
if s0 6∈ S0l
Let conM0 : T(S0 ,F 0c ) (M 0l ) → M 0 (S0 ,F 0c ) be the unique extension of the inclusion {Ms0l0 ,→Ms0 0 }s0 ∈S0 to a model (S0 , F 0c )-morphism. If we prove that conM0 is surjective on the sortsin χ1 (S1 ) and ϕ2 (S2 ), since S0 = χ1 (S1 ) ∪ ϕ2 (S2 ), it follows that conM0 is surjective, meaningthat M 0 ∈ Mod(S0 , F 0 , F 0c , P0 ).
1. 
We define the S1 -sorted set M1l such that for all sorts s1 ∈ S1 , we have (M1l )s1 =(M1 )s1 if s1 ∈ S1l. Let conM1 : T(S1 ,F1c ) (M1l ) → M1 (S1 ,F1c ) be the unique exten0/
if s1 6∈ S1l
sion of the inclusion {(M1l )s1 ,→ (M1 )s1 }s1 ∈S1 to a (S1 , F1c )-morphism. By Proposition
19, χ1 is a (i ∗ e∗)-morphism, which implies that χ1 (S1l ) ⊆ S0l . It follows that the following inclusion exists {(M1l )s1 ,→ (T(S0 ,F 0c ) (M 0l ))χ1 (s1 ) }s1 ∈S1 .
Let hM1 : T(S1 ,F1c ) (M1l ) → T(S0 ,F 0c ) (M 0l ) (S1 ,F1c ) be the unique extension of the inclusion{(M1l )s1 ,→ (T(S0 ,F 0c ) (M 0l ))χ1 (s1 ) }s1 ∈S1 to a model (S1 , F1c )-morphism. Note that for allm ∈ M1l , conM1 (m) = (hM1 ; conM0 (S1 ,F1c ) )(m), which implies that the following diagram is commutative.
conM1

T(S1 ,F1c ) (M1l )hM1(/ M1 (S ,F c )1 1
7conM 0 (S ,F c )1 1

T(S0 ,F 0c ) (M 0l ) (S1 ,F1c )Since conM1 is surjective we obtain that conM0 (S1 ,F1c ) is surjective, meaning that conM0
is surjective on the sorts in χ1 (S1 ).
13

(M2 )s2 if s2 ∈ S2l.
0/
if s2 6∈ S2l
Let conM2 : T(S2 ,F2c ) (M2l ) → M2 (S2 ,F2c ) be the unique extension of following inclusion{(M2l )s2 ,→ (M2 )s2 }s2 ∈S2 to a (S2 , F2c )-morphism. We define the S2 -sorted function
hM2 = {(hM2 )s2 : (M2l )s2 → (T(S0 ,F 0c ) (M 0l ))ϕ2 (s2 ) }s2 ∈S2 . For all s2 ∈ S2l such that ϕ2 (s2 ) ∈S0l , and m ∈ (M2l )s2 , we define hM2 (m) = m. Let s2 ∈ S2l such that ϕ2 (s2 ) ∈ S0c , andm ∈ (M2l )s2 . By the pushout construction, S0c = χ1 (S1c ) ∪ ϕ2 (S2c ). There exists s1 ∈ S1csuch that χ1 (s1 ) = ϕ2 (s2 ). Since conM0 is surjective on the sorts in χ1 (S1 ), there exists
t 0 ∈ (T(S0 ,F 0c ) (M 0l ))ϕ2 (s2 ) such that conM0 (t 0 ) = m. We define hM2 (m) = t 0 . Note that for
all sorts s2 ∈ S2 , we have (hM2 )s2 ; (conM0 )ϕ2 (s2 ) = (conM2 )s2 .

2. Let M2l be the S2 -sorted set such that for all s2 ∈ S2 , (M2l )s2 =Let h#M2 : T(S2 ,F2c ) (M2l ) → T(S0 ,F 0c ) (M 0l ) (S2 ,F2c ) be the unique extension of hM2 to a model(S2 , F2 )-morphism, and note that the following diagram is commutative.
conM2

T(S2 ,F2c ) (M2l )
h#M

2

(

/ M2 (S ,F c )2 2
7
conM 0 (S ,F c )2 2

T(S0 ,F 0c ) (M 0l ) (S2 ,F2c )Since conM2 is surjective, conM0 (S2 ,F2c ) is surjective, which implies that conM0 is surjective on the sorts in ϕ2 (S2 ).

The ideas of lifting semi-exactness from the base institution to the constructor-based variant provided by Proposition 26 can be applied in other cases such as preorder algebra.

4

Initial models

In this section we provide sufficient institution-independent conditions for a set of Horn sentences to have an initial model.
Definition 27 Let I = (Sig, Sen, Mod, |=) be an institution with a sub-functor Sen0 : Sig →Set of Sen, and a subcategory D ⊆ Sig of signature morphisms. A D -Horn sentence overVχ
Sen0 (Σ) is a sentence semantically equivalent to (∀χ) H ⇒ C, where Σ → Σ0 ∈ D , C ∈0
0
Sen0 (Σ ) and H ⊆ Sen0 (Σ ).
VWhen the sub-functor Sen0 and the subcategory D are fixed, we call (∀χ) H ⇒ C,
simply, Horn sentence.
An example of institution I = (Sig, Sen, Mod, |=) as in Definition 27 is CHCL, where theinstitution I0 = (Sig, Sen0 , Mod, |=) is the restriction CHCL0 of CHCL to atomic sentences,and D consists of signature extensions with a finite number of constants.
Note that not all sets of sentences in CHCL have an initial model. If we restrict thesignatures such that all operators of constrained sorts are constructors then we obtain initiality
for Horn sentences (i.e. any set of sentences in RHCL has an initial model). Abstractly weassume14

1. an institution I as in Definition 27, and
2. a subcategory Sigr ⊆ Sig of signature morphisms.
Let Senr : Sigr → Set, Senr0 : Sigr → Set and Mod r : (Sigr ) → Cat op be the functors define
as the restrictions of Sen : Sig → Set, Sen0 : Sig → Set and Mod : Sig → Cat op , respectively,de f

to Sigr . We also define |=r = {|=Σ }Σ∈|Sigr | .
Fact 28 I r = (Sigr , Senr , Mod r , |=r ) and I0r = (Sigr , Senr0 , Mod r , |=r ) are institutions.
We provide ‘easy-to-check’ institution-independent conditions for any set of sentencesin I r to have an initial model. Our methodology of proving initiality follows exactly the
structure of the sentences:
1. we assume that all sentences of I0r are epi basic;
2. based on this assumption, which is checked in concrete examples of institutions, we
prove that any set of quantifier-free Horn sentences in I r has an initial model;
3. we extend the initiality result to the quantified Horn sentences of I r .
One may wonder what is the role played by I in the abstract setting. The answer issimple: I provides the subcategory D of signature morphisms and the satisfaction relation
for quantified sentences. If I is CHCL and I r is RHCL then it is easy to notice that asignature extension with constants of constrained sorts is not a signature morphism in RHCL.
Therefore in concrete examples we have D 6⊆ Sigr .

4.1

Quantifier-free layer

Assume an institution I = (Sig, Sen, Mod, |=) and a sub-functor Sen0 : Sig → Set of Sen. We
denote by I0 the institution (Sig, Sen0 , Mod, |=). A concrete example of such institution is
RHCL such that I0 is the restriction of RHCL to atomic sentences.
Proposition 29 If all sets ofsentences in I0 are epi basic then every set Γ of Σ-sentencesV
semantically equivalent to H ⇒ C, where H ⊆ Sen0 (Σ) and C ∈ Sen0 (Σ), has an initialmodel .
P ROOF. Let Σ ∈ |Sig| and Γ ⊆ Sen(Σ). We define Γ0 = {e ∈ Sen0 (Σ) | Γ |= e}. Let MΓ0 be
the basic model of Γ0 . We prove that MΓ0 is the initial model of Γ. If M |= Γ then M |= Γ0 ,and since Γ0 is epi basic, there exists a unique morphism MΓ0 → M. We only need to showVMΓ0 |= Γ. Let H ⇒ C ∈ Γ and assume MΓ0 |= H. Since H is basic, there exists
a modelVmorphism MH → MΓ0 , which implies Γ0 |= H, and we obtain Γ |= H. Since H ⇒ C ∈ Γand Γ |= H, we get Γ |= C. It follows that C ∈ Γ0 and hence MΓ0 |= C.
Corollary 30 In RHCL and RHPOA, any set of quantifier-free sentences has an initialmodel that is ground reachable.
P ROOF. We set the parameters of Proposition 29 for RHCL. The other case is similar. I =RHCL and I0 = RHCL0 is the restriction RHCL to atomic sentences. By Lemma 11, theRHCL0 sentences are epi basic, and by Proposition 29, any set of quantifier-free RHCL
sentences has an initial model. Since the initial models are basic models, by Remark 15, they
are also ground reachable.
15

4.2

Quantification layer

Assume an institution I = (Sig, Sen, Mod, |=) with a broad subcategory D ⊆ Sig of signature morphisms, and a sub-functor Sen1 of Sen such that all sentences of I are semanticallyχ
equivalent to (∀χ)ρ, where Σ → Σ0 ∈ D and ρ ∈ Sen1 (Σ0 ). An example of such institution
is CHCL such that D is the subcategory of signature extensions with a finite number of
constants, I1 = (Sig, Sen1 , Mod, |=) is the restriction CHCL1 of CHCL to quantifier-free
sentences.
Any subcategory of signature morphisms Sigr ⊆ Sig determines two institutions I r =(Sigr , Senr , Mod r , |=r ) and I1r = (Sigr , Senr1 , Mod r , |=r ) as in Fact 28. If Sigr is the full subcategory of CHCL signature morphisms such that all operators of constrained sorts are constructors then I r = RHCL, and I1r = RHCL1 , the restriction of RHCL to quantifier-free
sentences.
Theorem 31 All sets of sentences in I r have an initial model when all sets of sentences in
I1r have an initial model, which is D -reachable in I .
P ROOF. Let Σ ∈ |Sigr | and Γ ⊆ Sen(Σ). We define Γ1 = {e ∈ Sen1 (Σ) | Γ |= e}. The set
Γ1 has an initial model MΓ1 which is D -reachable. If M |= Γ then M |= Γ1 . Since MΓ1 is
the initial model of Γ1 , there exists a unique morphism MΓ1 → M. We only need to proveχMΓ1 |= Γ. Let (∀χ)ρ ∈ Γ, where Σ → Σ0 ∈ D and ρ ∈ Sen1 (Σ0 ), and N be a χ-expansion ofMΓ1 . Since MΓ1 is D -reachable, there exists a substitution θ : χ → 1Σ such that MΓ1 θ = N.
Since (∀χ)ρ |= θ(ρ), we obtain θ(ρ) ∈ Γ1 . It follows MΓ1 |= θ(ρ), and by the satisfaction
condition N |= ρ.
Corollary 32 In RHCL and RHPOA, any set of sentences has an initial model.
P ROOF. We set the parameters of Theorem 31 for RHCL. The other case is similar. I
is CHCL, I1 is the restriction of CHCL to the quantifier-free sentences, I r is RHCL andI1r is the restriction of RHCL to the quantifier-free sentences. By Corollary 30, every setof quantifier-free sentences in RHCL has an initial model which is ground reachable. By
Theorem 31, every set of sentences in RHCL has an initial model.

4.3

Sufficient completenessFw→s : s ∈ Sc
. A CHCL
0/ : s 6∈ Sc
presentation ((S, F, F c , P), E) is called sufficient complete if for all (S, F, F c , P)-models M
scpresthat satisfies E we have M ∈ Mod(S, F, F c , P). Let SigCHCL ⊆ SigCHCL be the full subsc
category of sufficient complete presentations: |SigCHCL | consists of CHCL presentations((S, F, F c , P), E) that are sufficient complete. We define the institution CHCLsc of sufficientcomplete presentations as the the restriction of CHCL pres to the sufficient complete presentations:Sc =For any CHCL signature (S, F, F c , P), recall that Fw→s

sc

sc

• |=CHCL = {|=CFOL
(Σ,E)

pres

sc



sc

• SenCHCL : SigCHCL → Set and Mod CHCL : SigCHCL → Cat op are the restrictions
pres
pres
pres
pres
of the SenCHCL : SigCHCL → Set and Mod CHCL : SigCHCL → Cat op , resc
CHCL
spectively, to Sig;
sc}(Σ,E)∈|SigCHCLsc | .
16

Similarly, one can define the institution CHPOAsc of sufficient complete CHPOA presentations.
Proposition 33 In CHCLsc and CHPOAsc , any set of sentences has an initial model.
P ROOF. Let ((S, F, F c , P), E) be a sufficient complete CHCL presentation, and Γ a set ofc(S, F, F c , P)-sentences. By Corollary 32, Mod((S, F, F S , P), E ∪ Γ) has an initial modelc
OE∪Γ . Since ((S, F, F , P), E) is sufficient complete, OE∪Γ ∈ Mod(S, F, F c , P). Since OE∪Γ iscthe initial model of Mod((S, F, F S , P), E ∪ Γ) and Mod((S, F, F c , P), E ∪ Γ) is the full subcatc
egory of Mod((S, F, F S , P), E ∪Γ), we obtain that OE∪Γ is the initial model of Mod((S, F, F c , P), E ∪Γ).
The case of CHPOAsc is similar.

5Free models

In this section we give sufficient institution independent conditions for proving the existenceof free models along sufficient complete presentation morphisms in constructor-based institutions. Our ideas are based upon [31] and especially [10]. More concrete, we notice that
one of the conditions of the result in [10] is too restrictive and we replace it with a somewhat
less restrictive variant, such that we can apply it in more cases. We also define the conceptof weak diagrams for CFOL which is essential for proving the existence of free models andprovides ideas to define it for other constructor-based institutions.

5.1

Institution-independent diagrams

In this paper we present a simplified version of institutional diagrams of [10], which omits
the compatibility of this notion with the signature morphisms.
Definition 34 An institution I = (Sig, Sen, Mod, |=) has weak diagrams ι if for each signature Σ, and Σ-model A there exists a signature morphism ιΣ (A) : Σ → ΣA called the extension of Σ via A, and a set EA of ΣA -sentences called the diagram of the model A such that
Mod(ΣA , EA ) and the comma category A/Mod(Σ) are naturally isomorphic, i.e. the following diagram commutes by the isomorphism iΣ,A natural in Σ and A.
Mod(ΣA , EA )Mod(ιΣ (A))

iΣ,A

&
x
Mod(Σ)/ A/Mod(Σ)
forgetful

1

A
Remark 35 Since the comma category A/Mod(Σ) has an initial model A →A and iΣ,A is an
isomorphism of categories, the followings hold:

1. Mod(ΣA , EA ) has an initial model AA such that AA ιΣ (A) = A, and
2. for all M ∈ Mod(ΣA , EA ), iΣ,A (M) = (AA → M) ιΣ (A) , where AA → M is the uniquemorphism from AA to M.
We define the diagrams for CFOL. Let A be a Σ-model, where Σ = (S, F, F c , P).
17• ΣA consists of the signature Σ enrichedwith all elements of loose sorts of A, i.e. ΣA =lF→s ∪ As i f w = λ and s ∈ S(S, FA , F c , P), where (FA )w→s =Fw→sotherwise• ιΣ (A) : (S, F, F c , P) ,→ (S, FA , F c , P) is the inclusion of signatures,• AA is the ιΣ (A)-expansion of A interpreting each a ∈ A as a, and• EA is the set of all ΣA -atoms satisfied by AA .
Proposition 36 In CFOL, for each Σ-model A, where Σ = (S, F, F c , P) there exists an isomorphisms of categories iΣ,A : Mod(ΣA , EA ) → A/Mod(Σ).
P ROOF. Let fAA : T(S,FA ,P) → AA be the unique morphisms from T(S,FA ,P) to AA . Since A is areachable model, fAA is a surjection.
We show that AA is the basic model of EA . Assume a ΣA -model M, and let fM : T(S,FA ,P) →M be the unique morphism from T(S,FA ,P) to M.
1. If M |= EA then Ker( fAA ) ⊆ Ker( fM ), and there exists a unique model morphism hM :AA → M such that fAA ; hM = fM .
2. If there exists hM : AA → M, then by the initiality of T(S,FA ,P) , we have fAA ; hM = fM .
Since AA is ground reachable, for all atomic ΣA -sentences e, AA |= e implies M |= e. It
follows that M |= EA .
Since AA is the basic model of EA , AA /Mod(ΣA ) = AA /Mod(ΣA , EA ). Because AA is theinitial model of Mod(ΣA , EA ), the forgetful functor F : AA /Mod(ΣA , EA ) → Mod(ΣA , EA ) is
an isomorphisms of categories. Also, the functor IΣ,A : AA /Mod(ΣA ) → A/Mod(Σ) defined
h

h

h

h

M
M
by IΣ,A (AA →M) = (AA →M) ιΣ (A) on models, and by IΣ,A (hM → hN ) = (hM → hN ) ιΣ (A)on morphisms, is an isomorphism of categories. Then iΣ,A = F −1 ; IΣ,A is also an isomorphismof categories as a composition of two isomorphisms.

In institutions with no constructors, such as FOL, all sorts are loose, and the extensionιΣ (A) of a signature Σ via a Σ-model A is obtained by adding all the elements of the model A
to the signature Σ. This is the classical approach, which can be found, for example, in [10].
Proposition 37 [12] If I is an institution with weak diagrams ι then the institution of presentations I press has also elementary diagrams.
P ROOF. [Sketch] Let (Σ, E) be a presentation, and A a Σ-model that satisfies E. The extensionof (Σ, E) via A in I pres is ιΣ (A) : (Σ, E) → (ΣA , ιΣ (A)(E)) and the diagram of the (Σ, E)-model
A is EA .
Corollary 38 CHCLsc has weak diagrams.
P ROOF. Assume a sufficient complete CHCL presentation (S, F, F c , P), E), and let A be a
(S, F, F c , P)-model that satisfies E. Note that (S, FA , F c , P), E) is sufficient complete, whereι(S,F,F c ,P)(A) : (S, F, F c , P) ,→ (S, FA , F c , P) is the extension of (S, F, F c , P) via A. Indeed, forccany M ∈ Mod((S, FA , F S , P), E), M (S,F,P) ∈ Mod((S, F, F S , P), E); since (S, F, F c , P), E) issufficient complete, M (S,F,P) ∈ Mod((S, F, F c , P), E), which implies M ∈ Mod((S, FA , F c , P), E).
In CHCLsc , let18• ι(S,F,F c ,P)(A) : ((S, F, F c , P), E) ,→ ((S, FA , F c , P), E) be the extension of the presentation(S, F, F c , P), E) via A, and• the diagram EA of A in CHCL be the diagram of A in CHCLsc .
By Proposition 37, the following diagram is commutative.
i((S,F ,F c ,P),E),A/ A/Mod((S, F, F c , P), E)

A

Mod(((S, FA , F c , P), E), EA )Mod(ι(S,F,F c ,P) (A))

forgetful*tMod((S, F, F c , P), E)

Note that the signature morphisms in CFOL do not preserve the loose sorts, in general.
It follows that our notion of diagrams is not ‘functorial’ in the sense of [10], which implies
that CFOL does not have elementary diagrams.

5.2

Liberality

An institution I = (Sig, Sen, Mod, |=) is L -liberal [20], where L ⊆ Sig, if for all presentationϕϕmorphisms (Σ, E) → (Σ0 , E 0 ) such that Σ → Σ0 ∈ L the functor
Mod(ϕ)

Mod(Σ0 , E 0 ) −→ Mod(Σ, E)
has a left adjoint.
The following theorem can be proved as in [10].
Theorem 39 Let I = (Sig, Sen, Mod, |=, ι) be an institution with weak diagrams. Assume
two categories L , R ⊆ Sig of signature morphisms such that
1. ιΣ (A) ∈ R , for all Σ ∈ |Sig| and A ∈ |Mod(Σ)|,
2. Sig has (L , R )-pushouts,
3. I is (L , R )-semi-exact, and4. each presentation has an initial model.
Then I is L -liberal.
ϕ

P ROOF. [sketch] Let ϕ : (Σ, E) → (Σ0 , E 0 ) be a presentation morphism such that Σ → Σ0 ∈L , and let A be a Σ-model that satisfies E. Consider the following pushout of signaturemorphisms
ϕ0

ΣO A

/ Σ00
O
ι0

ιΣ (A)

Σ

ϕ

ϕ0

/ Σ0
ϕ0

We define the free model Aϕ to be (AA ) ι0 where AA is the initial model of ϕ0 (EA ) ∪ ι0 (E 0 ),ϕ0

and the the universal arrow ηA : A → (Aϕ ) ϕ to be (AA → (AA ) ϕ0 ) ιΣ (A) .
19

Below is a corollary of the above theorem.
Corollary 40 CHCLsc is (∗ ∗ e∗)-liberal.
P ROOF. We set the parameters of Theorem 39. The institution I is CHCLsc , L consists ofsufficient complete presentation (∗ ∗ e∗)-morphisms, and R consists of sufficient complete
presentation morphisms that add non-constructor constants of loose sorts. By Proposition 33,
each set of sentences in CHCLsc has an initial model. For each span of CHCLsc signatureχϕmorphism ((S, F ∪C, F c , P), EC ) ←- ((S, F, F c , P), E) → ((S1 , F1 , F1c , P1 ), E1 ) such that ϕ is a(∗ ∗ e∗)-morphism, and C is set of constants of loose sorts, the following pushout((S, F ∪C, F c , P), EC )O

ϕC

/ ((S1 , F1 ∪C0 , F c , P1 ), E 0 )
O 1

χ

χ1

?

((S, F, F c , P), E)ϕχ?
/ ((S1 , F1 , F c , P1 ), E1 )
1
ϕ

ϕ

C
is constructed as follows: {(S, F ∪C, F c , P) ←- (S, F, F c , P) → (S1 , F1 , F1c , P1 ), (S, F ∪C, F c , P) →

χ1

(S1 , F1 ∪ C0 , F1c , P1 ) ←- (S1 , F1 , F1c , P1 )} is a pushout of CFOL signature morphisms, andE 0 = ϕC (EC ) ∪ χ1 (E1 ). Note that• χ1 is the extension of (S1 , F1 , F1c , P1 ) with constants from C0 , and• ϕC works like ϕ on (S, F, F c , P).
Let M1 ∈ Mod((S1 , F1 , F1c , P1 ), E1 ) and M2 ∈ Mod((S, F ∪C, F c , P), EC ) such that M1 ϕ =M2 χ . By Proposition 26, there exists M 0 ∈ Mod(S1 , F1 ∪ C0 , F1c , P1 ) such that M 0 χ1 = M1
and M 0 ϕC = M2 . By the satisfaction condition, M 0 |= E 0 . It follows that CHCLsc is (L , R )semi-exact.
By Theorem 39, ϕ has a left adjoint.
Similar results can be formulated for CHPOA too.
The example below shows that CHCLsc is not liberal, in general.
Example 41 Consider the following example of CHCL signature morphism:
sort Trivϕ
Triv7→Boolsort Bool/ op true : Bool{constr}
op false : Bool{constr}

/ 0,
/ 0)
/ and BOOL = ({Bool}, {true :→ Bool, f alse :→ Bool}, {true :→where T RIV = ({Triv}, 0,/ Let A be a T RIV -model that consists of one element (a : Triv). AsBool, f alse :→ Bool}, 0).
sume that Aϕ is the free model along ϕ generated by A, and ηA : A → Aϕ ϕ is an universal arrow. Let TBOOL be the term BOOL-model, and f1 : A → TBOOL ϕ defined by f1 (a) = true. By
the universality of ηA , there exists a model morphism h1 : Aϕ → TBOOL such that ηA ; h1 ϕ = f1 .
ϕϕϕϕ
If Atrue = A f alse then h1 (Atrue ) = h1 (A f alse ), which implies (TBOOL )true = (TBOOL ) f alse , aϕϕcontradiction. Since Aϕ is reachable and Atrue 6= A f alse , h1 is an isomorphism. We haveϕ−1
ηA (a) = h−1
1 ( f 1 (a)) = h1 ((TBOOL )true ) = Atrue . Let f 2 : A → TBOOL ϕ , defined by f 2 (a) =f alse. By the universality of ηA , there exists a model morphism h2 : Aϕ → TBOOL such thatϕϕ
ηA ; h2 ϕ = f2 . Since Aϕ is reachable and Atrue 6= A f alse , h2 is an isomorphism. We haveϕϕϕ−1
ηA (a) = h−1
2 ( f 2 (a)) = h2 ((TBOOL ) f alse ) = A f alse . We obtained Atrue = ηA (a) = A f alse , acontradiction. Therefore, ηA is not an universal arrow.
20

6Conclusions

We investigate the existence of pushouts in the concrete category of CFOL signature morphisms. This research is important as the pushout construction constitutes the basis of building large specifications from smaller ones. In connection to the semantics of the complex
system development we conduct an institution dependent study of the semi-exactness property in logics with constructors.
We proved the existence of initial models of any set of sentences in arbitrary ‘reachable’
institutions. We do not use factorization systems as [2, 33, 1] or inclusion systems as [10].
We simply require that all sets of atoms are basic and the models defining the sets of atoms
as basic sets of sentences are ground reachable. Note that the restriction to reachable models
can be also obtained by allowing infinitary disjunctions. For example, if Σ = ({Nat}, {0 :→/ is a first-order signature then the restriction to the models that are
Nat, s : Nat → Nat}, 0)
reachable by the constructors
0 :→ Nat and s : Nat → Nat can be obtained by using theWinfinitary sentence (∀x) n∈Nat x = sn 0, where sn 0 is the term obtained by applying n times
the function successor to 0. It follows that the class of models of an implicational theory inlogics with constructors do not form a quasi-variety, and do not fall into the framework of[2, 33, 10]. Therefore new initiality results are required for ‘reachable’ institutions. Initiality
is then extended to constructor-based institutions via sufficient completeness.
Free models along presentation morphisms provide semantics for the modules with initialdenotation in algebraic specifications. In order to provide an institution independent proofof liberality, we define the diagrams for logics with constructors. Given a Σ-model A, theextension of Σ via A is obtained by adding all elements of loose sorts of A to the signature
Σ. Taking into consideration that constructor-based institutions do not have all pushouts,
freeness follows as in [10], and then it is instantiated to the institution of sufficient complete
presentations.
Our abstract results can be applied to other frameworks such as order sorted algebra[22, 21], higher order logic [6, 24] with intensional Henkin semantics, and partial algebra[28, 5]. In the future we are planning to study interpolation in logics with constructors. Alsoan axiomatizability result is desired in this case.

References[1] J. Adámek, H. Herrlich, and G. Strecker. Abstract and concrete categories. WileyInterscience, New York, NY, USA, 1990.
[2] H. Andréka and I. Németi. Generalization of the concept of variety and quasivariety topartial algebra through category theory. Dissertationes Mathematicae, CCIV, 1983.
[3] M. Bidoit and R. Hennicker. Constructor-based observational logic. J. Log. Algebr.
Program., 67(1-2):3–51, 2006.
[4] M. Bidoit, R. Hennicker, and A. Kurz. Observational logic, constructor-based logic,
and their duality. Theor. Comput. Sci., 3(298):471–510, 2003.
[5] P. Burmeister. A Model Theoretic Oriented Approach to Partial Algebras. AkademieVerlag, 1986.

21

[6] A. Church. A formulation of the simple theory of types. J. Symb. Log., 5(2):56–68,
1940.
[7] M. Codescu and D. Găină. Birkhoff completeness in institutions. Logica Universalis,2(2):277–309, September 2008.
[8] R. Diaconescu. Extra theory morphisms for institutions: logical semantics for multiparadigm languages. Applied Categorical Structures, 6(4):427–453, 1998. A preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997.
[9] R. Diaconescu. Institution-independent ultraproducts. Fundamenta Informaticae, 55(34):321–348, 2003.
[10] R. Diaconescu. Elementary diagrams in institutions. Journal of Logic and Computation,
14(5):651–674, 2004.
[11] R. Diaconescu. Herbrand theorems in arbitrary institutions.
90(1):29–37, 2004.

Inf. Process. Lett.,[12] R. Diaconescu. Institution-independent Model Theory. Birkhäuser Basel, 1st edition,
2008.
[13] R. Diaconescu and K. Futatsugi. CafeOBJ Report: The Language, Proof Techniques,
and Methodologies for Object-Oriented Algebraic Specification, volume 6 of AMAST
Series in Computing. World Scientific, 1998.
[14] R. Diaconescu and K. Futatsugi. Logical foundations of CafeOBJ. Theor. Comput. Sci.,
285(2):289–318, 2002.
[15] R. Diaconescu, J. Goguen, and P. Stefaneas. Logical support for modularisation. In
G. Huet and G. Plotkin, editors, Logical Environments, pages 83–130. Cambridge, 1993.
Proceedings of a Workshop held in Edinburgh, Scotland, May 1991.
[16] K. Futatsugi. Verifying specifications with proof scores in CafeOBJ. In ASE, pages
3–10. IEEE Computer Society, 2006.
[17] K. Futatsugi, J. A. Goguen, and K. Ogata. Verifying design with proof scores. In
B. Meyer and J. Woodcock, editors, VSTTE, volume 4171 of Lecture Notes in Computer
Science, pages 277–290. Springer, 2005.
[18] D. Găină, K. Futatsugi, and K. Ogata. Constructor-Based Logics. submitted.
[19] D. Găină, K. Futatsugi, and K. Ogata. Constructor-based institutions. In A. Kurz,
M. Lenisa, and A. Tarlecki, editors, CALCO, volume 5728 of Lecture Notes in Computer
Science, pages 398–412. Springer, 2009.
[20] J. A. Goguen and R. Burstall. Institutions: Abstract model theory for specification andprogramming. Journal of the Association for Computing Machinery, 39(1):95–146,
January 1992.
[21] J. A. Goguen and R. Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(3):363–392, 1994.

22

[22] J. A. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer
Science, 105(2):217–273, 1992.
[23] J. A. Goguen and G. Rosu. Institution morphisms. Formal Asp. Comput., 13(3-5):274–
307, 2002.
[24] L. Henkin. Completeness in the theory of types. J. Symb. Log., 15(2):81–91, 1950.
[25] S. Mac Lane. Categories for the Working Mathematician. Springer, second edition,
1998.
[26] K. Ogata and K. Futatsugi. Flaw and modification of the iKP electronic payment protocols. Inf. Process. Lett., 86(2):57–62, 2003.
[27] K. Ogata and K. Futatsugi. Simulation-based verification for invariant properties in the
OTS/CafeOBJ method. Electr. Notes Theor. Comput. Sci., 201:127–154, 2008.
[28] H. Reichel. Structural induction on partial algebras. Akademie-Verlag (Berlin), 1984.
[29] D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Inf. Comput.,76(2/3):165–210, 1988.
[30] L. Schröder, T. Mossakowski, A. Tarlecki, B. Klin, and P. Hoffman. Amalgamation in
the semantics of CASL. Theor. Comput. Sci., 331(1):215–247, 2005.
[31] A. Tarlecki. On the existence of free models in abstract algebraic institutions. Theor.
Comput. Sci., 37:269–304, 1985.
[32] A. Tarlecki. Bits and pieces of the theory of institutions. In D. Pitt, S. Abramsky,
A. Poigné, and D. Rydeheard, editors, Proceedings, Summer Workshop on Category
Theory and Computer Programming, Lecture Notes in Computer Science, volume 240,
pages 334–360. Springer, 1986.
[33] A. Tarlecki. Quasi-varieties in abstract algebraic institutions. J. Comput. Syst. Sci.,
33(3):333–360, 1986.

23