ñòð. 3 |

which summand the result of any operation shall be. The choice, in general, leads

to nonisomorphic term models which are nevertheless initial in a more general

sense which we will make precise.

1.3.1 DÂ½mons How to make the choice? Clearly there is no systematic way.

One way of dealing with the problem is to take all choices, or at least to explore

all choices. In the example in Section ES 1.2 of Â¯elds, we mentioned that not

all choices are possible; once 2 60, it followed that also 4 60. (Recall that in

= =

that example, saying that something is zero is saying that it is in one of two

summands.)

More generally, suppose we have an FD sketch and there is an operation s : a

Â¡ b and a cocone expressing b = b1 + b2 + : : : + bn . If we are building a model M

!

of this sketch and we have an element x 2 M (a), then M (s)(x) 2 M (b), which

means that we must have a unique i between 1 and n for which M (s)(x) 2 M (bi ).

(For simplicity, this notation assumes that M (b) is the actual union of the M (bi ).)

6 Finite discrete sketches

Now it may happen that there is some equation that forces it to be in one

rather than another summand, but in general there is no such indication. For

example, the result of a push operation on a stack may or may not be an overÂ°ow,

depending on the capacity of the machine or other considerations. Which one it

is determines the particular term model we construct and it is these choices that

determine which term model we will get.

Our solution is basically to try all possible sequences of choices; some such

sequences will result in a model and others will abort. Thus as we explore all

choices, some will eventually lead to a model; some will not. The theoretical tool

we use to carry out this choice we call a dÂ½mon. Just as a Maxwell DÂ½mon

chooses, for each molecule of a gas, whether it goes into one chamber or another,

our dÂ½mon chooses, for each term of a model, which summand it goes into. The

following description spells this out precisely.

1.3.2 DeÂ¯nition Let be an FD sketch and suppose the maximum number

of nodes in the base of any cocone is Â·. A dÂ½mon for is a function d from

the set of all strings in the alphabet A (see 7.6.5) of the underlying FP sketch

(in other words, forget the cocones) to the initial segment f1: : Â·g of the positive

integers.

1.3.3 We will use a dÂ½mon this way. We assume that the nodes in the base of

are indexed by 1; 2; : : : ; k where k Â· Â· is the number of nodes

each cocone of

in that cocone. In constructing an initial algebra, if a string w must be in a sort

which is the vertex of a cocone (hence in the model it must be the disjoint union

of no more than Â· sorts), we will choose to put it in the D(w)th summand. If

D(w) > k, the construction aborts. We will make this formal.

1.3.4 Construction of initial term models for FD sketches This con-

struction includes the processes in 4.7.10 and 7.6.5; we repeat them here modiÂ¯ed

to include the eÂ®ects of a dÂ½mon D. The alphabet is the same as in 7.6.5.

If a node b is the vertex of a cocone with k = k(b) summands, the summands

will be systematically denoted b1 ; : : : ; bk and the inclusion arrows ui : bi Â¡ b for

!

i = 1; : : : ; k. If b is not the vertex of a cocone, then we take k(b) = 1, b1 = b

and u1 = idb . We denote the congruence relation by Â» and the congruence class

