Nested Sketches

(Preliminary Version)

Horst Reichel^{∗} TU Dresden

1 Introduction

Since the fundamental work of Lawvere in 1963 [7] it is common to understand a theory as category with additional structure, to understand a model of the theory as a functor preserving the additional structure, and to represent homomorphisms by natural transformations. The resulting model category becomes a suitable subcategory of a functor category. Many different classes of mathematical structures have been described and investigated in this way. The aim of this paper is, to find a functorial model theory for those classes of algebras that appear naturally as semantics of algebraic specifications of parameterized data types, using initial respectively more general free functor semantics, and to extend the functorial model theory to specifications that use as well inductively defined data types as coinductively defined patterns of behavior and their systematic combinations.

The final result is a categorical model theory of discrete mathematical structures whose basic operations may have arbitrarily structured domains and codomains. Such kind of structures have been first systematically investigated by T. Hagino in his PhD thesis , [5]. The basic idea to achieve this generalized categorical model theory is the use of combined left and right Kan extensions in order to constrain iteratively functor categories.

The resulting categorical model theory generalizes algebraic and essentially algebric theories, since algebras are structures whose basic operations have a structured domain, being a product or finite limit, and the codoamin is one of the basic types (usually called sorts in algebra). The approache also generalizes coalgebras, for which dually the codomains of the basic operations are structured and the domain is one of the basic types.

As we will the, we are also able to represent model categories that have not jet been described by different kinds of sketches. To justify the last statement we consider the description of lists and trees as described in the electronic supplement of Barr and Wells book [2].

∗This work has been partially supported by EPSRC grant GR/M36694

In the Section 1.1.2 The sketch for lists there is used a finite discrete sketch with objects L, D, L^{+}, 1 and morphisms head : L^{+} → D, tail : L^{+} → L an two other unnamed ones that are used to express by a sum sketch that L^{+} = 1+L^{+}. Additional product sketches imply that 1 has to be mapped by a model M to a final object of a category, i.e., to a singleton set in the category of sets, and that for a model M(L^{+}) = M(D) × M(L) holds.

It is easy to check that the intended interpretation:

M(L) = set of all finite lists of elements in M(D)

with M(L^{+}) = set of all finite nonempty lists in M(D) is a model.

But the intended interpretation is not the only model. The discrete sketch does only imply that for each model M the set M(L) is a fixed point (up to isomorphism) of the recursive type equation

