D IAGRAMMES

I. N ÉMÉTI
Foundations for stepwise refinement of program specifications
via cylindric algebra theory
Diagrammes, tome 8 (1982), exp. no 1, p. N1-N24
<http://www.numdam.org/item?id=DIA_1982__8__A1_0>

© Université Paris 7, UER math., 1982, tous droits réservés.
L’accès aux archives de la revue « Diagrammes » implique l’accord avec les conditions générales d’utilisation (http://www.numdam.org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright.

Article numérisé dans le cadre du programme
Numérisation de documents anciens mathématiques
http://www.numdam.org/

Diagrammes, Volufi* 8, ftrifi 1982,

Foundations for
stepwise refinement of Program Spécifications
via
Cylindric Algebra Theory

I. Németi

1. Introduction.
To investigate connections between différent théories formulât ed in completely différent languages is a problem in many
branches of computer science , e. g. in structured prograraming,
in structuring program spécifications, Burstall-Goguen (77),(79),
Goguen-Burstall (78),(80),(79), Domolki (79), Mosses (79), in
data types and semantics, Blum-Estes (77), in A* I. , AndrékaGergely-Németi (72), McCarthy-Hayes (69), Andréka-Németi (79a)
etc.•• The connections between the différent théories and languages can be called interprétations or trnslations but translations
would suggest something much simpler than the thing we hâve in
roind. Most often they are called Theory Morphisms. One point to
be stressed is that between two théories there are usually many
theory morphisms. The subject of investigation hère is actually
a category consisting of théories and their morphisms. The notion
of a theory morphism from the theory

T

into the theory

defined for example in

Winkowski (78) §1 (p. 277)

was called a modelling

\x

T

f

of the

theory

T

Tf

was

and there it

in the other one

. I n that paper theory morphisms are used to study Computer

Simulation.
There is a related branch of ••standard" Universal Algebra
called Lattice of Varieties, see Gratzer (79) p. 389. That lattice

N 2
is a spécial subcategory of the Category of Théories considered
hère. For the purposes reported hère, it is too spécial for two
reasons s
1. The main point in the présently reviewed field is that the
théories are of différent similarity types.
2. Between two théories there are many morphisms.
(In some Computer Science papers the Category of Théories was
called "Hierarchy of Languages" to emphasize that the underlying
languages, similarity types, or even logics are usually différent,
see Andréka-Gergely-Német (72), Rattray-Rus (77), Andréka-Németi
(79a), Sain (79b).)
Hère we quote three approaches which are complémentary (and
are most useful when applied together).
(1.1) Let the théories Th-

and Th 2

heterogenous (many sorted). Let

F A/ 1

be aquatlonal but possibly
and F 0 be the countably
/\/ 2

generated free algebras of the varieties

Mod(Th;.) and

respectively. Then a suitable homomorphism h: F -

Mod(TlO
>

A/ 1

F„
/y

2

could establish a connection between the two théories i. e.
between the two varieties. The problem is that

Fn

and

r** 1

F„
+* l

are usually of completely différent similarity types ! Hence
the notion of a homomorphism between them is just meaningless.
To alleviate this problem, Blum-Estes (77) generalized the usual
notion of homomorphism to be defined between algebras of différent
similarity types* One définition could be to say that
is a generalized homomorphism if f
of A

f: A — > B

takes every term function

into some term function of B . That is, the image of an

opération of

A

is required to be a function definable in B .

One can then make restrictions (or generalizations) on the notion
of definability used e. g. term-definable, first-order definable,
implicitely definable by first order formulas etc... Then the
Theory of Definability

which is a branch of Model Theory, see

for example the Chang-Keisler monograph, can be used as a guide

N 3
for choosing the notion with the desired properties from a fairly
broad spectrum of existing and well understood ones. For some
varying choices see Blum-Estes (77), Blum-Lynch (79a),(79b).
(1.2) One of the main aims of Algebraïc Théories of Lawvere is to
deal with the présent problem. I. e. the aim is to investigate the
"structure" or"systemHconsisting of several théories of several
similarity types and several possible "interprétations" (i. e.
connections) between thèse théories and languages. Hence this is
not a mère translation of Universai Algebra into category theoretical language, but instead this is an approach to a problem
inhérent both in Uni versai Algebra and in Model Theory s to a
problem which has not been attacked in "standard" Univeral Algebra
or Model Theory yet. Though it should be mentioned her thats the
Lattice of varieties, Reducts, Clone Algebras, see Gratzer (79),
are branches in "standard" Universal Algebra which might be applicable to the présent problem. Our reason for pointing this out
is that there hâve been misinterpretations saying Lawvere*s
Algebraïc Théories were merely "new bottles for old wine".
Algebraïc Théories hâve been widely applied to the quoted
Computer Science problems and from thèse applications the theory
itself benefited considerably. Some of the références ares
Elgot (71),(75), Tiuryn (79a), Wand (75a),(77a), Goguen-Burstall
(78), Wagner et al (77),(76), and other works of the ADJ team.
The field is too extensive to make proper références hères our
références are samples chosen in a random manner,
Burstall and Goguen hâve made a distinction hère which is
worth of emphasizing. Namelys Stepwise refinement of programs and
stepwise refinement of spécifications are two différent matters
which need différent tools. The former needs Rational Algebraïc
Théories, ADJ (76), or itérative ones, Elgot (75), while the second needs only plain Algebraïc Théories. In program spécifications,
in their stepwise refinement, etc..., no algorithms are involved.
Spécifications are only déclarative statements. Hence in the

N 4
theory (or foundations) of Spécifications no algorithmic or itérative notions are needed.
Spécifications are important in themselves. Spécifications
are answers to "what" while programs are answers to "how".
Sometimes it is more important to understand clearly what we are
trying to do than to understand how we are trying to do it. It is
valuable to be aware of what one really does intend to do and
what one does not (and what one just happens to do without really
intending).
An autonomous theory of spécifications is badly needed. An
approach to that is Burstall-Goguen (77),(79), Goguen-Burstall
(78),(80),(79), Mosses (79) etc..
(1.3) The category of ail first-order théories and their morphisms
can be treated naturally by using Cylindric Algebras, Németi-Sain
(78). Hère a theory morphism correspond to an homomorphism between
two cylindric algebras. This correspondent works both ways. A représentation theorem to this effect was formulated in Németi-Sain
(7 8), and Sain (79b). See Thm. 5 in the présent paper. The category
of théories obtained this way is complète and cocomplete, thence
"Theory Procédures" of Burstall-Goguen (77) do work in this setting
too, see Thm. 4 in this paper. Hère, the so-called "Regular Cylindric Algebras" are the main tool for handling ail first order
théories see Prop. 1 in Németi-Sain (78). For regular cylindric
algebras see Henkin-Monk-Tarski (79), Andréka-Gergely-Németi (77),
Németi-Sain (78). In the latter two références they were called
"i-finite" instead of "regular". "Base homomorphisms" of cylindric
set algebras do représent theory morphisms see Sain (79b),
Andréka-Németi (79b).
By this kind of Algebraïc Logic one can go beyond ciassical
first order logic and languages as was shown in Andréka-GergelyNémeti (77) and Németi-Sain (7 8).
In this paper we shall not explain in more détail than it
was done in sec. 1 , 2 , how and why the category of ail first

N 5
order théories and theory morphisms is considered to be the basic
device for stepwise refinement of program spécifications. For
detailed explanations the reader is kindly referred to e. g.
Burstall-Goguen (77),(79) and Goguen-Burstall (78)-(80). However,
if we keep in mind that algebraïc théories (and their morphisms)
are spécial cases of first order théories (and their morphisms)
then reading sec. 1 , 2

again might be sufficient to see the point,

i. e. to see that an appropriate study of the category of ail
first order théories and their morphisms is soaehow a mathematical
foundation for an autonomous theory of spécifications (in the
sensé outlined in sec. 1 , 2 ) .

2» The category of ail first order théories.
Définition 1 (théories, concepts).
(i) By a similarity type

t we understand a pair

t = < H,tf >

t1* Dom(tf)

such that

t»

is a function

where N

is the set of natural numbers and 0 £ N , and

Dom(tf) . Let < r,n> €

H c

If r € H

then r

symbol, if r £ H

t*

>

N

(i. e. let t*(r) = n ).

is said to be an (n - l)-ary function
then r is said to be an n -ary relation

symbol.
(ii) Throughout the paper

xs Ord >

>

Sets

one function defined on the class Ord
I. e.

if

Let

a € Ord

F~

ot < (3

are two

and let

t

is a fixed one-

of ail ordinals.

ordinals then x

£ TU .

be a similarity type.

dénotes the set of ail first order formulas with

equality and with variables in £x. s i < a} , see
Chang-Keisler (73), Monk (76).

e. g.

N6
(iii) Let a be an ordinal, A x c p ^ and 1*€ F .
The semantic conséquence Ax l=:f is defined the usual
way, see e. g. the références in (ii).
(iv) By a theory T in a variables we understand a pair
T = < Ax,Fv> such that t is a similarity type and
Ax c f^ .See Def. 11.29. of Monk (76).
(v) Let T be a theory, Then the set CL, of the concepts of
T is def ined as follows. Let T = < Ax,F? > . Then
— T S F t x F is defined by
(Vf ,f

»ow

EF^ ) p S I f

q, «

^ ,„ T .

End of Définition 1.
Convention.
Throughout, a dénotes an arbitrary ordinal.
Let i be a number.
f
Then t.
« < H,i ,t.
> ', Ax.
e F? , T.
= < Ax.
,F? > .
i
l
i — t. *
i
i t.
i

i

Définition 2 (interprétations - cf. Monk (65), Def. 11.43 , theory
morphisms, concept-interprétations).
Let T- and T 2 be théories in a variables.
(i) Let m t F^
t

i

> F? .

H

We define < T 1 ,m,T„ > to be an interprétation going from
T, into T» (or an interprétation of T. in T_ ) iff
conditions (a)-(c) below hold:
(a) m( x. = x. ) = ( x. = x.) for every i,j < a »

(b) m(*f A ? ) = m(*f) M B ( Y ) ,
m( 1 f ) = 1 m( f ) ,
m( 3 x . f ) = 3x i m (^) ,
for ail ^, ^ € F?
and i < a ,

N 7
Ax2 \Z m("f) for ail

(c)

We shall often say that

m

m ,n
^

be two interprétations of T-

, < T-,n,T2 >

are def ined

(iii) Let < T lf m,T 2 >

> n(f)1

for ail

precisely

< T1,m,T2 > / s ) to bes

m/*

{ <T 1 ,n,T 2 >

?

^ € F^ .

be an interprétation.

We define the équivalence class m/-5

s n 2. m

\x: T-

(iv) By a theory morphism

of

m

(or more

} .

> T2

going from T-

we understand an équivalence class of interpré-

tations of T 1
jj^ T

, iff

(a) below holds.

(a) AX2 fcr j~m(^) <

into T 2

frf

in T 2 .

semantically équivalent, in syrabols m SE n

condition

Axx

< T-,m,T2 > •

The interprétations < T lf m,T 2 >
to

such that

is an interprétation but in

thèse cases we actually mean
(ii) Let

^ € F^

in T 2 , i. e.

» > T2

iff

\x

p, « m/^

is a theory morphism

for some interprétation

< Tx,m,T2 > .
End of Définition 2.

Définition 3 (présentations of theory morphisms).
Let T-

and T 2

be two théories in a

variables.

(i) By a présentation of interprétations from Twe understand a mapping

ps t*
1
(ii) The interprétations < T-,m,T2 >
p: tj

~-> F**

iff

to

T2

> Fr •
c
2
satisfies the présentation

for every < r,n > € t!

conditions

(a) and (b) below hold.
(a) If

r € n^

then m(r(xQ,...,xn_2) « x

^) = p(r,n).

.

N 8
(b) If r (f H 1

then m(r(xQ,. •. >xn--1))

u

PCcfn) .

We define the theory morphism p, to satisfy the présentation
p

if < T lf m,T 2 >

satisfies

p for some < T-,m,T2 > € p, •

End of Définition 3.

Proposition 1 (présentations détermine morphisms uniquely).
Let TLet

and T 2

ps t* —

> F^ be a présentation of interprétations from

i

Tx

be two théories in a variables.

t2

to T 2 .

Then there is at most one theory morphism which satisfies

p .

QED

Définition 4.
(i) Tî^

is def ined to be the pair llf

< ObTH** , MorTHa >

~

of classes where
ObTrf1

s-

{T : T

is a theory in a

variables }

(i. e.

ObTH0^ = { < AxfP^ > Ï t is an arbitrary similarity type
and

MorTflF

~

(ii) Let \ii T-

Ax g F^ }

)

{ < T 1 ,(i,T 2 > s p, i s a theory morphism
^. T
> x 2 and T $ x 2 ç QbTH*1 3 .
> T2

and

> T3

vs T 2

be two

theory morphisms. We def ine the composition v.p.s T-

> T3

to be the (unique) theory morphism for which
( 3 m ^ [ l # i n Ç v ) V.p, = (n.m)/»
where the function

(n.m)s 1^

> 1^

h

3

Z

(n.m)(f) s n(mOf )) for ail ^ € ï?
z

is def ined by

.

l

(iii) Let T » < Ax,F^ >

be a theory. The identity function
~

Idjût is def ined to be

Icyx

The identity morphism

ItL, on T

£<f ,f > s f € F^ 3 .
is def ined to be

N 9

Idj

—

(idpOO/n

End of Définition 4.
From now on we shall use the basic notions of category theory, see
Herrlich-Strecker (73).
Proposition 2.
TH00

is a category with objects ObTH00 , morphisms MorTI^,

composition
Id

X

fo r a X I

v.p, for any p,,v € MorTH^
T e 0bTî

and identity morphisms

^ •

Proof.
Fact 2.1. Let p,s T-

> T2

be a theory morphism. Then there

is a unique mapping \x s CL, —
concepts (of T-

and T 2

> CL,

between the sets of

resp.) such that

(Vm€^)(Vf€F^t ) {T (f/«LT ) = m(1))/^
T .
l
l

l

2

Fact 2.2. < ObT!T%Interprétations >

is a category with usual

set theoretic composition <T-,(n.m),T~ >
< Tx,m,T2 >

and < T2,n,T3 >

of interprétations

and with identity < T,IdFa#T >

for every theory T r < Ax,JEr > •
QED
Now we shall use the category theoretic notion of isomorhism
between théories. Two théories Tisomorphic iff in the category T^

and T ?
1

are defined to be

the objects T-

and T 2

are isomorphic in the category theoretical sensé, i. e. iff there
are two morphisms p,s Tsuch that p,.v « IcL,

and

> T2

and

v.p, = IdL

.

vs T-

> T-

N 10
Proposition 3,
Let T = < Ax,F^ >

be an arbitrary theory with

Then there exists a theory T = < Ax >%+>

t = < H,tf > .

such that (i)-(iv)

below hold.
+

+

(i) t = < 0,tf >

(i. e. t

is the same as t*

there is no function symbol in t
empty set.
(ii) T and T

are isomorphic, i. e. T^s T

(iii) Let the présentation
p(r,n) «•

) where 0

ps t1

r(xQ,...,x

is the

.

-> Fr+

be def ined as

,) for every < r,n > £ t f .

Then there is an isomorphism p,§ T
satisfies

except that

*~> T

which

p , i. e.

( B m Ç. (i)(V< r,n > € t f ) r(xQ,...#x

if r € H
j^) =V
m(r(x(),...,xn^1))
if r i H

(iv) The above interprétation ms F^

> F +

is

effective (is a computable function).
Proof.
The proof is based on Thm. 10.5 of Bell-Machover (77).
QED
To formulate Theorem 4 below we use the notion of completeness of
catégories in the sensé of Herrlich-Strecker (73) or équivalently
MacLane (71). For those unfamiliar with thèse notions we shall
recall them after having formulated Thm. 4 •
Theorem 4.
(i) The category TH0^ of ail théories is complète and cocomplete.
(ii) There is an effective procédure to construct the limits and

N 11
colimits of the effectively given diagrams in TET ,
Before proving Thm. 4 we shall recall the basic notions used in
its formulation, and shall try to illustrate its meaning.
By a small category we understand a category £ = < Ob£,Mor£ >
such that MorC is a set.
Examples.
(1) Every partially ordered set is a small category? let
< P> £ >

be a partial order, then < P, {< a,b > € P x P :

a < b3>
is a small category.

a^rl^D
(2) P

(3)

w

* s a small category .

(
^ 0 ^T

°^3

(4) E

^s a small category.

iç^3

*~ l~J

f 0

is a small category,

b
End of examples.
By a

diagram in the category TH^ we understand a functor
Ds C
> l¥r where £ is a small category, and a functor is
a pair D » <D ,D-> of functions DQs 0b£
•—> ObTH0^ ,
D. : Mor£
> Morïrf* such that D préserves the basic structure
of £

i. e. (i)-(iii) below hold.

(i) If fs A
in T}f

— > B in £

, then D ^ f ) : D Q (A)

> D Q (B)

.

(ii) Dx(f.g) « D1(f).D1(g) for ail f,g € Mor£ .
(iii) D x (Id A ) = IdD , A) for ail A € 0b£ .
The category C is called the index category of the diagram D .

N 12
Examples.
(5) Let

P

be the category in Example (2). Let

be any functor. Let T. = DQ(i) for
\i

~

Dx(a) , V sf

are théories and p,, v
diagram

D

i< 3

Ds P

> TflP

and let

Dx(b) . By définition, T Q , T][ , T 2
are theory morphisms • Then the

is usually il lustrât ed as

v
We do not indicate the identity morphisms

D,(i,i) , i < 3 ,

if not needed.
The historical reason for calling thèse functors diagrams
is the possibility of illustrating them as we hâve just done.
(6) In the above diagram we may choose

D Q ( D = D n^ 2 ^ f T h e n w e

obtain

(7) If we replace the index category of the above diagram by
E

given in Example (4) then we obtain

T

JL -> T
V

It is important to keep in mind that the diagrams (6) and (7)
above are différent !
End of Examples.
Définition 5 (cône, colimit, limit).
Let Ds 1^ •(i) A cône over

> TH01
D

be a diagram. Let ^ = < I,M > .

is a System

<<h. s i € I > f T >

such

N 13

that TÇObTuF, (Vi 6 I) h. € MorT*^
if

f. i — ^ _ > j i n ^

(ii) The colimit of

D

and for every f € M

then h. = h..D1(f) in THP .

in TH a

is a cône < < g. s i

€ I> ,G >

over

D

such that for every cône < < h . s i € I > , T >

over

D

there is a unique morphism p,s G —

(Vi € D \

> T

such that

a (i.gi .

(iii) The limit of

D

is defined exactly as above but ail the

arrows are reversed.
End of Définition 5.
Examples.
(8) The colimit of the diagram

Tr

Example (5) is a theory T 3

given m

and two theory morphisms V

9P

such that

M-^ 1 \ ?
T 2

V-v^
and

^

/

V'.p, » P , v , and for any other T,

|3.p, =

â •V

and

then there is a unique TTS T~

p , b

if

— > T.

such that TT. x* = TT. P

(9) The colimit of the diagram in Example (7) is a single theory
morphism

^f

and a theory T~

->

and

y(»\i * 7f»v etc...

L

l

such that

— > T,

N 14
Note that the différence between diagrams (6) and (7) shows
itself in that in the colimit of (6) there are two morphisms y*
P

from T,

into T~

while in the colimit of (7) there is

only one.
(10) Let the index category j[ of the diagram
in Example (3). Then our diagram
T

D

be the one

D has the shape

T

!• e. no morphisms except the identity ones,
The limit of this cdiagram is a theory T?
TT0 , TN

and two morphisms

such that
T

«°/ *\i
l

0

1

anf for every similar cocone < T^,(3,d >

there is a unique

morphism

j3 = rr0. p, and

p,s T^

• •"»« > T 2

such that

â = T^.p, .

End of Examples.
Limits of the kind of Example (10) are called products and are
denoted by Tfl x T ,

. If T 0

and T 1

are two théories then

N 15
is defined to be the limit in Example (10) and is called the
product of T
the

and T.. • The morphisms TTQ

and TT., are called

Projections of the product.

Définition 6.
A category K is said to be complète and cocomplete if for every
small category ,1 and for every diagram (i. e. functor)
0S i*
,,,„, > K b0th the limit and the colimit of D exixt in K •
End of Définition 6.
By the aboves we see that Theorem 4 says that every diagram
Ds I

> TH** has both limit and colimit in TH** . I. e. in

the category T¥r

of ail théories ail possible limits and coli-

mits exist (and can be constructed).
Exaiaples.
(14) Let T

~ < 0,F.^> , T
~ < Ax..
l , Fz ^ > , where
u
tQ
i
l
tQ = < 0,{ < R,2 > 3 > , tx = < £+3,{ < + , 3 > 3 > and
A*! îf C (3¾4,3¾ = x 0 ) , ( ( x 0 ^ p + x 2 ^ H x 1 ^ ) ) , x 0 + x 1 = x 1 + x 0 } ,
Let p, s T Q — — - * > T-

and

V s T '••»"•"»> T

be two

theory morphisms such that for some m € p, and n € v we
hâve

m(R(x(),x1)) = X Q + X J ^ ^

and n(R(x Q ,x 1 ) = ^ + ¾ 3 8 3 ¾ •

(a) Consider the diagram
T

T

o

l

The colimit of this diagram is

T

l

N 16
T

1

/1

Tx 2
where T« « "Lattice theory" , i. e.
T^ «- <
^A:"V*^ > * Where *2 = < t*>
2
and

^'tK +'3 >,<C *'3 ^ >

Ax^ « {(x^)+(x0.x1)=x0),(x0.(x0+x1)=x0)3
U {(x0.x0^)f((x0.x1).x2=x0.(x1.x2)),(x0.x1=x1.x())3
U Axx

.

£> and S are such that r(x0+x1=sx2) s ^+¾ 5 ¾ a n d
d(x Q +x 1 =x 2 ) = X Q . X ^ X ^ for some r Ç |> and d € b .
(b) Consider the diagram
T

JL

l

0

~>

T
L

l

>

The colimit of this diagram is

—il,

>

T

f
T —-!

>T

where T 2 «s < Ax^F^4* > and
Ax2 = { x 0 ^ ^ ^ > ( x Q ^ ) ^ ^ + ( x 1 ^ ) , ^ ^ a x Q ,

x0+x1=x0—5^-¾ 3
Proof.
Proof of (a).
1). Proof of P •(! = d»v s
r(m(R(x0,x1))) = r ^ + x ^ X j ) = X Q + X J * ^

,

N 17

d(n(R(xQ,x1))) « d(x0+x1=x()) = xQ.x1=x0 .
We hâve to prove r.m = d.n , i. e. we hâve to show
(x 0 +x 1 =^ x )/£ T

~

' i # e°

^^i^o^^T

A ^ 1«

(XQ+X^XJ

Suppose

x^^x.^x^ . Then

that

<—~-> x 0 .x 1 =x Q ).
xQ.x1=x0.(x0+x1)=^0

by

(^).(x^)+x1)=x0) € Ax^ .
We obtain

Ax2 \m

(XQ.X^XQ

>

XQ+X^X^

similarly.

2). Suppose

Pf,p, « ô'.v • We hâve to show TT. P = £ f

and TT.Ô K è*

for some theory morphism TT •

T

Let rf € £ »

and

2 « < * 3 ' Tt* >
df € ô 1 .

Ax£ •* (rt(x0+x1=x1) <•—-> d K x ^ ^ s * ^ ) ) by
Let

p(x0+x1=x2) =¾

p(xD.x1=x2) ^

and

d^XQ+Xj^^) .

We hâve to show that
^ .i

rf(x0+x1=x2)

p détermines a theory morphism

> T| . I. e. we hâve to show that

( V f € AX2) Ax£ \m
Notations

p(f ) .

r*(+) = fr , df(+) = ft .

We know that
Ax£ I» { X 0 » X 0 = X D , ( X 0 . X 1 ) » X 2 = X 0 » ( X 1 » X 2 ) ,

NOW

£>f.|i = ô'.v

p(x0+(3^).X1)=X0) =

X Q . C X Q ^ ) ^

.

N 18
We hâve to show

Axï V* x^Cx^Stx^^L.

x0»(x0*x1)«(x0*x0)*x1 = xQ*x1

•

and therefore

xoa(xQ»x1) = x Q .
Similarly for the other éléments of Ax2 •
Proof of (b).
The proof i s based on t h e f a c t t h a t
T l ^ A x ^ « Th(Ax 1 U { X Q + X ^ Q <

> Xg+x-^x^ > •

QED
End of Examples.
Définition 7.
Let a

be any ordinal. The class

Lf

of Cylindric Algebras

was defined in the monograph Henkin-Monk-Tarski (71). Hère Lf
is ccusidered a category the usual way;
The objects of

Lf

morphisms of Lf
Lf

are the cylindric algebras

Lf

and the

are the homomorphisms between algebras in

„
a•

In more détail*
Lf

is defined the following way.

First a similarity type &

of algebras is fixed with

a+2

opérations symbols. Then 8 simple schemes C0-C7 of équations are
postulated. Then
of type

<?

CA

is defined to be the class of ail algebras

satisfying the équations C0-C7 • Clearly

CA

is

a variety.
Then

Lf

ç: CA

a

a

is defined as followss

Let

&l Ç CA . Then &^€ Lfa
iff
a
<2£
(N/x € A) Cf€Dom(^»)s € » ( f ) > 0 and f ( x , . . . , x ) i x) i s f i n i t e
I. e. Oiç Lf
iff
OC
( V x € A) f the number of those basic opérations of &L which
x is not a fixed point is finite3

.

N 19
I. e. 01 € Lf
iff
a
( V x € A) £x is a fixed point of every basic opération of OL
with finitely many exceptions\\
By this the class

Lf

of algebras has been defined.

The category Lf
ObLf
~ Lf

is the usual one, namelys

a
-a

-~

a

-sr

Ail the homomorphisms between the algebras in Lf

and
torLf

in the usual sensé•
End of Définition 7.
From the above définition it should be clear that the définition
of

Lf

is much simpler than that of TH*1 , at least for certain

kinds of investigations. Certainly the standard tools of abstract
algebra and universal algebra can be directly applied to

Lf .

Theorem 5.
Let a

be an arbitrary ordinal •

catégories TH** and

Lf

Assume a > ***•* • Then the

are isomorphic in the sensé of

MacLane (71).
QED of Theorem 5.

Parts and some semantic aspects of the above Theorem 5 are illustrated and proved in Németi-Sain (78). See also Andréka-GergelyNémeti (77),(80).

Theorem 5 above can be used to apply the theory of Cylindric
Algebras (CA-theory) to investi^ate the category Tir

of théories

and theory morphisms. Hence CA-theory can be used as a theoretical
foundation for stçpwise refinement of program spécifications
along the lines outlined e. g. in Burstall-Goguen (77),(79),
Goguen-Burstall (78)-(80).

N 20
In the remaining part of this paper we shall concentrate on
the category TH

of ail first order théories and interprétations

between thera. We hâve seen that
category Lf

Tn

is isomorphic with the

of ail locally finite cylindric algebras and their

homomorphisms. Lf

can be defined in a clear abstract style

and nice représentation theorems simplify our work with
We shall prove that

Lf

and

Tir

Lf

.

are strongly algebroïdal

catégories (in the sensé of e. g. Banaschewski-Herrlich (76),
Andréka-Németi (79) ) and they hâve enough projectives, are
complète and cocomplete e t c . Hence the resuit s of category theoretic Uni versai Algebra in the sensé of e. g. Andréka-Németi (79),(78),
Németi-Sain (77) can be applied to TH00

and

Lf

. The strongly

small objects (or compact objects) and projective objects of TKr
and

Lf

will be characteri^ed. TYr

is a locally finitely presented

category in the sensé of Gabriel-Ulmer. Specially ultraproducts
exist in TH0,

and

Lf

. It turns out that ultraproducts of

théories (objects of TIT ) commute with ultraproducts of their
models. I. e. let < T . : i € I >

b e a System of théories and F

be an ultrafilter on

be the ultraproduct of

< T. s i € I >
ÊA

I . Let T

modulo

F

in the category TH0C . Then a structure

is a model of the ultraproduct theory T

ultraproduct of some models < £/L s i € I >
that

(Vi € I) f&l

iff
modulo

&L is an
F

such

is a model of the theory T. 3 . This

resuit extends to reduced products if and only if the cylindric
algebras

Lf

are replaced with cylindric (meet) semilattices.

Parts of the results reported hère are joint resuis of the author
with H. Andréka and T. Gergely.

Références.
ADJ (76)s J. A. Goguen, J. W. Thatcher, E. G. Wagner, J. B. Wright,
Rational Algebraïc Théories and Fixed-Point Solutions, Froc.
IEEE 17th Symp. on Foundations of Computer Science (Houston,

N 21

Texas), 1976, pp. 147-158.
H. Andréka, T. Gergely, I. Németi (72)s Hierarchy of languages for
A.I. , Hungarian Pub. of Central Res. Inst. Phys. Budapest,
No KFKI-72-46, 1972.
H. Andréka, T. Gergely, I. Németi (77)s On Universai Algebraïc
Construction of Logics, Studia Logica XXXVI,1-2 , 1977,
pp. 9-47.
H. Andréka, T. Gergely, I. Németi (80)s Model theoretic semantics
for many-purpose languages and language hiérarchies, Proc.
of C0LINGf80 Tokio, 1980 .
H. Andréka, I# Németi (78); tçis

lenàûa holdd tn every category,

Studia Soi. Math. Hung., To appear.
H. Andréka, I. Németi (79) Formulas and Ultraproducts in Catégories,
Beitrage z. Algebra u. Geom. , 1979, pp. 133-151.
H. Andréka, I. Németi (79a)s Néhany magyarorszagi kutatas a
szamitastudomany maternâtikai alapjai teren, Proc. of the
"NJSZT Elso Orszagos Kongresszusa", 1979.
H. Andréka, I. Németi (79b) s Base horoomorphisms of generalized
cylindric set algebras, Manuscript, 1979.
B. Banaschewski, H. Herrlich (76)z Subcategories defined by
implications, Houston J. of Math., 1976/2 , pp. 149-171.
J. L. Bell, M. Machover ¢77)s A course in Mathematical Logic,
North-Holland, 1977.
E. K. Blum, D. R. Estes (77)g A generalization of the homomorphism
concept, Alg. Univ. 7 , 1977, pp. 143-161.
E. K. Blum, N. A. Lynch (79a)s A différence in expressive power
between flowcharts and recursive schemes, Math. Syst. Theory
12, 1979, pp. 205-211.
E. K. Blum, K. A. Lynch (79b)Î Relative complexity opération sets
for numeric and bit string algebras, To appear in Math. Syst.
Theory.

N 22
R. M. Burstall, J. A. Goguen (77): Putting théories together to
make spécifications, Proc. of 5th Int. Joint Conf. on
Artificial Intelligence, MIT, Cambridge, Mass. , 1977,
pp. 1045-1058.
R. M. Burstall, J. A. Goguen (79)§ Some Fundamental Properties of
Algebraïc Théories? A Tool for Semantics of Computation,
accepted by Theoretical Computer Science.
C. C. Chang, H. J. Keisler (73): Model Theory, Nerth-Holand, 1973.
B. Domolki (79): An example of hierarchical program spécification,
to appear in Proc. Abstract Software Spécifications, Jan.
1979, Copenhagen, Ed. D. Bj^rner and C. Jones.
C. C. Elgot (71)§ Algebraïc théories and program schemes, Symp.
on Semantics of Algorithmic Languages, éd. E. Engeler,
Springer-Verlag, 1971, pp. 71-88.
C. C. Elgot (75): Monadic computation and itérative algebraïc
théories, IBM Res. Report RC 4564, Oct. 1973

and Proc.

f

of Logic Coll. 73, North-Holland, 1975, p. 230.
J. A. Goguen, R. M. Burstall (78)g Some fundamental properties of
algebraïc théories: A tool for semantics of computation, preprint 1978, submitted to Theor. Comput. Sci. •
J. A. Goguen, R. M. Burstall (79): CAT, a System for the structured élaboration of correct programs from structured spécifications, in préparation.
J. A. Goguen, R. M. Burstall (80)s The semantics of CLEAR, a
spécification language, to appear in Proc. of 1979
Copenhagen Winter School on Abstract Software Spécifications.
G. Gratzer (79)s Universai Algebra, 2nd Ed., Springer-Verlag, 1979.
L. Henkin, J. D. Monk, A. Tarski (71): Cylindric Algebras Part I,
North-Holland, 1971.
L. Henkin, J. D. Monk, A. Tarski (79): Cylindric set algebras and
related structures I , submitted to Alg. Univ. .

N 23

H. Herrlich, G. E. Strecker (73): Category Theory, Allyn and
Bacon Inc. , Boston, 1973.
S. MacLane (71): Catégories for the Working Mathematician,
Springer-Verlag, 1971.
J. McCarthy, P. J. Hayes (69): Some philosophical problems from
the standpoint of artificial intelligence, Machine Intelligence
4, 1969.
J. D. Monk (76): Mathematical Logic, Springer-Verlag, 1976.
P, Mosses (79): Modular Denotational Semantics, Rep. of the 2nd
Int. Workshop on the Semantics of Programming Languages,
presented in the Rundbrief d. Fachgruppe Kunstliche Intelligenz
in der Gesellschaft fur Informatik, No. 17 , 1979, pp. 50-51,
pub, P. Raufels (Instit. fur Informatik III, Univ. Bonn,
Kurtfurstenstr. 74, 5300 Bonn 1 ) .
I. Németi, I. Sain (77)s Cone-injectivity and some Birkhoff-type
theorems in catégories, contributions to Universai Algebra,
Proc. Coll. Esztergom, 1977, Colloq. Math. Soc. J. Bolyai,
Noth-Holland, 1981.
I. Németi, I. Sain (78): Connections between Algebraïc Logic and
Initial Algebra Semantics of CF Languages, to appear in Proc.
Coll. Logic in Programming, Salgotarjan, 1978, Colloq. Math.
Soc. J. Bolyai, North-Holland.
C. M. I. Rattray, T. Rus (77): Hash-Hierarchy, a mathematical device
for computer system modelling, Proc. lst Symp. on Math.
Modelling, Missouri, 1977, pp. 1-15.
I. Sain (79b)s Théories, Theory Morphisms and Cylindric Algebras,
Manuscript, 1979.
J. Tiuryn (79a)s Connections between regular algebras and rational
algebraïc théories, Proc. 2nd Workshop categorical and algebraïc methods in comp. sci. and syst. theory, Dortmund, 1979.
E. G. Wagner, J. B. Wright, J. A. Goguen, J. W. Thatcher (76):

N 24

Some fundamentals of order-algebraïc semantics, IBM Res. Rep.
RC 6020, June 1976 and Proc. of 5th Int. Symp. on Math.
Found. of Comp. Sci. , Gdansk, Poland, LNCS 45, pp. 153-168.
E. G. Wagner, J. W. Thatcher, J. B. Wright (77): Free continuous
théories, IBM Th. Watson Res. Cent., RC 6906, 1977.
M. Wand (75a)§ Fixed-point constructions in orderenriched catégories, Techn. Rep. 23, Comp. Sci. Dept., Indiana Univ., Apr.
1975, to appear in Theor. Comput. Sci., 1979.
M. Wand (77a)s Algebraïc théories and tree rewriting Systems,
Techn. Rep. No. 66, Comp. Sci. Dept., Indiana Univ.,
Bloomington, Indiana 47401, 1977.
J. Winkowski (78): Towards an understanding of computer simulation,
Ann. Soc. Math. Pol., Séries IV: Fundamenta Informaticae I,
1978, pp, 277-289.