containing the element x by [x]. Rules FD{ES 3 through FD{ES 6 refer to a cone

C in of the form:

q

Â¡ @

p1 Â¡ @

pi pn

Â¡ @

Â¡

Âª ? R

@

a1 ai an

Â¢Â¢Â¢ Â¢Â¢Â¢

FD{1 If ui : ai Â¡ a is an inclusion in a cocone and [x] 2 I(ai ), then [ui x] 2 a and

!

I(ui )[x] = [ui x]. (Thus we ignore the wishes of the dÂ½mon in this case.)

1.3 Term algebras for FD sketches 7

FD{2 Suppose f : a Â¡ b in , f is not an arrow of the form ui , and [x] 2 I(a). Let

!

j = D(f x) (we ask the dÂ½mon what to do). If j > k(b), the construction

aborts. Otherwise, we let [f x] 2 I(bj ) and I(f )[x] = [uj fx].

FD{3 For i = 1; : : : ; n, let [xi ] be a term in I(ai ). Let

j = D(C(x1; : : : ; xn ))

If j > k(q), the construction aborts. If not, put [C(x1 ; : : : ; xn )] in I(q j ).

FD{4 If for i = 1; : : : ; n, [xi ] and [yi ] are elements in I(ai ) for which [xi ] = [yi ],

i = 1; : : : ; n, then

[C(x1 ; : : : ; xn )] = [C(y1 ; : : : ; yn )]

FD{5 For i = 1; : : : ; n, I(pi )([C(x1 ; : : : ; xn )]) = [xi ].

FD{6 For x 2 I(q),

[x] = [C(p1 x; : : : ; pn x)]

FD{7 If hf1; : : : ; fm i and hg1; : : : ; gk i are paths in a diagram in , both going

from a node labeled a to a node labeled b, and [x] 2 I(a), then

(If1 Â± If2 Â± : : : Â± Ifm )[x] = (Ig1 Â± Ig2 Â± : : : Â± Igk )[x]

in I(b). If

D(f1 f2 : : : fm x) 6D(g1 : : : gk x)

=

(causing (If1 Â± If2 Â± : : : Â± Ifm )[x] and (Ig1 Â± Ig2 Â± : : : Â± Igk )[x] to be in two

diÂ®erent summands of I(b)), then the construction aborts.

This construction gives a term model if it does not abort. It is an initial model

for only part of the category of models, however. To make this precise, we recall

the deÂ¯nition of connected component from 4.3.10. It is easy to see that each

connected component is a full subcategory of the whole category of models.

1.3.5 Proposition For each dÂ½mon for which the construction in FD{1 to

FD{6 does not abort, the construction is a recursive deÂ¯nition of a model I of

. Each such model is the initial model of a connected component of the category

of models of , and there is a dÂ½mon giving the initial model for each connected

component.

We will not prove this theorem here. However, we will indicate how each model

determines a dÂ½mon which produces the initial model for its component. Let M

be a model of an FD sketch . Every string w which determines an element of

a sort I(a) in a term model as constructed above corresponds to an element of

M (a). That element must be in a unique summand of a; if it is the ith summand,

then deÂ¯ne D(w) = i. On strings not used in the construction of the term models,

deÂ¯ne D(w) = 1, not that it matters.

8 Finite discrete sketches

Our deÂ¯nition of dÂ½mon shows that one can attempt a construction of an

initial model without already knowing models. In concrete cases, of course, it will

often be possible to characterize which choices give initial models and which do

not.

1.3.6 Confusion maybe, junk no The slogan, `No junk, no confusion' is only

half true of the initial models for FD theories. The `No junk' half of the slogan

expresses exactly what we mean when we say that every element is reachable.

There are no extraneous elements. `No confusion' means no relations except those

forced by the equations in the theory. As we will show by example it may happen

that some initial models have confusion and others not. Later we give an example

of a sketch that has more than one unconfused initial model and one that has no

unconfused initial (or noninitial) model.

If there is just one unconfused initial model, that one may be thought of as

a `generic' model. The others remain nonetheless interesting. In fact, it is likely

that the generic model is the one that cannot be accurately modeled on a real

machine.

1.3.7 Example A typical example of a sketch with many initial models is the

sketch for natural numbers with overÂ°ow. The generic model is easily seen to be

the one in ES 1.1.5 in which the overÂ°ow state is empty. The models with overÂ°ow

in ES 1.1.6 are all initial algebras for some component of the category of models,

but they have confusion, since nothing in the sketch implies that the successor of

any element can be the same element. None of these models have junk.

The modular arithmetic models of ES 1.1.7 are not initial models; in fact they

are all in the same component as the natural numbers since the remainder map

(mod N ) is a morphism of models. They also have no junk.

1.3.8 Example Here is a simple sketch with no generic model. It has two initial

models, each satisfying an equation the other one does not. There are Â¯ve nodes

a = b + c, d and 1. There is one constant x of type d, and a single operation s : d

Â¡ a. The initial models have one element { the constant { of type d. One of the

!

initial models has an element of type b and the other an element of type c.

ñòð. 3 |