M(L) ≡ 1 + (M(D) × M(L).

The intended interpretation is given by the least fixed point, and there are several other ones not isomorphic to the intended model. Thus, the used formalization by discrete sketches is not able to constrain the functor category to the intended class of models.

In the next section be will introduce the notion of nested sketches and we will show, that this kind of constraining functor categories can represent exactly the intended class of functors, such that up to isomorphisms, a functor

M : ℂ → Set

is a model of a corresponding set of nested sketches, if and only if M(L) = M(D)^{∗}, where M(D)^{∗} denotes the set of finite list with elements in M(D).

2 Nested Sketches

In the following we assume that ℂ denotes a finitely generated category, represented by a finite directed graph G(ℂ) and a finite set Rel(ℂ) of defining relations, where a defining relation ⟨w_{1}, w_{2}⟩ ∈ Rel(ℂ) is an ordered pair of finite paths over G(ℂ) with the same beginning and end node.

If F : 𝔸 → 𝔹 and G : 𝔹 → ℂ are functors, there composition will be denoted by F; K : 𝔸 → ℂ.

Definition 2.1. A projective sketch (respectively injective sketch) in a category ℂ is given by three functors

J : ℂ_{0} → ℂ_{1}, K : ℂ_{1} → ℂ, F : ℂ_{0} → ℂ

and a natural transformation

π : J; K ⇒ F

respectively by a natural transformation

η : F ⇒ J; K.

A functor M : ℂ → Sem is a model of a projective sketch if

(K; M : ℂ_{1} → Sem, (π; M) : J; K; M ⇒ F; M)

is a right Kan extension of F; M : ℂ_{0} → Sem along J : ℂ_{0} → ℂ_{1}.

Correspondingly M : ℂ → Sem is a model of an injective sketch if

(K; M : ℂ_{1} → Sem, (η; M) : F; M ⇒ J; K; M)

is a left Kan extension of of F; M : ℂ_{0} → Sem along J : ℂ_{0} → ℂ_{1}.

A sketch in ℂ is either an injective or a projective sketch in ℂ. A functor M : ℂ → Sem is a model of a finite set of sketches if it is a model of each of sketch in the given set. □

Sketches as defined here do not improve the expressiveness with respect to the kind of sketches used by Barr and Wells [2]. They have been considered by Ross Street in the 60th, according to a personal communication, but have not been published. One advantage of the introduced sketches is the possibility to represent countable limit and colimit sketches in a finite manner. This can be illustrated by a specification of natural numbers.

Example 1: We take the category ℂ which is defined by the generating graph G(ℂ)

\xymatrix{B \ar[r]^{z} & N \ar[r]^{s} & N}

and with the empty set of defining relations. We take ℂ_{0} = 1, i.e., the category with exactly one object 1, ℂ_{1} = ℂ, K = Id_{ℂ}, J(1) = B, F (1) = B and the natural transformation η : F ⇒ J; K is the identity of F (= J; K). This defines an injective sketch in ℂ.

One can easily check that a functor M : ℂ → Set is a model of that injective sketch, if (up to isomorphisms)

M(N) = IN × M(B) = ∑_{i∈IN} M(B)_{i}

Proving that one has to show that for each functor X : ℂ_{1} → Set and each natural transformation α : F ⇒ J; X there is exactly one natural transformation α^{∗} : K; M ⇒ X with α = (η; M)∘(J; α^{∗}). This natural transformation is defined by α_{B}^{∗} = α_{B} and the component

α_{N}^{∗} : IN × M(B) → X(N)

is given by

\begin{aligned}α_{N}^{∗}(0, x) & = & (X(z))(α_{B}(x)) \\ α_{N}^{∗}(i + 1, x) & = & X(s)^{i+1}((X(z))(α_{B}(x))) \end{aligned}

If one wants to specify exactly the natural numbers (up to isomorphisms), one has to add a product sketch which forces a model to map the object B to the terminal object in the category of sets. □

However, trying to extend this idea to a specification of finite lists will fail.

Example 2: For the example of the parametric data type of finite lists we take a category ℂ^{2} with obj(ℂ^{2}) = {B, C, L, P } and with the following generating morphisms

\begin{matrix}nil : B → L \\ cons : P → L \\ p_{1} : P → C \\ p_{2} : P → L \end{matrix}

which constitute the generating graph G(ℂ^{2}). Also in that case the set of defining relations is empty.

Beside two product sketches, where one forces a model to map B to the terminal object and the other to map the object p to the product of the images of L and C, one takes an injective sketch defined as follows. ℂ_{1} = ℂ^{2}, ℂ_{0} = 1 + 1 having exactly the two objects 1 and 2. K = Id_{ℂ}, F (1) = B = J(1), F (2) = C = J(2) and η : F ⇒ J; K is the identity again.

But, now a functor M : ℂ^{2} → Set is a model of that injective sketch, if M(L) = M(P) = ∅. □

Why does the conjunction of that injective sketch with the two product sketches do not work as expected? That’s because the intended interpretation M : ℂ^{2} → Set with M(L) = M(C)^{∗} does not have the required universal property of a left Kan extension within the whole functor category Set^{ℂ^{2}}, but only within the subcategory of those functors being a model of the two product sketches.

How one can relate the universal property of a Kan extension to a subcategory of the functor category? This possibility will be achieved by the notion of nested sketches in a category ℂ defined as follows.

Definition 2.2 1. For each category ℂ there is a trivial nested sketch denoted by ⊤(ℂ).

2. Any finite set of nested sketches in an category ℂ is again a nested sketch

in ℂ, written

Δ = {Δ_{1}, …, Δ_{n}}

3. Let be

(J : ℂ_{0} → ℂ_{1}, F : ℂ_{0} → ℂ, K : ℂ_{1} → ℂ, η : F ⇒ J; K)

be an injective sketch in ℂ, let Δ_{1} be a nested sketch in ℂ_{1}, and Δ_{0} a nested sketch in ℂ_{0}. Then

Δ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, η : F ⇒ J; K⟩

is a nested sketch in ℂ.

4. Let be

(J : ℂ_{0} → ℂ_{1}, F : ℂ_{0} → ℂ, K : ℂ_{1} → ℂ, π : J; K ⇒ F)

be a projective sketch in ℂ, let Δ_{1} be a nested sketch in ℂ_{1}, and Δ_{0} a nested sketch in ℂ_{0}. Then

Δ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, π : J; K ⇒ F ⟩

is a nested sketch in ℂ.

In the following we define under which conditions a functor M : ℂ → Sem is a model of a nested sketch in ℂ:

1. Each functor M : ℂ → Sem is a model of the trivial nested sketch ⊤(ℂ).

2. M : ℂ → Sem is a model of Δ = {Δ_{1}, …, Δ_{n}} if it is a model for each Δ_{i}, i = 1, …, n.

3. M : ℂ → Sem is a model of

Δ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, η : F ⇒ J; K⟩

if

(a) K; M : ℂ_{1} → Sem is a model of Δ_{1}.

(b) F; M : ℂ_{0} → Sem is a model of Δ_{0}.

(c) For each functor X : ℂ_{1} → Sem such that X is a model of Δ_{1} and J; X is a model of Δ_{0}, and for each natural transformation α : F ⇒ J; X there is exactly one natural transformation α^{∗} : K; M ⇒ X with α = (η; M) ∘ (J; α^{∗}).

4. M : ℂ → Sem is a model of

Δ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, π : J; K ⇒ F ⟩

if

(a) K; M : ℂ_{1} → Sem is a model of Δ_{1}.

(b) F; M : ℂ_{0} → Sem is a model of Δ_{0}.

(c) For each functor X : ℂ_{1} → Sem such that X is a model of Δ_{1} and J; X is a model of Δ_{0}, and for each natural transformation α : J; X ⇒ F there is exactly one natural transformation α^{∗} : X ⇒ K; M with α = (J; α^{∗}) ∘ (π; M).

A pair (ℂ, Δ) consisting of a finitely generated category and a nested sketch in ℂ will be called a theory of nested sketches NS-theory for short. □

Using the trivial nested sketch for Δ_{1} and Δ_{0} in definitions (3) and (4) one gets the injective and projective sketches as special cases of nested sketches. Therefore we will in the following no more distinguish between nested and flat sketches, and will uniquely use the more general notion of nested sketches.

With this more general notion we are now able to specify the parametric data type of finite lists.

Example 3: We take the injective sketch of Example 2 and build a nested sketch according part (3) of the preceding definition, by taking Δ_{1} to consists of the two product sketches (seen as nested sketches in ℂ_{1}), and taking for Δ_{0} the trivial nested sketch ⊤(ℂ_{0}).

Let Δ_{tree} denote the resulting nested sketch in ℂ. Now the class of models M : ℂ → Set of Δ_{tree} coincides with those interpretation where M(B) is a singleton set {∗}, M(C) can be an arbitrary set, M(L) = M(C)^{∗} is the set of all finite list with elements in M(C), and M(P) = M(C)×M(L). M(p_{1}), M(p_{2}) are the projections, M(nil) : {∗} → M(L) maps ∗ to the empty list and M(cons) : M(C)×M(L) → M(L) maps an element x_{0} ∈ M(C) and a list l = [x_{1}, …, x_{n}] ∈ M(L) to the list [x_{0}, x_{1}, …, x_{n}]. □

What about the existence of models? Can an NS-theory be unsatisfiable? This general questions can easily be answered, since for any NS-theory (ℂ, Δ) the unique functor !_{ℂ} : ℂ → 1 is a model. Evidently the category 1 is not an interesting domain to construct models. The interesting question is, if in a specific category like Set models exist. In general the answer is no. To see that we take ℂ = 1 and let Δ consists of two discrete sketches which force a model M : ℂ → Sem to map the unique object as well to the initial as to the terminal object of Sem. Since in Set the initial object is not terminal and vice versa, there is no model in Set for that NS-theory. But, this NS-theory has for instance a model in the category of commutative groups.

Another interesting question concerns the existence of generic models, where a model M_{Δ} : ℂ → 𝕃_{Δ} of an NS-theory (ℂ, Δ) is called generic, if for each model M : ℂ → Sem of (ℂ, Δ) there is a unique functor M′ : 𝕃 → Sem with M = M_{Δ}; M′.

Theorem 2.3 For each NS-theory (ℂ, Δ) there exists (up to isomorphisms) a unique generic model M : ℂ → 𝕃.

Proof: From the definition of generic models immediately follows that a generic model, if it exists, is unique up to isomorphisms.

So it remains to show that there is a generic model. This will be proved by induction on the depth of nested sketches, which will be defined next.

According to the inductive definition of nested sketches, the depth i(Δ) of a nested sketch can be defined as follows:

i(⊤(ℂ))  = 0
i({Δ_{1}, …, Δ_{n}})  = max{i(Δ_{1}), …, i(Δ_{n})}
i(⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, π : J; K ⇒ F ⟩) = 1 + max{i(Δ_{1}), i(Δ_{0})}
i(⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, η : F ⇒ J; K⟩) = 1 + max{i(Δ_{1}), i(Δ_{0})}

Let be Δ a nested sketch in ℂ and H : ℂ → ℂ′ any functor. Then we can define the nested sketch

Δ; H in ℂ′ (∗)

by using the inductive nature of nested sketches. First we set ⊤_{ℂ}; H = ⟨(⊤_{ℂ}, ℂ), (⊤_{ℂ}, ℂ), Id_{ℂ}, H, H, Id_{H} : H ⇒ H⟩ which can be seen as well as an instance of a nested sketch according (3) as well of (4) in Definition 2.2. The nested sketch ⊤_{ℂ}; H is semantically equivalent to ⊤_{ℂ′} since each functor G : ℂ′ → ℂ′′ is a model of ⊤_{ℂ}; H. Next we set Δ; H = {Δ_{1}; H, …, Δ_{n}; H} if Δ = {Δ_{1}, …, Δ_{n}}, and Δ; H = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F; H, K; H, η; H : F; H ⇒ J; (K; H)⟩ if Δ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, η : F ⇒ J; K⟩, and finally Δ; H = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F; H, K; H, π; H : J; (K; H) ⇒ F; H⟩ if Δ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, π : J; K ⇒ F ⟩.

Equipped with this notions we can start the inductive construction of a generic model.

The starting point is trivial, since for a nested sketch with Δ in ℂ with i(Δ) = 0 the identity of ℂ is a generic model.

Now we assume, that for any nested sketch Δ with i(Δ) ≤ n+1 a generic model is given by M_{Δ} : ℂ → 𝕃_{Δ}.

Let Δ′ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, η : F ⇒ J; K⟩ be a nested sketch with i(Δ′) = n + 1 which implies max{i(Δ)_{0}), i(Δ)_{1})} = n.

Let be Δ = {Δ_{1}; K, Δ_{0}; F }. Then i(Δ) = n and the induction hypothesis can be applied to Δ.

The generic model M_{Δ′} : ℂ → 𝕃_{Δ′} will be constructed as injective limit of a chain

Q_{i} : 𝕃_{i} → 𝕃_{i+1}, i = 0, 1, …

with 𝕃_{0} = 𝕃_{Δ}, and each 𝕃_{i} will be given by a directed graph G(𝕃_{i}), representing the generating morphisms, and by a congruence relation ρ_{i} in the category freely generated by G(𝕃_{i}), i.e., in the category of finite paths over G(𝕃_{i}). The chain of pairs ⟨G(𝕃_{i}), ρ_{i}⟩ will be inductively defined, and it will turn out that it is an increasing chain, so that the the injective limit will be given by the infinite unions, separately constructed in each component.

The construction of the chain starts with the pair ⟨G(𝕃_{0}), ρ_{0}⟩ with results from the induction hypothesis. Now let be given ⟨G(𝕃_{i}), ρ_{i}⟩.

Let H_{i} : ℂ → 𝕃_{i} be the composition H_{i} = M_{Δ}; Q_{0}; … O_{i−1}.

For each pair (X, α), where X : ℂ_{1} → 𝕃_{i} is a functor such that it is a model of Δ_{1} and J; X is a model of Δ_{0}, and α : F; H_{i} ⇒ J; X is a natural transformation, such that no natural transformation α^{∗} : K; H_{i} ⇒ X with α = (η; H_{i}) ∘ (J; α^{∗}), for each such pair (X, α) we add the set of generating morphisms

{f_{(X,α,c)} : H_{i}(K(c) → X(c) | c ∈ obj(ℂ_{1})}

to the generating graph G(𝕃_{i}), which leads to the generating graph G(𝕃_{i+1}). The congruence relation ρ_{i+1} is the smallest congruence relation in the category freely generated by G(𝕃_{i+1}) such that ρ_{i} ⊆ ρ_{i+1} and such that for each (X, α) used in the construction of G(𝕃_{i+1}) the family α^{∗} = {f_{(X,α,c)} : H_{i}(K(c) → X(c) | c ∈ obj(ℂ_{1})} becomes the unique natural transformation α^{∗} : K; H_{i} ⇒ X satisfying α = (η; H_{i}) ∘ (J; α^{∗}). The association f ↦ [f]_{ρ_{i+1}} defines the functor Q_{i} : 𝕃_{i} → 𝕃_{i+1}.

Let be G(𝕃_{Δ′}) be the injective limit of the increasing chain of generating graphs G(𝕃_{i}), i = 0, 1, …, and let ρ_{Δ′} be the smallest congruence relation in the category freely generated by G(𝕃_{Δ′}). This two constructions give us a representation of the category 𝕃_{Δ′}, being the injective limit of the chain Q_{i} : 𝕃_{i} → 𝕃_{i+1}, i = 0, 1, . . ..

Let M_{0} : 𝕃_{0} → 𝕃_{Δ′} the injection into the injective limit, and let M_{Δ′} : ℂ → 𝕃_{Δ′} be the composition of M_{Δ} with M_{0}. The proceeding construction makes it evident that M_{Δ′} : ℂ → 𝕃_{Δ′} is a model of Δ′.

It remains to show that this model is a generic mode of Δ′.

For that reason let M : ℂ → Sem be an arbitrary model of Δ′. By definition is K; M a model of Δ_{1} and F; M a model of Δ_{0}, which implies that M is a model of both Δ_{1}; K and Δ_{0}; F, i.e. M is a model of Δ = {Delta_{1}, Δ_{0}; F }. By induction hypothesis is M_{Δ} : ℂ → 𝕃_{Δ} a generic model of Δ. This guarantees the existence of a unique functor M_{0} = 𝕃_{Δ} → Sem with M = M_{Δ}; M_{0}.

Inductively we will show that for each i ∈ IN there is a unique functor M_{i} : 𝕃_{i} → Sem with (Q_{0}; Q_{1}; …; Q_{i−1}); M_{i} = M_{0} which implies the existence of the required unique M′ : 𝕃_{Δ′} → Sem, since 𝕃_{Δ′} is the injective limit of that chain.

For i = 0 the existence of M_{0} : 𝕃_{Δ} → Sem has just been proved. Let M_{i} : 𝕃_{i} → Sem with the corresponding properties be given. For each pair (X, α), used to construct new generating morphisms in G(𝕃_{i+1}) we obtain a natural transformation α; M_{i} : F; H_{i}; M_{i} ⇒ J; X; M_{i}, i.e., α; M_{i} : F; M ⇒ J; X; M_{i}, because of H_{i}; M_{i} = M. Because M is a model of Δ′ there exists a unique natural transformation α^{∗} : K; M ⇒ X; M_{i} with α; M_{i} = (η; M) ∘ (J; α^{∗}). Mapping each new generating morphism f_{(X,α,c)} : H_{i}(K(c)) → X(c) in G(𝕃_{i+1}) to α^{∗}(c) : M(K(c)) → M_{i}(X(c)) defines together with M_{i} a graph homomorphisms from G(𝕃_{i+1}) to the underlying graph of the category Sem. The resulting unique graph homomorphism M′′_{g} : G(𝕃_{Δ′}) to the underlying graph of the category Sem induces finally a functor from the category freely generated by G(𝕃_{Δ′}) to Sem whose kernel contains each ρ_{i}. This implies the existence of the unique functor M^{∗} : 𝕃_{Δ′} → Sem with M = M_{Δ′}; M^{∗}.

The construction of a generic model of a nested sketch according point (4) of Definition 2.2 can be done analogously.

If Δ = {Δ_{1}, …, Δ_{n}} with i(Δ) = n + 1 and more than one of the Δ_{i}’s has depth n, then one has to consider all pairs (X, α) simultaneously for all Δ_{i}’s with depth n, in the inductive construction of the category 𝕃_{Δ′}. □

Next we point out a property of nested sketches and their models which basically guarantees that nested sketches built an institution in the sense of Goguen and Burstall [3].

Proposition 2.4. Let Δ be a nested sketch in ℂ and H : ℂ → 𝔹 any functor. A functor M : 𝔹 → Sem is a model of Δ; H if and only if H; M is a model of Δ.

Proof: The equivalence can be proved again by induction on the structure of nested sketches.

The case Δ = ⊤_{ℂ} is trivial, since each functor H : ℂ → 𝔻 is a model of ⊤_{ℂ}, and each functor H′ : ⊤_{𝔹} → ⊤_{𝔻} is a model of ⊤_{ℂ}; H.

With the induction hypothesis immediately follows that Proposition 2.4 holds if Δ = {Δ_{1}, …, Δ_{n}}.

A bit more interesting are the cases where the nested sketches are constructed according point (3) or (4) in definition 2.2.

Let Δ = ⟨(Δ_{1}, ℂ_{1}), (Δ_{0}, ℂ_{0}), J, F, K, π : J; K ⇒ F ⟩ and assume that M is a model of Δ; H.

To prove that H; M is a model of Δ we assume that there is a functor X : ℂ_{1} → Sem and a natural transformation α : F; (H; M) ⇒ J; X. By associativity of functor composition we have a natural transformation α : (F; H; )M ⇒ J; X, and since M is a model of Δ; H there is a unique natural transformation α^{∗} : (K; H); M ⇒ X with α = ((η; H); M) ∘ (J; α^{∗}). Using again associativity we obtain a unique natural transformation α^{∗} : K; (H; M) ⇒ X with α = (η; (H; M) ∘ (J; α^{∗}), which implies that H; M is a model of Δ.

The converse and the case that Δ is constructed according point (4) in Definition 2.2 can be proved identically. □

To get an institution of nested sketches in the sense of Goguen and Burstall one takes the category Cat_{f} of finitely generated categories as a category of signatures, one takes nested sketches in a category ℂ as sentences over the signature ℂ, and one takes for each functor H : ℂ → 𝔹 in Cat_{f} the mapping

Δ ⟼ Δ; H

as translation from sentences over ℂ to sentences over 𝔹. With respect to that construction Proposition 2.4 just states the validity of the satisfaction condition of the institution of nested sketches.

3 Examples of NS-theories and generic models

If a NS-theory only contains product sketches, the corresponding generic model corresponds to the term model, with the exception that only finitely many variables are given, since finitely many product sketches do not imply that the generic model is closed under finite products.

The term model considered as a category can be understood as a minimal logic for talking about structures whose domains of the basic operations are defined by products, i.e., for talking about many sorted algebras. The minimal logic, resulting from a Kan theory containing only product sketches, corresponds to equational logic.

In the following we will see that the minimal logic, given by the generic model of a NS-theory can be surprisingly expressive, depending on the constructions used to define domains and codomains of basic operations.

To get a better understanding for the range of expressiveness of NS-theories we consider as next theories which contain projective sketches.

Example 4: We take the category ℂ^{4}, given by the generating graph G(ℂ^{4}):

\xymatrix{B & S \ar[l]_{head} \ar[r]^{tail} & S}

and the empty set of defining relations. We take the categories and functors ℂ_{0}^{4} = 1, ℂ_{1}^{4} = ℂ^{4}, K = Id_{ℂ^{4}}, J(1) = B = F (1), and the natural transformation π : J; K ⇒ F is the identity of F (= J; K). With the notation of Definition 2.2 we consider the nested sketch (of depth one)

Δ^{4} = ⟨(⊤_{ℂ^{4}}, ℂ^{4}), (⊤_{1}, 1), J, F, K, π : F ⇒ J; K⟩

in ℂ^{4}.

A functor M : ℂ^{4} → Set is a model of Δ^{4} iff M(S) = M(B)^{IN}, with (M(h))(f) = f(0) and (M(t))(f) = λ x.f(x + 1) for each (f : IN → M(B)) ∈ M(S), i.e., the NS-theory (ℂ^{4}, Δ^{4}) specifies the parametric Type of infinite streams. □

Example 5: We extend the preceding example by taking the category ℂ^{5}, defined by the generating graph

\xymatrix{B & S \ar[l]_{head} \ar[r]^{tail} & S & S′ \ar[l]_{head′} \ar[r]^{tail′} & S′}

and the empty set of defining relations. Now we consider two nested sketches (both of depth one) given by the following projective sketches:

Δ_{1}^{5} : \xymatrix{ℂ_{1}^{1} \ar[r]^{K^{1}} & ℂ^{5} \\ 1 \ar[u]^{J^{1}} \ar[ur]_{F^{1}}} Δ_{2}^{5} : \xymatrix{ℂ_{1}^{2} = ℂ^{5} \ar[r]^{Id} & ℂ^{5} \\ ℂ_{0}^{2} = ℂ_{1}^{1} \ar[u]^{J^{2}} \ar[ur]_{F^{2}(=K^{1})}}

Where ℂ_{1}^{1} = ℂ_{1}^{2} = ℂ^{4}, F^{1}(1) = b = J^{1}(1) and K^{1}, J^{2} are the inclusion functors. Since both diagrams commute we can take for π_{1}, π_{2} the corresponding identities to define projective sketches.

A functor M : ℂ^{5} → Set is a model of the NS-theory (ℂ^{5}, {Δ_{1}^{5}, Δ_{2}^{5}}) iff M(S) = M(B)^{IN} and M(S′) = (M(B)^{IN})^{IN}. Thus, the object S′ represents the type of infinite streams of infinite streams with elements in M(B). This type is a simple example of a higher order process type, since the outputs of a process are again processes which themselves output elements of base type B. □

In the following we generalize the Example 4 in such a way that we allow the processes to terminate after an arbitrary finite number of steps. The specification of this kind of processes requires a nested sketch of depth two.

Example 6: We take the category ℂ^{6} given by the defining graph

\xymatrix{B & S \ar[l]_{head} \ar[r]^{tail} \ar[r]_{inl} & S + T & T \ar[l]_{inr}}

and the empty set of defining relations. The nested sketch Δ^{6} is depicted by

Δ^{6} : \xymatrix{Δ_{1}^{6} : ℂ^{6} \ar[r]^{Id} & ℂ^{6} \\ ⊤_{1} : 1 \ar[u]^{J} \ar[ur]_{F}}

the natural transformation π : J; Id ⇒ F (= id_{F}), where J(1) = B = F (1) and where Δ_{1}^{6} consists of one product sketch, constraining the object T to the terminal object, and one sum sketch, making the object S + T to the sum of S and T with the two injections inl : S → S + T, inr : T → S + T. □

Similarly to the specification of the parametric data type of finite lists one has to nest sketches in Example 6, since for each fixed interpretation M(B) of the sort B one has to characterize the set M(S) of finite and infinite sequences of elements in M(B) as a final coalgebra, or equivalently as a most abstract, deterministic, partial automata with a singleton set as input alphabet, the set M(B) as output alphabet and M(S) as state set, where M(tail) : M(S) → M(S) + {∗} represents the state transition function.

The preceding examples have shown that nested sketches with an injective top sketch are strongly related to inductively defined data types, and that nested sketches with a projective top sketch are related to coinductively defined process types. More advanced examples can be found in the literature on algebraic specifications of data types and on coalgebraic approaches to systems. We will not go further in that direction.

In the following we will investigate in which way induction and coinduction is present in the corresponding generic models. i.e., if induction and coinduction is present in the canonically related term model of the structures specified by an NS-theory.

Let as first look if induction is available in a generic model of an NS-theory with injective sketches. For that reason we consider first the following preparative example.

Example 7: ℂ^{7} is the category given by the defining graph

\xymatrix{T \ar[r]^{T inl} \ar[r]_{T inr} & T + T & (T + T) × B \ar[l]_{p 1} \ar[r]^{p 2} & B \ar[r]^{B inl} \ar[r]_{B inr} & B + B}

and the empty set of defining relations. We are interested in the generic model of the NS-theory

(ℂ^{7}, Δ^{7} = {Δ_{1}^{7}, Δ_{2}^{7}, Δ_{3}^{7}, Δ_{4}^{7}})

where Δ_{1}^{7} constrains the object T + T to the sum of T and T with the two injections T inl : T → T + T, T inr : T → T + T, where Δ_{2}^{7} analogously constrains the object B + B to become the twofold sum of B with the injections B inl : B → B + B, B inr : B → B + B, Δ_{3}^{7} constrains the object T to the terminal object, and Δ_{4}^{7} finally constrains the object (T +T)×B to become the product of T + T and B with the projections p 1 : (T + T) × B → T + T, p 2 : (T + T) × B → B.

In the generic model 𝕃_{Δ^{7}} the projective sketch Δ_{3}^{7} generates for each object X a unique morphism !_{X} : X → T with !_{T} = id_{T} and the two sum sketches generate morphisms cd_{T} : T + T → T, cd_{B} : B + B → B with T inl; cd_{T} = id_{T} = T inr; cd_{T} and B inl; cd_{B} = id_{B} = B inr; cd_{B} . Whoever constructing the congruence ρ_{1} according the proof of Theorem 2.2, the two generated morphisms cd_{T} and !_{T +T} will be identified. In the next generation step the two morphisms !_{B}; T inl,!_{B}; T inr : B → B + B generate the morphism !_{B}+!_{b}B : B + B → T + T. This morphism together with the morphism cd_{B} : B + B → B cause the product sketch Δ_{4}^{7} to generate a morphism

⟨!_{B}+!_{B}, cd_{B}⟩ : B + B → (T + T) × B

with corresponding equations. We have pointed out that morphism, because each model M : ℂ^{7} → Set of Δ^{7} interprets that morphism as a bijection, i.e. as an isomorphism in Set, since the disjoint sum of a set M(B) with itself can be constructed by a product {1, 2} × M(B). As it is well known, this relation between products and sums does not hold in each category and so also not in the generic model. □

We have developed this simple example so carefully, since induction is usually expressed as parametric induction, i.e., induction applied to a component of a Cartesian product. Primitive recursion is a typical induction scheme of that kind. This kind of induction cannot be present in generic models in general. In which way the induction is present in generic models will be illustrated, by defining the operation of adding two natural numbers.

Example 8: If we want to specify the addition of natural numbers as a morphism in the generic model, then there has to be an object representing the domain of that operation. The argumentation above makes clear that a product would not work. Coming back to Example 1 we see that a functor M : ℂ → Set is a model of the injective sketch introduced there if

M(N) = IN × M(B) = ∑_{i∈IN} M(B)_{i}

If one takes M(B) = IN then we obtain IN × IN = ∑_{i∈IN} IN_{i}. This instantiation of the parameter can be achieved by the following NS-theory (ℂ^{8}, Δ^{8} = {Δ_{1}^{8}, Δ_{2}^{8}, Δ_{3}^{8}}), where ℂ^{8} is given by the generating graph

\xymatrix{T \ar[r]^{z_{1}} & N_{1} & N_{1} \ar[l]_{s_{1}} \ar[r]^{z_{2}} & N_{2} & N_{2} \ar[l]_{s_{2}}}

and the empty set of generating relations. Δ_{1}^{8} constrains the object T to the terminal object, and the two injective sketches Δ_{2}^{8}, Δ_{3}^{8} of depth one are given by the diagrams

Δ_{2}^{8} : \xymatrix{ℂ_{1}^{1} \ar[r]^{K^{1}} & ℂ^{8} \\ 1 \ar[u]^{J^{1}} \ar[ur]_{F^{1}}} Δ_{3}^{8} : \xymatrix{ℂ_{1}^{2} = ℂ_{1}^{1} \ar[r]^{K^{2}} & ℂ^{8} \\ 1 \ar[u]^{J^{2}} \ar[ur]_{F^{2}}}

Where ℂ_{1}^{2} = ℂ_{1}^{1} is the category given by the defining morphisms

\xymatrix{T \ar[r]^{z} & N & N \ar[l]_{s}}

and the empty set of defining relations. The corresponding functors are defined by J^{1}(1) = T = F^{1}(1), J^{2}(1) = T, F^{2}(1) = N_{1}, K^{1}(z) = z_{1}, K^{2}(z) = z_{2}, K^{1}(s) = s_{1} and K^{2}(s) = s_{2}. The corresponding natural transformations η_{2}^{8} : F^{1} ⇒ J^{1}; K^{1} and η_{3}^{8} : F^{2} ⇒ J^{2}; K^{2} are the identities.

Pairs of natural numbers (n, m) ∈ IN × IN can be represented by morphisms

z_{1}; \underbrace{s_{1}; …; s_{1}}_{n−times}; z_{2}; \underbrace{s_{2}; …; s_{2}}_{m−times} : T → N_{2}.

The sketch Δ_{1}^{8} generates for each object X uniquely morphisms !_{X} : X → T.

In the next step we construct morphisms p_{1}, p_{2} : N_{2} → N_{1} in the generic model which satisfy

\begin{aligned}z_{1}; \underbrace{s_{1}; …; s_{1}}_{n−times}; z_{2}; \underbrace{s_{2}; …; s_{2}}_{m−times}; p_{1} & = & z_{1}; \underbrace{s_{1}; …; s_{1}}_{n−times} \\ z_{1}; \underbrace{s_{1}; …; s_{1}}_{n−times}; z_{2}; \underbrace{s_{2}; …; s_{2}}_{m−times}; p_{2} & = & z_{1}; \underbrace{s_{1}; …; s_{1}}_{m−times} \end{aligned}

and represent projections (not satisfying universal properties).

One can easily check that the two equations would hold if the two morphisms p_{1}, p_{2} would satisfy the following equations:

\begin{aligned}z_{2}; p_{1} & = & !_{N_{1}}; z_{1} \\ s_{2}; p_{1} & = & p_{1}; s_{1} \end{aligned}  \begin{aligned}z_{2}; p_{2} & = & id_{N_{1}} \\ s_{2}; p_{2} & = & p_{2} \end{aligned}

These two projections can be constructed as

p_{1} = f_{(H_{p_{1}} ,id,N_{2})}, p_{2} = f_{(H_{p_{2}} ,id,N_{2})}

where the functors H_{p_{i}} : ℂ_{1}^{2} → ℂ^{8} for i = 1, 2 are defined by H_{p_{1}}(z) = z_{1}, H_{p_{1}}(s) = s_{1} and H_{p_{2}}(z) = id_{N_{1}}, H_{p_{2}}(s) = id_{N_{1}}.

Even though one can define the two projections, they do not have the universal property necessary for a product. However, for each model M : ℂ^{8} → Set of (ℂ^{8}, Δ^{8}) the mapping M((p_{1}, p_{2})) : M(N_{2}) → M(N_{1}) × M(N_{1}) is a bijection. This is one consequence of distributivity properties of the category of sets with respect to injective and projective limits.

Finally the morphism

add = f_{(H_{+},id,N_{2})} : N_{2} → N_{1}

using the functor H_{+} : ℂ_{1}^{2} → ℂ^{8} defined by H_{+}(z) = id_{N_{1}}, H_{+}(s) = s_{1} defines the addition of natural numbers. The corresponding equations represent with the notation of pairs of natural numbers the following recursive definition:

\begin{aligned}add(n, 0) & = & n \\ add(n, m + 1) & = & add(n, m) + 1 \end{aligned}

This is not the only way to construct in the generic model a morphism representing the addition. □

This example does not only illustrate the expressive power of generic models, it shows in addition that the iterative construction of the generic model does not necessarily converge after finitely many steps, because for the given NS-theory the schema of primitive recursion can always be applied to that operation, that has been generated in the step before and delivers a new operation. Thus in the second step we would generate a morphism representing the multiplication, in the following a morphism representing the exponentiation and so on.

By the next example we illustrate that generic models also reflect coinduction.

Example 9: Let ℂ^{9} be the category that results from ℂ^{4} by adding a new object, denoted by s × s and two new generating morphisms p_{1}, p_{2} : s × s → s. If Δ^{4} denotes the projective sketch in ℂ^{4} as defined in Example 4, and if I : ℂ^{4} → ℂ^{9} denotes the inclusion, then let

(ℂ^{9}, Δ^{9} = {Δ^{4}; I, Δ_{s×s}^{4}})

denote the NS-theory, where Δ_{s×s}^{4} denotes a product sketch which makes the object s×s to the product with the projections p_{1}, p_{2} : s×s → s. In the generic model the product sketch generates a morphism

⟨p_{2}, (p_{1}; tail)⟩ : s × s → s × s

satisfying the equations ⟨p_{2}, (p_{1}; tail)⟩; p_{1} = p_{1} and ⟨p_{2}, (p_{1}; tail)⟩; p_{2} = p_{1}; tail. By means of that morphism we can define a functor H : ℂ_{1}^{1} → ℂ^{9} by H(head) = p_{1}; head and H(tail) = ⟨p_{2}, (p_{1}; tail)⟩. If α : J; I ⇒ F; I denotes the identity transformation, so that in the next generation step a morphism

f_{(H,α,s×s)} : s × s → s

is generated which satisfies the equations

\begin{aligned}f_{(H,α,s×s)}; head & = & p_{1}; head \\ f_{(H,α,s×s)}; tail & = & ⟨p_{2}, (p_{1}; tail)⟩; f_{(H,α,s×s)} \end{aligned}

One can easily recognize the coinductive definition of the merge operation. □.

The examples show that in the generic models both induction and coinduction are present in a very natural and explicit way.

The next example represents the parameterized data type of the finitary power set construction.

Example 10: Let ℂ^{10} be the category with the object set {t, b, p, b×p, b×b×p}, with the defining morphism empty : t → p, add : b × p → p, p_{1}^{2} : b × p → b, p_{2}^{2} : b × p → p, p_{1}^{3} : b × b × p → b, p_{2}^{3} : b × b × p → b, p_{3}^{3} : b × b × p → p, d : b × p → b × b × p, ⟨p_{1}^{3}, p_{3}^{3}⟩ : b × b × p → b × p, ⟨p_{2}^{3}, p_{3}^{3}⟩ : b × b × p → b × p, ⟨p_{1}^{3}, ⟨p_{2}^{3}, p_{3}^{3}⟩; add⟩ : b × b × p → b × p, ⟨p_{2}^{3}, ⟨p_{1}^{3}, p_{3}^{3}⟩; add⟩ : b × b × p → b × p

and with the defining relations

d; p_{1}^{3} = d; p_{2}^{3} = p_{1}^{2}, d; p_{3}^{3} = p_{2}^{2}, ⟨p_{1}^{3}, p_{3}^{3}⟩; p_{1}^{2} = p_{1}^{3}, ⟨p_{1}^{3}, p_{3}^{3}⟩; p_{2}^{2} = p_{3}^{3}, … ⟨p_{2}^{3}, ⟨p_{1}^{3}, p_{3}^{3}⟩; add⟩; p_{1}^{2} = p_{2}^{3}, ⟨p_{2}^{3}, ⟨p_{1}^{3}, p_{3}^{3}⟩; add⟩; p_{2}^{2} = ⟨p_{1}^{3}, p_{3}^{3}⟩; add, d; ⟨p_{1}^{3}, ⟨p_{2}^{3}, p_{3}^{3}⟩; add⟩; add = add, ⟨p_{1}^{3}, ⟨p_{2}^{3}, p_{3}^{3}⟩; add⟩; add = ⟨p_{2}^{3}, ⟨p_{1}^{3}, p_{3}^{3}⟩; add⟩; add.

The last two equations express the idempocy and commutativity of adding an element to a finite set of elements. The other morphisms and equations represent manipulations with variables, which are not present explicitly.

Let Δ_{t}, Δ_{b×p}, Δ_{b×b×p} be product sketches in ℂ^{10} that constraint the object t to the terminal one and the others to the indicated products and Δ = {Δ_{t}, Δ_{b×p}, Δ_{b×b×p}}. Finally we define a nested Kan sketch Δ^{10} in ℂ^{10}

\xymatrix{Δ : ℂ^{10} \ar[r]^{Id} & ℂ^{10} \\ 1 \ar[u]^{J} \ar[ur]_{F}}

with J(1) = F (1) = b, where the natural transformation η^{10} : F ⇒ J; (Id_{ℂ^{10}}) is once more the identity.

A functor M : ℂ^{10} → Set is a model of the Kan theory (ℂ^{10}, Δ^{10}) if M(p) is the set of all finite subsets of M(b). □

Example 10 demonstrates in addition to the preceding examples the use of defining equations for the constraint category.

But, the example also demonstrates that the notation used so far is not convenient for more complex examples. One needs some more readable textual representations and possibilities to built up complex NS-theories from smaller ones, defined before.

4 Structuring NS-theories

In the examples above most sketches have been commutative triangles, so that the corresponding natural transformation is the identity. In addition the functor J : ℂ_{0} → ℂ_{1} has been the embedding of a subcategory. In the following we will show that natural transformations as parts of nested sketches ar not explicitly needed and that a restriction to this kind of sketches does not restrict the expressiveness of sketches.

Definition 4.1. An injective (respectively projective) sketch

(J : ℂ_{0} → ℂ_{1}, F : ℂ_{0} → ℂ, K : ℂ_{1} → ℂ, η : F ⇒ J; K)

is called a commutative triangle sketch, ct-sketch for short, if J : ℂ_{0} → ℂ_{1} is the embedding of a subcategory, if J; K = F and if η = id_{F} respectively π : J; K ⇒ F = id_{F}. A nested sketch is called a nested ct-sketch if all included sketches are ct-sketches or if it is the trivial nested sketch. □

Theorem 4.2. For each nested sketch Δ in a category ℂ there exists a semantically equivalent nested ct-sketch.

Proof: We consider first nested sketches of depth one.

Let

Δ (J : ℂ_{0} → ℂ_{1}, F : ℂ_{0} → ℂ, K : ℂ_{1} → ℂ, η : F ⇒ J; K)

be an injective sketch in ℂ. This sketch can equivalently be replaced by the following injective ct-sketch

Δ^{∗} (J^{∗} : ℂ_{0} → ℂ_{1}^{∗}, F : ℂ_{0} → ℂ, K^{∗} : ℂ_{1}^{∗} → ℂ, id_{F} : F ⇒ J^{∗}; K^{∗}(= F))

where J^{∗}; K^{∗} = F and J^{∗} : ℂ_{0} → ℂ_{1}^{∗} is the embedding of a subcategory.

The category ℂ_{1}^{∗} can be constructed form J : ℂ_{0} → ℂ_{1} as follows:

Take the sum ℂ_{0} + ℂ_{1}, then adjoin for each object X ∈ obj(ℂ_{0}) a morphism h_{X} : X → J(X) and adjoin an equation f; h_{Y} = h_{X}; J(f) for each morphism f : X → Y in ℂ_{0} to the union of the defining relations of ℂ_{0} and ℂ_{1}. Let J^{∗} : ℂ_{0} → ℂ_{1}^{∗} denote the embedding of ℂ_{0} into ℂ_{1}^{∗}

Let J_{1}^{∗} : ℂ_{1} → ℂ_{1}^{∗} be the embedding of ℂ_{1} and η^{∗} : J^{∗} ⇒ J; J_{1}^{∗} be the natural transformation with η_{X}^{∗} = h_{X} for each object X ∈ ℂ_{0}

The resulting pair (ℂ_{1}^{∗}, η^{∗}) has the following universal property: For each pair of functors F : ℂ_{0} → ℂ, K : ℂ_{1} → ℂ and each natural transformation η : F ⇒ J; K there exists a unique functor K^{∗} : ℂ_{1}^{∗} → ℂ with J^{∗}; K^{∗} = F and η = η^{∗}; K^{∗}.

It remains to prove that the two injective sketches Δ, Δ^{∗} are semantically equivalent.

First let M : ℂ → Sem be any model of Δ. To prove that this model is aslo a model of Δ^{∗} let H : ℂ_{1}^{∗} → Sem by any functor and α : F; M ⇒ J_{0}^{∗}; H be any natural transformation.

Then η^{∗}; H : J_{0}^{∗} ⇒ J; (J_{1}^{∗}; H) and since M : ℂ → Sem is a model of Δ for the functor J_{1}^{∗}; H : ℂ_{1} → Sem and the natural transformation α ∘(η^{∗}; H) : F; M ⇒ J; (J_{1}^{∗}; H) there exists exactly one natural transformation α^{∗} : K; M ⇒ J_{1}^{∗}; H satisfying

(∗) α ∘ (η^{∗}; H) = (η; M) ∘ (J_{1}^{∗}; α^{∗})

In the next step we lift the two natural transformations

\begin{matrix}α^{∗} : K; M(= J_{1}^{∗}; K^{∗}; M) ⇒ J_{1}^{∗}; H \\ α : F; M(= J_{0}^{∗}; K^{∗}; M) ⇒ J_{0}^{∗}; H \end{matrix}

to a natural transformation

α^{∗∗} : (K^{∗}; M)|_{ℂ_{0}+ℂ_{1}} ⇒ H|_{ℂ_{0}+ℂ_{1}}

Because of obj(ℂ_{1}^{∗}) = obj(ℂ_{0} + ℂ_{1}) and since each morphism in ℂ_{1}^{∗} which is neither contained in ℂ_{0} nor ℂ_{1} can be represented as X; η^{∗} : X; J_{0}^{∗} ⇒ X; J; J_{1}^{∗} for some X : 1 → ℂ_{0} the equation (*) implies the commutativity of the following diagram:

\xymatrix{X; J_{0}^{∗}; K^{∗}; M(= X; F; M) \ar[r]^{X;η∗;K^{∗};M(=X;(η;M))} \ar[d]_{X;J_{0}^{∗};α^{∗∗}(=X;α)} & X; J; J_{1}^{∗}; K^{∗}; M \ar[d]_{X;J;J_{1}^{∗};α^{∗∗}(=X;J;α^{∗})} \\ X; J_{0}^{∗}; H \ar[r]_{X;η^{∗};H} & X; J; J^{∗}; H}

which shows that the lifting defines a natural transformation

α^{∗∗} : K^{∗}; M ⇒ H.

Evidently holds α = J_{0}^{∗}; α^{∗∗}. Since α determines α^{∗} uniquely, and these two natural transformations determine α^{∗∗} uniquely, it is proved that M : ℂ → Sem is a model of Δ^{∗}.

For the second part we assume now that M : ℂ → Sem is a model of Δ^{∗}, and that a functor H : ℂ_{1} → Sem and a natural transformation α : F : M ⇒ J; H is given.

The universal property of (ℂ_{1}^{∗}, η^{∗}) implies the existence of a functor H^{∗} : ℂ_{1}^{∗} → Sem satisfying J_{1}^{∗}; H^{∗} = H, J_{0}^{∗}; H^{∗} = F; M, and η^{∗}; H^{∗} = α. Since M : ℂ → Sem is a model of Δ^{∗} there is a unique natural transformation α^{∗} : K^{∗}; M ⇒ H^{∗} with J_{0}^{∗}; α^{∗} = id_{F;M}.

The sequential composition of the two natural transformations

η^{∗}; α^{∗} : J_{0}^{∗}; K^{∗}; M ⇒ J; J_{1}^{∗}; H^{∗}

together with the associated equalities

η^{∗}; α^{∗} = (J_{0}^{∗}; α^{∗}) ∘ (η^{∗}; H^{∗}) = (η^{∗}; (K^{∗}; M)) ∘ ((J; J_{1}^{∗}; α^{∗}))

deliver the equality

id_{F;M} ∘ α = (η; M) ∘ (J; (J_{1}^{∗}); α^{∗})

that has to be proved.

If α′ : K; M ⇒ H with η; M) ∘ (J; α′) would be given, then one can lift this natural transformation to α′′ : K^{∗}; M ⇒ H^{∗} with J_{0}^{∗}; α′′ = id_{F;M} and J_{1}^{∗}; α′′ = α′. Because of J_{0}^{∗}; α′′ = id_{F;M} it follows α^{∗} = α′′, so that J_{1}^{∗}; α^{∗} = J_{1}^{∗}; α′′ = α′. This completes the proof of the second part of the semantical equivalence of Δ and Δ^{∗}.

The construction of a semantically equivalent projective ct-sketch for a given projective sketch can be done in a completely analogous way.

If Δ is a projective, respectively injective ct-sketch in ℂ and H : ℂ → ℂ′ any functor, then Δ; H is evidently a ct-sketch in ℂ′. This simple observation allows to extend the construction described above inductively to a construction of semantically equivalent nested ct-sketch of finite depth. □

This observation above makes it possible to describe complex NS-theories basically by the concept of sub theories that are initially or finally constraint. Initial constraints are expressed by injective ct-sketches and final constraints by means of projective ct-sketches.

The construction of complex NS-theories is furthermore based on the fact that the category of nested ct-sketches is closed under injective limits and that these limits can be computed in the category of categories.

Definition 4.3. Let (ℂ^{1}, Δ_{1}), (ℂ^{2}, Δ_{2}) by NS-theories with nested ct-sketches. A functor F : ℂ^{1} → ℂ^{2} is called a theory morphism if the translation Δ_{1}; F of Δ_{1} along F : ℂ^{1} → ℂ^{2} is a subset of Δ_{2}. ℕ𝕊𝕋 denotes category of NS-theories with nested ct-sketches. □

Theorem 4.4. The category ℕ𝕊𝕋 of NS-theories with nested ct-sketches is closed under injective limits and the forgetful functor U : ℕ𝕊𝕋 → ℂ𝔸𝕋 into the category of categories preserves injective limits.

Proof: Since the proof is simple, we sketch only the idea by the example of pushouts. Let

\begin{matrix}F : (ℂ^{0}, Δ_{0}) → (ℂ^{1}, Δ_{1}), \\ G : (ℂ^{0}, Δ_{0}) → (ℂ^{2}, Δ_{2}) \end{matrix}

be theory morphisms, and let

\xymatrix{ℂ^{0} \ar[r]^{F} \ar[d]^{G} & ℂ^{1} \ar[d]^{Q_{F}} \\ ℂ^{2} \ar[r]^{Q_{G}} & ℂ}

be a pushout diagram in ℂ𝔸𝕋. Then is

\begin{matrix}Q_{F} : (ℂ^{1}, Δ_{1}) → (ℂ, Δ_{1}; Q_{F} ∪ Δ_{2}; Q_{G}) \\ Q_{G} : (ℂ^{2}, Δ_{2}) → (ℂ, Δ_{1}; Q_{F} ∪ Δ_{2}; Q_{G}) \end{matrix}

evidently a pushout in ℕ𝕊𝕋. □

Injective limits can be used to define operations that glue together NS-theories. The main construction used in structuring NS-theories is the pushout. We will try to take over the structuring operations from the recently defined specification language CASL, [8].

A specification of an NS-theory (ℂ, Δ) consists of four parts: the first part, indicated by the key word sort, declares (the names of) the objects of ℂ, the second part, indicated by op, declares the generating morphisms of ℂ, the third part, starting with equations, represents the defining relations of ℂ, and the final part, indicated by constraints, lists the initial and terminal constraints contained in Δ.

The first operation for combining specifications is the union: If SP_{1}, …, SP_{n} are specifications then

SP_{1} and SP_{2} and …, SP_{n}

is a specification which combines the specifications such that when any part is common to some of the combines specifications, its interpretation in a model has to be a common one too.

The next operation is the translation which renames the objects and morphisms in a specification by means of a functor, i.e., the translation represents the construction of translating an NS-theory along a functor. The translated specification is written:

SP with {X_{1} ↦ X′_{1}, …, f_{n} ↦ f′_{n}}

The key word then will be used to represent extensions of specifications. We distinguish three different kinds of extensions: simple, free and cofree extensions of a specification.

SP_{1} then SP′

adds conservatively new objects, new morphisms and new axioms to the given specification P S_{1}, i.e. the reduct of a model of the extended specification to the category described by SP_{1} has to be a model of SP_{1}.

SP_{1} then free SP′ [regarding SP′′]

requires that a model of the freely extended specification is an extension of a model of SP_{1} that it satisfies all axioms stated in SP′ and that it forms a left Kan extension of its reduct to SP_{1} within the class of models satisfying SP′′.

Accordingly

SP_{1} then cofree SP′ [regarding SP′′]

requires that a model of the cofreely extended specification is an extension of a model of SP_{1} that it satisfies all axioms stated in SP′ and that it forms a right Kan extension of its reduct to SP_{1} within the class of models satisfying SP′′.

Thus, SP_{1} represents (ℂ_{0}, Δ_{0}), SP′ describes the extension to ℂ_{1} and SP′′ represents Δ_{1}. In this way we are able to represent a single ct-sketch with ℂ = ℂ_{1} and K = Id_{ℂ}. In this way basic patterns of initial and terminal constraints can be defined. By translations this patterns can be adapted to other specifications

It is not the aim of this paper to define a new specification language. We only want to sketch in which way specifications could be composed by means of structuring operations on NS-theories, and we want to be able to represent more complex examples of NS-theories in a readable way.

In the following we give some simple specifications which will be used later to build more complex specifications.

Triv = sorts : Elem end Nat1 = Triv then free

sort Nat ops zero : Elem → Nat

succ : Nat → Nat end

This specification represents the NS-theory of Example 1.

Other basic patterns of constraints are the following:

Terminal = ∅ then cofree sort 1 end

Sum = sort A, B then free sort S op in_{A} : A → S

in_{B} : B → S end

Prod = sort A, B then cofree sort P op p_{A} : P → A

p_{B} : P → B end

In the following specification some of this patterns are used within the constraints part of the specification.

Nat2 = sort B, Nat1, Nat2

op zero1 : B → Nat1 succ1 : Nat1 → Nat1

zero2 : Nat1 → Nat2
succ2 : Nat2 → Nat2

constraints Terminal with {1 ↦ B} Nat1 with {zero ↦ zero1, succ ↦ succ1} Nat1 with {zero ↦ zero2, succ ↦ succ2} end

This specification describes Examples 8 and the following specification Streams = Triv then cofree

sort Streams

op head : Streams → Elem
tail : Streams → Streams end

corresponds to Example 4.

Since product and sum sketches are so frequently used, we will use them as built in constructions, and will not explicitely use the injective or projective sketches described above. In addition we use for terms generated by products and sums the usual notations with variables in order to improve readability. Thus, if generating morphisms f : A × B → C, h : B → A, g : A → B are given, then f(h(x), g(y)) : B × A → C, and f(x, g(x)) : A → C, and if additionally t : C → (A + B) is given, then [g(f(x)), f(x)] : C → B and [g(f(x)), h(f(x))] : C → (B + A).

The specifications given so far correspond to ct-sketches of depth one. The next example represents a ct-sketch of depth two.

Sequences = Triv then cofree sort Sequences, 1 op head : Sequences → Elem

tail : Sequences → (Sequences + 1)

regarding 1, Sequence + 1

end

5 The expressive power of the generic model

By the following examples we will demonstrate, that the investigation of the generic model of an NS-theory can be very helpful for the understanding of the corrsponding structure. Since inductively defined data types are well understood we will predominantly deal with coinductively defined structures.

As made visible in Example 8 some very useful relations between injecitve and projective limites valid in the category of sets are not satisfied in generic models. Since we are basically intersted in model in Set we will enforce some of this properties. A first example in this direction is the specification Bool of truth values.

Bool = sort Bool, Bool + Bool, 1

op true, false : 1 → Bool

inl, inr : Bool → Bool + Bool

constraints Terminal with {1 ↦ 1} Sum with {in_{A} ↦ true, in_{B} ↦ false} Sum with {in_{A} ↦ inl, in_{B} ↦ inr} Prod with {p_{A} ↦ [()_{Bool+Bool}; true, ()_{Bool+Bool}; false],

p_{B} ↦ [id_{Bool}, id_{Bool}]}

end

Up to isomorphism the unique model M : Bool → Set is given by M(Bool) = {true, false}, M(inl)(x) = (true, x), M(inr)(x) = (false, x).

It is easy to see that all operations on truth values are represented in the generic model of Bool. For instance, the conjunction is represented by

[id_{Bool}, (()_{Bool}; false)] : Bool + Bool → Bool

and the disjunction by

[(()_{Bool}; true), id_{Bool}] : Bool + Bool → Bool.

As next we give a specification of the finitary power set construction, which will be needed later to represent the codomain of the state transition function of nondeterministic, image finite transition systems.

Sets = Triv and Bool then free sort Set, Elem × Set, Elem × Elem × Set op empty : 1 → Set

join : Elem × Set → Set

equations x, y : Elem, s : Set join(x, join(x, s)) = join(x, s) join(x, join(y, s)) = join(y, join(x, s)) regarding Elem × Set, Elem × Elem × Set, Bool end

and let be

Set1 = Set then op h : Elem → Bool end

In Set1 with exception of the sort Elem and the morphism h : Elem → Bool all other objects and morphism are subject of a constraint, so that their interpretations are unique up to isomorphisms.

In the generic model of Set1 one can find morphisms

all_{h} : Set → Bool, ex_{h} : Set → Bool

such that for each model M : Set1 → Set of Set and each finite subset X ⊆ M(Elem) hold

• M(all_{h})(X) = true if and only if for all x ∈ X, M(h)(x) = true, and

• M(ex_{h})(X) = true if and only if there is at least one x ∈ X such that M(h)(x) = true.

These morphisms in the generic model are induced by the free extension and respectively by the functors

F_{all} : {Set ↦ Bool, empty ↦ true,
join ↦ and(h(x), y) : Elem × Bool → Bool}
F_{ex} : {Set ↦ Bool, empty ↦ false,
join ↦ or(h(x), y) : Elem × Bool → Bool}

To justify these constructions one has to proof that the given interpretations of the morphism join satisfy the required equations. But, this is easy to see, since conjunction and disjunction are both idempotent and commutative.

The next example approaches transition systems. There are many ways to formalize transition systems. One way is, to understand a transition system as a relational structure with a ternary relation

next ⊆ States × Actions × States

which describes by ⟨s_{1}, a, s_{2}⟩ ∈ next that s_{2} is a possible successor state of s_{1} if the system performs the action a.

Constraining a morphism f : A → B to a monomorphism or dualy to an epimorphism can be done by pullback or pushout sketches, which state that id_{A}; f = id_{a}; f respectively f; id_{B} = f; id_{B} are pullback, respectively pushout diagrams. To be more precise, let be

Pullback = sort A, B, C op f : A → C

g : B → C

then cofree sort P op p_{f} : P → A

p_{g} : P → B

equations

p_{f}; f = p_{g}; g

end

Pushout = sort A, B, C op f : C → A

g : C → A

then free sort P op p_{f} : A → P

p_{g} : B → P

equations

f; p_{f} = g; p_{g}

end

Transition systems can now be formalized as models of the following NS-theory:

TRsystems1 = sort Actions, States, R, States × Actions × States op inc : R → States × Actions × States constraints States × Actions × States Pullback with{f ↦ inc, g ↦ inc, p_{f} ↦ id_{R}, p_{g} ↦ id_{R}} end

If we are interested in the most abstract TR-system for any given set of actions, we have to constrain the model class using a cofree extension.

TRsystems2 = Triv with {Elem ↦ Actions} then cofree sort States, R, States × Actions × States op inc : R → States × Actions × States regarding States × Actions × States Pullback with{f ↦ inc, g ↦ inc, p_{f} ↦ id_{R}, p_{g} ↦ id_{R}} end

However, a functor M to Set is a model of TRsystems2 iff M(States) = {∗} and M(R) = {∗} × M(Actions) × {∗}, i.e., the state set of the most abstract model collapses. The collaps is caused by the lack of observations for the states. This fact may be seen as a hint not to formalize transition systems as such kind of structures.

In a growing number of papers transition systems are formalized as coalgebras, see [9] and [6]. This would leed to the following specification of most abstract transition systems for given sets of actions:

TRsystems = Triv with{Elem ↦ Actions}then cofree sort States, Statesets, Actions × States op next : Action × States → Statesets

empty : 1 → Statesets
join : States × Statesets → Statesets

regarding

Bool, Actions × States

Sets with{Elem ↦ States, Sets ↦ Statesets} end

What about the collaps of the state set in that case? Even though there is no explicite observation operation in the specification TRsystems the state set does not collaps in the most abstract model. This is caused by the fact that in the most abstract model M, within the class of models in Set, two states s_{1}, s_{2} ∈ M(States) are different, if there is a morphism t : States → Bool in the generic model such that M(t)(s_{1}) ≠ M(t)(s_{2}).

In the following we investigate what kind of observations or experiments t : States → Bool in the generic model 𝕃_{TRsystems} exist.

First we have the observation ()_{States}; true : States → Bool which is induced by constraining the object 1 to the terminal one. Using the constraint Set in TRsystems, this observation induces the morphisms

all_{(()_{States};true)} : Statesets → Bool, ex_{(()_{States};true)} : Statesets → Bool.

M(all_{(()_{States};true)}) : M(Statesets) → {true, false} becomes the constant function true, but

M(ex_{(()_{States};true)})(X) = true iff X ≠ ∅.

Therefor we obtain for any (a, s) ∈ M(Actions) × M(States) that

M(next; ex_{(()_{States};true)})(a, s) = true

if and only if there is at least one successor state of s ∈ M(States) performing the action a ∈ M(Actions), i.e.

M(next; ex_{(()_{States};true)})(a, s) = true iff M ⊧_{s} ⟨a⟩true.

This observation can now be used to construct other ones. To make this generation process precise we have to work in the following specification.

Let be Act be a fixed set of actions and let TRsystems[Act] be the specification

TRsystems[Act] = TRsystems then constraints InfSum with Actions ↦ ∑_{a∈Act} 1 InfSum with Actions × States ↦ ∑_{a∈Act} States end

The generic model of TRsystems[Act] contains as observations t : States → Bool all formulae of the modal logic with action set Act. Let for instance be a_{1}, a_{2} ∈ Act and in_{a_{1}}, in_{a_{2}} : States → ∑_{a∈Act} States the corresponding injections of the infinite sum, then

t_{⟨a_{1}⟩true} = in_{a_{1}}; next; ex_{(()_{States};true)} : States → Bool

represents the modal formula ⟨a_{1}⟩true, and

in_{a_{2}}; next; all_{t_{⟨a_{1}⟩true}} : States → Bool

represents the modal formula [a_{2}]⟨a_{1}⟩true.

The specifications TRsystems and TRsystems[Act] are related in such a way that the unique model of TRsystems[Act] in Set is isomorphic to that model M of TRsystems with M(Actions) = Act.

It is well known that for image finite transition systems two states are equivalent with respect to strong bisimulation if they cannot be distinguished by any formula of modal logic. Therefore, the unique model of TRsystems[Act] in Set is fully abstract with respect to strong bisimulation and can be constructed as the canonical model of the modal logic with action set Act, see [4]. A construction of the unique model of TRsystems[Act] as terminal coalgebra of the endofunctor,

P_{Act} : Set → Set with P_{Act}(X) = (P_{fin}(X))^{Act},

where P_{fin} : Set → Set denotes the finitary power set functor, is given in [1] and [10].

It is this example which from our point of view justifies to understand the generic model of an NS-theory as a minimal logic representing essential properties of the specified structures. But this example demonstrates additionally, that one can not expect very interesting properties of the categories of models of an NStheory in a given category Sem. It seems that there is some kind of tradeoff in the interest in the model class of an NS-theory and the generic model: If the model class has reach structure the generic model seems to be rather simple and conversely, if the model class has a simple structure (being an isomorphisms class for instance) all the more interest deserves the generic model.

An advantage of models of NS-theories over coalgebras is the possibility to deal with binary state transition functions. To demonstrate this we consider the following specification:

2-1-TreeFun = Triv with cofree sort St, St × St op head : St → Elem

tail : St → St
comp : St × St → St

regarding St × St

end

Without the product object St × St and the binary state transition operation comp : St × St → St this specification would define the infinite streams over the freely interpretable sort Elem. The existence of the binary state transition operation does not cause any problems to qualify the models M_{cofree} : 2-1-TreeFun → Set. One has just to apply the usual construction of a right Kan extension to see that

M_{cofree}(St) = {f : T_{St→Elem} → M(Elem)},

where T_{St→Elem} denotes the set of all terms with one variable of sort St that produce a value of sort Elem. These terms may be illustrated as trees with at most two subtrees, i.e., one or twofold branching trees.

To prove the required universal property of M_{cofree} : 2-1-TreeFun → Set we consider the algebraic signature

2-1-Tree = sort St op s_{0} : 1 → St

tail : St → St
comp : St × St → St

end

The set of terms T_{St→Elem} forms an initial algebra of 2-1-Tree, so that for each model M : 2-1-TreeFun → Set and each m_{0} ∈ M(St) there is exactly one 2-1-Tree-homomorphism

f_{m_{0}} : T_{St→Elem} → M_{cofree}|2-1-Tree

with f_{m_{0}}(s_{0}) = m_{0} which defines a mapping

h_{m_{0}} : T_{St→Elem} → M_{cofree}(Elem)

by h_{m_{0}}(t) = M(head)(f_{m_{0}}(t)), i.e. by applying M_{cofree}(head) to the unique value of t (als element of the initial 2-1-Tree-algebra) in the 2-1-Tree-algebra M_{cofree}|2-1-Tree canonically derived from M_{cofree} by interpreting s_{0} by m_{0}. This construction delivers the required unique homomorphism from M to M_{cofree}.

It is worth to mention, that in this and similar examples the set of distinguishing observations can canonically be constructed as an initial algebra. This makes it additionally possible, to use equations within the cofree constraint part of a specification, i.e. one can easily deal with state valued equations in specifications of processes.

References

[1] M. Barr. Terminal coalgebras in well–foundet set theory. Theoretical Computer Science, 114:299–315, 1993.

[2] M. Barr and C. Wells. Category Theory for Computing Science (second edition). International series in computer science. Prentice Hall, 1996.

[3] J.A. Goguen and R. M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39:95–146, 1992.

[4] Robert Goldblatt. Logics of Time and Computation. Number 7 in CSLI Lecture Notes. CSLI, Center for the Study of Language and Information, second edition, 1992.

[5] T. Hagino. A categorical programming language. PhD thesis, Edinburgh University, 1987.

[6] Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS, (62):222–259, June 1997.

[7] F.W. Lawvere. Functorial semantics of algebraic theories. Proc. Nat. Acad. Sci. U.S.A., 50:869–873, 1963.

[8] CoFI Task Group on Langugage Design. Casl, the common algebraic specification language (summary). Technical report, CoFI: The Common Framework Initiative, 1998.

[9] J.J.M.M. Rutten. A calculus of transition systems (towards universal coalgebra). In A. Ponse, M. de Rijke, and Y. Venema, editors, Modal Logic and Process Algebra, a bisimulation perspective, volume 53 of CSLI Lecture Notes, pages 231–256, Stanford, 1995. CSLI Publications. FTP-available at ftp.cwi.nl as pub/CWIreports/AP/CS-R9503.ps.Z.

[10] J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Technical Report CS-R9652, CWI, Amsterdam, 1996. to appear in Theoretical Computer Science.