D IAGRAMMES

S EYED -K AZEM L ELLAHI
N ICOLAS S PYRATOS
Deduction over graphs under constraints : a soundness
and completeness theorem
Diagrammes, tome 29 (1993), exp. no 2, p. LS1-LS24
<http://www.numdam.org/item?id=DIA_1993__29__A2_0>

© Université Paris 7, UER math., 1993, 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

VOLUME 29,1993

DEDUCTION OVER GRAPHS UNDER
CONSTRAINTS: A SOUNDNESS AND
COMPLETENESS THEOREM
Seyed-Kazem LELLAHI
e-mail: kl@lipn.univ-parisl3.fr

LIPN, URA 1507 du CNRS
Université de Paris 13, Institut Galilée
Av. J.B.Clément, 93430 Villetaneuse, France
Nicolas SPYRATOS
e-mail: spyratos@lri.fr
LRI, URA 410 du CNRS
Bât. 490, Université de Paris 12
91405 Orsay Cedex, France

Abstract
We introduce a notion of compilation and a notion of constraint over graphs, and we give
an inference system for deducing new compilations or constraintsfromold. The graphs and the
inference rules are interpreted in suitable enriched catégories, which allow to define the model of
a graph under constraints. We prove that our inference system is sound and complète.
Keywords: Categorical Semantics, Categorical Logic, Enriched Catégories, Graph-Based
Modelling of Knowledge, Algebraic Spécification-

1

INTRODUCTION

In advanced computer applications, such as multimédia applications, entities
of différent Systems must cooperate together. Thèse entities hâve usually différent
représentations and organizations, and they may corne from a functional, or a
logic, or an applicative or an object-oriented programming language as well as
from a data or a knowledge base. As a conséquence it seems necessary to hâve a
uniform représentation of ail kinds of entities at conceptual level. Indeed such a
représentation makes easier interfacing of the Systems concerned on the one hand,

A.M.S. SUR CLASS. : 18 C10 ,68 C 9 9 , 1 8 D 20

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

and the compréhension of the behavior of the whole system on the other hand. In
any case, in order to answer user queries, the system must be able to combine old
entities of various kinds to deduce new entities. Therefore, the uniform
représentation of entities should be equipped with constructs such that their
instantiation in a given system provides constructs of that system.
In récent years the database community and the knowledge base community
hâve been faced with this kind of problems. Some researchers hâve argued that at
conceptual level data should be structured as graphs, and several graph-based
models hâve been proposed recently [CoMe90], [GPV90], [Wedd92], [VaVa92],
[KaVa93]. Others hâve proposed second order signatures as a modeling tool
[Guti93], and some authors hâve tried to use category theory for such a modelling
[TGP91], [TuGu92]. In [LeSp93,92,91] we hâve proposed a data model in which
the conceptual level is presented as a graph with constraints and in which data are
organized as partial/mutivalued functions, or more generally as morphisms of a
spécial category. However, the approach of [LeSp93, 92, 91] is a model theoretic
approach. In this paper we présent a proof theoretic approach by introducing a
system of effective inference rules, and we show how the déduction process,
constructs a free adjoint functor. We prove soundness and completeness of the
rules using the properties of enriched catégories [Gray74], [Kelly82], [PoWe92]
and the Yoneda Lemma [MacL71], [BaWe90]. This may be seen as the main resuit
of the présent paper.
The rest of the paper is organized as follows. In Sections 2 we présent the
notion of semantic universe and semantic fonction: a semantic universe is a V category, and a semantic fonction is a V-fonctor [Gray74], [Kelly82], when V is
a category of spécial posets called well-behaved posets. In Section 3 we introduce
the basic concepts of graph and interprétation of a graph in a semantic universe.
We give a syntactic way that constructs a semantic universe over a graph. The
arrows of this semantic universe are called computations. We prove that the
'meaningfor computations with respect to a given interprétation for a given
graph is a free construction in a comma category. In Section 4 we define the
notion of constraint on a graph. Constraints are déclarations of the form p^e,
where p is a path and e is an edge, which must be enforced between computations.
We présent a set of inference rules which operate on a graph with constraints.
Computations obtained by thèse rules are called computations under constraints.
We introduce a notion of constraint satisfaction, a notion of model and a notion of
constraint implication and we prove that the inference rules are sound and
complète. This is the main resuit of the paper. In Section 5 we consider
interprétations which are not models but are consistent with the constraints. Such
an interprétation générâtes a canonical model and we prove that his model is
constructed as a least fixpoint. We call this least fixpoint the fixpoint semantics.
Finally, in Section 6, we offer some concluding remarks and suggestions for
further research.
LS 2

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS .

2 SEMANTIC UNIVERSES

A subset of a partially ordered set (poset) is said to be consistent if it is
bounded. A well-behaved poset, or wposet for short, is a non empty poset in
which every finite consistent subset A has a least upper bound, denoted lubA. In
particular, the empty subset has a least upper bound called the zéro of the wposet
Clearly every upper semi-lattice is a wposet. A morphism between two wposets is
a fonction which préserves consistency and lub. That is f is a morphism of
wposets if for every finite bounded subset A, of the source of f, the subset f(A) is
bounded, in the target of f, and lub(f(A)) = f(lubA). An équivalent way is to say
that f is a morphism of wposets if f préserves zéro and whenever (a, b] is
consistent so is (fa, fb) and f(lub[a, b)) = 1ub(fa, fb). Such a fonction f is
monotonie. The category of small wposets is denoted by WS>. It is easy to see that
this category is finite complète and finite cocomplete. Moreover, limits and sums
in WP can be computed pointwise.
Définition 1 A t^iP-category [Gray74], [Kelly82] is called a semantic universe. o
In fact, semantic uni verses are spécial 2-categories [PoWe92]. More
precisely, given an arrow u . A -* 6, call A the source of c/, denoted src(u), and B
the target of c/, denoted tgt(u). Now, the category C is a semantic universe if
• for ail objects A and B the set G(A, B) of arrows1 from A to B is a wposet; the
zéro of this wposet is denoted 0(A, B),
• 0(tgt(u), A)u = 0(src(u), A), and uO(A, src(u)) = 0(A, tgt(u)), for every
arrow u and every object A,
• for ail arrows x, y, z and t as in the following configuration

if (y, z) is a consistent pair, then so are (yx, zx) and (ty, tz) and we hâve:
- lubfyx, zx) = lub(yt z)x (left continuity)
- lubfty, tz] = t lub (y, z) (right continuity).
Let * dénote the partial ordering over arrows of 6. We can prove that
composition of arrows defines a monotoniefonctionwith respect to the ordering,
that is, in the above configuration:
- if y ï z then yx i zx (right augmentation), and
- if y £ z then ty i tz (left augmentation)
From now on, in a semantic universe we shall write V instead of z. It is
clear that the category *tâP is itself a semantic universe. Indeed, morphisms
1 Ail semantic universes considered in this paper are small or localiy small catégories

LS 3

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...
between two wposets can be ordered pointwise and this ordering satisfies the
above axioms. Other interesting examples of semantic universes are:
• the category $U± of sets and partial fonctions with the usual ordering on
partial fonctions,
• the category mSU of sets and multivalued fonctions with pointwise inclusion,
• the category Sbiel of sets and binary relations with the usual ordering on
binary relations, and
• the category Gp*oî continuous fonctions between complète partial orderings
[GuSc90].
A semantic universe with only one object is a monoid equipped with a well
behaved partial ordering satisfying continuity. More precisely, let M be a set
equipped with an associative product, an identity élément e and a partial ordering
V such that:
• there is an élément e of M, called zéro, satisfying e $m and em = me = e for
ail m in M,
• for ail éléments m, and m2 if there is m3 such that m, * m5 and m2 * m j, then
1ub(mh m2) exists, and
• if lub(m h m2) exists then so does lub(m5m h m5m2), for every m3 in M, and
1ub(mj, m2)m5 = lub(m jm2,m ^m3) and
mjlub(mh m2) = lub(m5mu m5m2)

A sub-category & of a semantic universe Gis called a sub-semantic universe
of G if & equipped with the restriction of the ordering of G becomes a semantic
universe.
A semantic universe G being a 2-category, G contains three category
structures which cooperate together, as sated for gênerai 2-categories in
[PoWe92]. Thèse three catégories are:
The base category G, whose class of objects will be denoted G0 and whose class of
arrows will be denoted Gh
The vertical category, defined by the ordering f 4 f of G, whose objects are ail
éléments of G, and whose arrows, called 2-cells, are pairs of parallel arrows f, g
such that f $ g. Such a cell is seen as a vertical arrow from f to g, and the vertical
composition is defined by the transitivity of the ordering. That is (f * g).(g * h) =
(f $ h) corresponds to: if (fig and gib) then fi h. Moreover, in this category the
coproduct of two objects f and g, when it exists, is lub(f, g). So, we use f e gas
an alternative notation for lub(f, g).
The horizontal category, whose class of objects is G0, and whose class of arrows is
the class G2 of ail 2-cells. A 2-cell f $ gis seen as a horizontal arrow from A to B
where A is the common source and B is the common target of parallel arrows f
us 4

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

and g. The horizontal composition is the composition in the category GxG, that is
(h * k)o(f * g) = (hf * kg) if and only if src(h) - tgt(f) and src(k) = tgt(g).
Thus, in a semantic universe, any pair a = (f, g) of arrows such that f * g, may be
seen as a vertical or a horizontal arrow. We adopt the notation of [PoWe92] and
we write a : f + g when a is seen as a vertical arrow, and we writeaf* g.A ->6
when a is seen as a horizontal arrow.
The interaction between thèse three catégories is expressed in the following well
known proposition:
Proposition 1 In a semantic universe G, for ail configurations of objects,
arrows and cells as in Figure 1, the following holds:
interchange law:

(P'oa').(poa ) = (p'.p)o(a'.a). o

Figure 1
> C

Intuitively, a morphism between two semantic universes is a functor which
préserves at least ail thèse three structures. More precisely:
Définition 2 A «MP-functor [Gray74], [Kelly82] is called a semantic function. o
Thus, semantic fonctions are spécial 2-fonctors. More precisely a functor /
from a semantic universe Gto a semantic universe G' is a semantic fonction if the
following holds:
• l(0(A, B)) « 0(1 A, IB) for ail objects A and B, and
• for ail parallel and consistent arrows a and b in G, the arrows la and Ib are
consistent in C'and l(a e b) = la e Ib.
It is clear that such afonctoris monotonie. We dénote by &m the category whose
objects are ail locally small semantic universes and whose arrows are semantic
fonctions.

3

COMPUTATIONS OVER A GRAPH

Graphs
In this paper, by graph we mean a directed labelled multigraph. An edge
from node / to node J with label e is displayed as e ; / -* J, or / -£-» J or leJ.
The node / is called the source of e, denoted src(e), and the node J is called the
LS 5

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

target of e, denoted tgt(e). We assume that edges hâve distinct labels. A séquence
(e h e2,..., en) of edges in a graph G, is called a G-path of length n, if tgt(ej) =
src(eh f) for every /, UHn- /. We dénote such a path by ete2...en. Morphisms of
graphs are defined as usual, and the category of locally small graphs is denoted by
Computations
Given a graph G, we apply the recursive inference rules, of Figure 2 on G to
obtain what we shall call G-computations. In thèse rules, a computation cp from A
to B is denoted <p : A —~-> B, and

means that " in any context, if we hâve already a premise O then we can construct
the conséquence *F.
Figure 2 :

(edçe)

Inclusion
e :

src(e)-

identity

tqt(e)

(note)

Product

y; A

Addition

y; A-

Parenthesis

_£

<p : A

id(A):Ay; d
<p.y: A
y; A-

ifi-

q>+y/: A—**

B

JSL

.&l;A; • e
g (notes)

zéro

zeroCAB): A •

If we regard src, tgt, id, '.' and '+' as opérations, then G-computations can be
seen as terms obtained by applying thèse opérations on the symbols representing
nodes and edges of G. A G-computation of the form e, e2...en where ail e ; are
edges is identified with the path e]e2....en. A G-computation of the form id(A) is
seen as a spécial G-path of length 0 associated with A. Thus, there are several
paths of length 0, one for each node. From now on by G-path we mean a path of
length 0, or a path of positive length. Two G-computations are said to be parallel
if they hâve common source and common target.
Note: It is important to note that ail the above rules are syntactic rules. A
computation may be seen as a program, and this is the reason why we dénote the
product of two consécutive computations <p : A ——> B and y/ : B —~» C by q>.y/
and not by y/.<p (which is the usual notation in a category).
Equivalent Computations
Let P/, p2,... , pnbe parallel G-computations with source A and target 6. We
say the G-computation p, +p2+... +pn is a G-expression if each p, is either a G-path

LS 6

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS ...
or the G- computation zero(A, B). In particular, every G-path is a G-expression.
We shall see that expressions are canonical forms of computations.
Now, with every G-expression e from A to 6 we associate a set A(e) of
parallel G-paths, from A to B, as follows:
• Mzero(A, B)) = 0,
• /6(p) = (p), for every path p, and
• Me+e') = /6(e)u/6(e'), for ail parallel G-expressions e and e'.
The particularity of the set Me) is that it is a set of parallel paths, so it contains at
most one computation of the form ld(A) and no computation of the form zero(A, B).
We can extend the fonction /6 to ail G-computations using the following rules,
where the extension is denoted M.
For every expression e, ail parallel computations (p, <p', ail computations y/, and
ail edges f with src(f) = tgt(ç) = src(yf), define:
• M(e) = Meh
• M(((p)) = M(<p.id(src((p))) = M(id(tgt((p)).ç) = M((p\
• M((p+ç') = M((p)vM(<p'),
• ^Vçi f) - U g M w ^Vflf. O, and

• M(<p.yr) = u / M ^*r<p.a
Définition 3 Two G-computations ç> and i/fare said to be équivalent, denoted ç
s y/, if they are parallel and /4 Yçtf =J*(yt). o
For instance,/+/s/and/+g s g + / Similariy,/+g+zer0fsrc(/;, *£*(/),) s / + g , and
so on. The following proposition is an immédiate conséquence of définitions.
Proposition 2 The relation s is a congruence relation for the opérations src,
tgt, zéro, \ \ '+ ' and parenthesizing. That is, s is an équivalence relation and:
• if (p s yfthtn src(ç) = src(y/) and tgt(ç) - tgt(yf), for ail parallel
G-computations (p and y/,
• if (p s yf then (<p) s (yr), for ail parallel G-computations <p and y/;
• if (p s ynhen (p + £ s y/ + £, for ail parallel G-computations <p, yf and £
• if (p s y/then ç.Ç = y/.Ç and p.<p = p. yr, for ail parallel G-computations (p, y/,
and ail G-computations p and Ç such that y>.£, y/:£, p.<p and p. y/" are well
defined. o
Let us dénote by [ç] the équivalence class of a G-computation ç>. Using the
above proposition, the opérations [id], [zéro], [src], [tgt], [.] and /+7 can be defined
on équivalence classes of G-computations as follows:
• [IdKA) = [id(A)]f [zeroKA, B) = [zero(A, B)],
• (src]((p) = src(cp), [tgt]((p) = tgt((p),
• [<p][.][yr] = [ç.yr] and
• [<p][+]fy]=[<p+yrL
LS 7

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...
Moreover, équivalence classes of G-computations can be ordered by:
[<p] i [çf] if and only if M(ç) c M(<p')
That is, [<p] ï [ç'J if and only if ç + y>' e (p1. Moreover, /y>+ç>7 - 1ub([q>], [<p'D,
for ail computations <p and <p\
For simplicity we dénote the opérations [id], [zéro], [src], [tgt], £7and/+7by ld,
zéro, src, tgt, '.'and +',respectively.
Proposition 3 The équivalence classes of G-computations equipped with the
opérations zéro, id and '.' , and the ordering %i% form a semantic universe,
denoted cG.
Proof The objects of cG are the nodes of G, the arrows of cG are ail
équivalence classes of G-computations, and the composition of arrows is defined
by:
[y/][(p] = [<p][y/] if and only if src(ys) = tgt((p).
The rest of the proof is obvious, but tedious, using the properties of union on sets
and the définitions of /6* and s. o
The fonction that associâtes each graph G with the semantic universe cG
defines a functor cfromthe category tjt, to the category «&m. However, c is not a
left free adjoint to the forgetfol fonctor U : Svm,—> tjt,. That is, there may exist a
graph morphism / from G to a semantic universe G which cannot be freely
extended to cG as a semanticfonction.Indeed for a computation <p which uses the
addition rule, l(<p) may be 4meaningless' in the semantic universe G. However, we
shall prove in the sequel, that / can befreelyextended to a suitable sub-semantic
universe of cG.

The Meaning of Computations
Recall that the ordering of a gênerai semantic universe is denoted '=>' and its
lub opération is denoted '•'.
Définition 4 Given a graph G, we say (G, I § ) is an interprétation of G, if C is
a semantic universe and S S is a graph morphism from G to UG. o
When G is given, U // is called a G-interpretation of G. Intuitively, for every
node/edge x of G, //x^ is the meaning of x in the universe of discourse G. Now,
the important question is: Can // § be extended to ail G-computations ? The answer
to this question dépends on the semantic universe G. For example, let G be the
graph with only two parallel edges e and e ', and let // // be an interprétation of G
in the semantic universe su± (i.e. the universe of partial fonctions). Suppose that
the greatest lower bound of thefonctions//e // and fle 'Il does not exist. Then e+e '
is a G-computation, but II II cannot be extended to e+e '. However, if we consider
LS 8

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...
g B as an interprétation in the universe of multivalued fonctions, then II can be

extended to e+e'by ll(e^e'Xx) = le(x)lule'(x)l,

for every x in

src(lej).

This example shows that, given an interprétation 11 of a graph, / I cannot
necessarily be extended to ail computations. We call those computations to which
I I can be extended meaningful computations with respect to I / . This partial
extension of II, denoted Um, is defined as follows:
Définition 5 Given an interprétation 11 of a graph G,
• every G-node or G-edge x is meaningfol and lxlm = /xI,
• id(A) is meaningfol and I id(A)lm = id(lA I), for every node A,
• every G-path p = eje2...en of positive length is meaningfol and
IPL=
lenl...le2llejl,
• zero(A,B) is meaningfol and lzero(A,B)lm = 0(1 Alm, lBlm), for ail nodes
A and 6, and
• a G-expression e = p, + p 2 + ... +Pn is meaningfol if //p, lmelp2Bm°
••*IIPnL exists in G, and then //e// m = //p, Hm*ip2lm* ... °BpnBm- <>
Note that when the meaning fonction I Bm is applied to a path p = e ; e2... en it
reverses the order of edges in the path.
It follows from this définition that ail équivalent G-expressions hâve the
same interprétation (if one exists). Now, let y>be a G-computation, let M(ç)=
(P\> P2> -> Pnh and let eç = p ; +p2 + ... +p n . Moreover, let eoq> =
PG( /ri>G(2)+ .+Parn> where cry> stands for a permutation of the indices /, 2, ...,
n in eç,. Since e,, and eaç, are équivalent, if leçlm exists then Iea<pBm exists and
//eç)//m= BeG<plm. The expression e^ is called the canonical form of ç. Now, we
can define the meaning of a computation as follows:
Définition 6 A computation (p is said to be meaningful, with respect to an
interprétation 11, if ^ e ^ is defined; otherwise (p is said to be meaningless. If <p
is meaningfol, then leçlm is called the meaning of y), o
For example if a, P and c are edges then (a+b).c is meaningful if and only if

h-clm*lb.clM=

Ibllalelcllal

exists. Moreover, l(a+b).clm

=

IbB lai*Ici
lai. We note that (a+b).c may be meaningfol while (a+b) may not
be meaningfol.
It is not difficult to prove that:
• if y> is meaningfol and (p s q>' then ç' is meaningfol and l<plm = I<p'Bm,
• if (p and <p' are meaningful and (p. ç' is defined then y>. <p' is meaningful and

h-<P'IL=

h'ijçiïwznd

• if <p and y>' are meaningful and if ll(plm* l<p'lm is defined then <p+ç' is
meaningful and lq>+ç'lm = lq>lm*fo'lm.
Thus we can state
us 9

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...
Proposition 4 Let G be a graph. For every interprétation (G, II) of G, the
équivalence classes of meaningfol G-computations, with respect to 11, form a
semantic universe mG which is a sub-semantic universe of cG. Moreover, I lm is
a semantic fonction from mG to G. o
We shall prove that the semantic universe mG may be seen as a free
construction over (G, II). Let us consider a category & m l in which the objects
are semantic universes, and morphisms from Cto G1 are fonctors / such that the
following holds:
• / préserves zéro, and
• for ail parallel arrows a and P in C, if laeib exists in C then a*b exists in G
and l(a e b) = la 0 Ib.
It is easy to prove that the semantic fonction I lmis also a morphism of
Seml. A morphism / : G -> G' of Seml is not necessarily a semantic fonction nor a
monotonie fonction. However, if a $ b and laolb exists (for instance, if la and Ib
are consistent) then la *¥ Ib. Again we hâve a forgetful functor V : Seml -> ^*v.
Let us dénote by j^t/Cthe category of objects over VG [MacL71]. An object of
tji/Gis a pair (G, II) where 11 is a (^-interprétation of G. An arrow of $i/G
from (G, 11) to (G', 11') is a graph morphism F : G -> G' satisfying //Fx//' =
llxl, for every node or arrow x in G. We define Seml/G similarly, replacing
graph morphisms by morphisms of Seml. The forgetful functor V defines a
forgetful functor l//efrom Seml/G to $i/G.
Theorem 1 Let G be a semantic universe. The fonction that associâtes each
object (G, 11) of $i/G with the object (mG, //1^) of £emï/£, defines a functor
™/C : §x/G -> Seml/G which is a left free adjoint to V/G : Seml/G -» §i/G.
Proof Let rjc : G -> V(mG) be the inclusion graph morphism. As 1/(7/ llm^c =
Il //, so 7]G is an arrow of $t/G from (G, // JO to V/G(mG, // // m ; = M m G ; ,
W l llm)). We shall prove that î]G is the unit of an adjunction. The notations in the
proof are referred to Figure 3. In this Figure, dotted Unes represent objects and
other Unes represent arrows of the catégories §t/G or Seml/G.
Let (&, T) be an object of Seml/G and let F : G-> V& be an arrow of §i/G
from (G, 11) to V/G(G', T) = (V(ff)9 V(T)). Let y) be a meaningfol computation
with canoical form e« = p , + p 2 + ... + pn. Thus, J ' y ) ^ = //e<p//m =
Wpi\\m*le2Bm*
... *IPnlm exists in £ If p/ = e;7 ei2....ein(t define p,* =
« e l n / ; F(eh)F(eiE). As 1/<TJ>F - | # wehave WDp/* - / / e , n / . J e , 2 / / / / e , J «
//p,// m . So //y>//m = W D p , * e ... e V(T)pn* = Tp1*e ... e Tpn* We conclude
that the arrow y>* = p ; * e ... e pn* exists in C'and 7Yy>*,) = Tp ; * e ... e 7p n *
(because 7 is a morphism of Seml). If we define Wy>J = ç* then H is an arrow of
Seml/G as it satisfies TH = // //m. Moreover, the équation V(H)ric = F is satisfied in

LS 10

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS ...

tjt/G and H is the unique arrow of Seml/G satisfying this équation. This complètes
the proof. o
Figure 3 r

mC

>V(mG)

u-'

vl Im)/!

x*

Seml/Cv m/?r
Initial Semantics An immédiate conséquence of this adjunction is the
following: Consider the category of V-objects under (G, II) [MacL71]; an object
of this category is a pair (F, (G', T)) where (G', T) is an object of Seml/G and
F ; (G, H) -> V/G(G', T) is an arrow of $i/&, an arrowfrom(F, (&', T)) to
(F', (G", T')isa semantic fonction H satisfying F(V(H)) = F'. In this category the
object (r\c, (mG, I lm)) is an initial object. Therefore, we may call (mG, // lm) the
initial semantics of (G, II).

4

COMPUTATIONS UNDER CONSTRAINTS

Inference Rules
Informally, constraints are 'relationships' that must be enforced on
computations and the question is: what is the effect of constraints on computations
? In other words, how do we compute under constraints? In this section we answer
this and other related questions.
Définition 7 A constraint over a graph G is any statement of the form <pi(p\
where (p and ç' are parallel G-computations and <p * <p'. A spécification G\K
consists of a graph G and a set K of constraints over G (usually G and K arefinite). o
Intuitively, a spécification G\K is a graph G under constraints K, so G\K can
be read "G such that K1'. In order to extend the results of the previous section to
computations under constraints we restrict our attention to a spécial class of
constraints, called edge constraint, Such a constraint has the form m e, where n is
a path called the body of the constraint, and e is an edge called the head of the
constraint. From now on constraints in a spécification will be edge constraints.

us u

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS.«

Given a spécification G\K we define G[K-computations and their preordering,
denoted iK using the recursive inference rules shown in Figure 4. It is important
to note that G|/C-computations and their preordering iK are defined
simultaneously.
Figure 4:

Computation
Inference rules
(edçe)

Constraint Inference rules

me

Inclusion

(constraint)

K:

e

**K

id(A):A-

Transitivity
(and Product)

S&K-

Addition

JS^KIÂ

y;A-~ïd
v;B<p.y/ : A — ^ C

9*K*0

+

<p yf*K

0

JXXÏ8L

ll&K*Q
+

Q*K P V

V*K

+

P V

ç+y/:

Parenthesls

Jt&K-fL

src(O)—*
ç; A

Zéro

tgt(<p))iK

zero(A,

ç

B)- A — »

X(node)

JSL.
zero(X,

tgt(O)

LÊ.

B
(<p). AA
B (nodes)

JBLzero(src(<p),

Augmentation

tgt(e)

src(e)-

(node)

Reflexivity
(and Identity)

src(<p))ç£K

zero(X,

g>

X (node)

<pzero(tgt(<p),

XhK*zero(src(<p),X

J&LKOJIL.

Ê;WW-

tgt(ç))

)

<P-&K*V'Ç
&.K*UL-

JL:

A—ÏSCÇ(Ç)

p.<piK*PV

Distributivity

ÙBIML

E: tçt(a>)-

(ç+\lf).Ç£K
(ç+y)

ç.ç+y.ç

Q;A

p.(<p+yr)£K

srç(v)

PV+PV

We note that ail G-paths and, in particular, ail G-edges are G\Kcomputations. Thus the G-computations used in edge constraints are already G\Kcomputations. We also note that the opération '*'of G|/<-computations is a
restriction of the opération '+' for G-computations. Indeed, the application of '+'
is now conditioned on the existence of a bound for the operands.
We use the notation K>-y>'*y> (read K infers (pop' ) as an alternative notation
for <piK<p'. In fact çiK(p' means that <p and <p' are G|K-computations and the

LS 12

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

constraint <p*ç' is deduced from K using the inference rules of Figure 4. Given
two sets of constrains K and K' over G, we write K H K' if K h- k for every k in K'.
Now, two G|/<-computations (p and y>' are said to be équivalent, denoted y> &K<p\
iff <p*Kç' and (p'ïK<p- We extend the relation &K as follows:
(p sK((p) sK id(src(<p)).ç sK (p. id(tgt(ç)), for every G|/C-computation (p.
One can prove that this extended relation sK is actually a congruence relation and
has ail properties seen earlier for the relation s. Therefore, the opérations src,
tgt, '. ', zéro and id can be defined on équivalence classes of G|K-computations.
Thèse opérations hâve the same properties as in Section 3. For example, from the
addition rules, the opération V is idempotent and product is distributive with
respect to addition. Moreover, the preordering *K induces an ordering on parallel
G|K-computations, denoted iK, which has also the same properties as the ordering
i defined earlier on G-computations. In particular, [q>] iK [ç'1 if and only if
[<p] + Iç'] =K l(p'h i.e. if and only if <p + <p' sK cp\ In view of the above rules and
définitions, Proposition 4 can be extended as follows:
Proposition 4 (continued) The équivalence classes of G|/<-computations
equipped with the opérations zéro, id and '.', and the ordering %ïK ' form a
semantic universe, denoted cG\K. o

The meaning of Computations under Constraints
Clearly, every G|/<-computation is a G-computation. Thus as in the previous
section one can define the meaning of a G|/<-computation with respect to an
interprétation (G, // //; of G. We recall that not ail G-computations are necessarily
meaningful, and thus not ail G|K-computations are necessarily meaningful. We
also recall, however, that two meaningful and équivalent G-computations hâve the
same meaning. This unfortunately, is not always the case for G|/<-computations,
i.e. two meaningful and équivalent G|/<-computations may hâve différent
meanings. For example let G = Set± and K = (eiel, where e and e' are edges. The
computation e+e' is a Gl/<-computation obtained by addition and reflexivity rules.
Now, if lubdlel, le'I) exists in G, but lub(hl, Ile'II) * le'B then le+e'lm=
lub(Hel, Ile'H) *le'l = lle'lm. However, e + e'and e' are équivalent G\Kcomputations.
So the effect of constraints on computations is that the constraints may cause
violation of our basic requirement, i.e. that two meaningful and équivalent
computations must hâve the same meaning. Clearly, this is an undesirable

LS 13

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS ...

situation, and in what follows we characterize interprétations in which équivalent
G|K-computations do hâve the same meaning, if they hâve a meaning at ail.
Définition 8 Given an interprétation (G, 11 ) of a graph G, we say that
• (G, 11) satisfies the constraint <p i ç', denoted II hs y*y>'> if <P and y>' are
meaningful with respect to (G, 11) and l<plm * l<p'lm,
• (G, I f) satisfies a set K of constraints, denoted / / Hc K, if (G, II) satisfies
every constraint in K, and
• (G, ll)isa model of the spécification G\K if BI he^ o
To simplify matters we shall drop the index G when no confusion is possible.
Clearly, in the absence of constraints, every ©-interprétation of G is a C-model of
G. Note that if /r = e ie2-..en is a path then n is meaningful and lnlm=
lenl len-jl... lej. Thus, (G, /JO satisfies the edge constraint me if
InI $ leI. A spécification G\K has always at least one C-model, namely, any
interprétation / such that l(e) = 0(src(le), tgt(le)) for every edge e présent in K,
is a model of G\K. Suchfî-modelsare called trivial ©-models. From now on by Gmodel we mean a nontrivial ©-model.
Let K be a set of constraints and let k be a constraint, which may or may not
be in K. We say that K implies k denoted K |= k, if every interprétation which
satisfies K also satisfies k. Given two sets of constraints K and K' over G, we say
that K implies K', denoted K H K\ if K implies every constraint in K".
Theorem 2 The constraint inference rules of Figure 4 are sound and complète.
That is, for every spécification G\K, if k is a constraint over G then K |= k if and
only if K h k.
Proof Note that soundness means that the conséquences of any constraint
inference rules are implied from its hypothèses. Let (G, 11) be an interprétation
which satisfies a set of constraints K. Clearly the inclusion rule is sound. Since 4 is
an ordering in the semantic universe, reflexivity and transitivity rules are sound
too. To prove the soundness of addition rule, assume y>, y/ and 0 to be G\Kcomputations and assume <p iKQ and \\fiKQ to be satisfied, and prove that (p+y/ïK6,
y)^y>+yf and \ffiK(p+\ff are satisfied. The assumption means that <p, yf and 6 are
meaningful and //<p//m^//0//m and ly/lm* llQllm in G. Thus, M/mW/W/m exists in
G, llç/Loly/IL* BOlL, BçlL* IçB^llylLznd //^ m ^y>// m ^/W/ m .Thus,itis
enough to prove that //<p//mW/ yf m = //y>+y//m- w ^ h earlier notations we can write
f Ç* W/m = I v ^ m . //W/m = h Jim ™d Mm = / / ^ L - B u t / / « W ^ & the sum of
paths in ^(qn-yr). Similarly, leçlm is the sum of paths in A*(ç) and //^^//m is the
sum of paths in /6*(y/). As ^(ç+y/) = ^*((p)u/6*(y/) so //<p+y//m differs from
Bçllm0! W/m by a permutation of its terms and by répétition of some of its terms.
But e is idempotent, associative and commutative, so //yn-y/fm = //y>// m W/ y/V/m.
US 14

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

The proof of the soundness of the remaining rules is similar. In fact each rule
reflects a property of the ordering of the semantic universe. Augmentation
reflects the monotonicity of composition, zéro reflects the axiom of zéro and
distributivity reflects continuity.
To prove completeness we show that if a constraint k cannot be inferred from K
using the rules, then there must be a nontrivial model (I, G) which does not satisfy
k. We shall give such a model when ©is tâP, using the (enriched) Yoneda's
Lemma [MacL71] as follows:
Let X be a node in G and consider the graph morphism lx: G -> WP defined by :
• for every node A, l/A) = cG\K(X, A), i.e. the well behaved set of ail
equivalece classes of G|K-computationsfromX to A, and
• for every edge u, lx(u) is the morphism from lx(src(u)) to lx(tgt(u)) that
associâtes the class of xu with every class x.
The graph morphism lx is a ttfiP-model. Obviously lx is a nontrivial
interprétation. Moreover, if pie is in K then for every u : X -» src(p) we can
write u.p iKu.e that is, lx(p)(u) <:Klx(e)(u). In other words lx(p)$lx(e) which
means that lx satisfies pie. Now, assume that k = ac' and KM-k. The model
lsrC(C) does not satisfy k, otherwise we must hâve l^(c) ^ lx(c')- This rneans that
/ src ^ c /cXi/^ *KlSrc(c)(c'Xu) or> equivalently,
u.c iKu.c', for every u : src(c) -> src(c).
Taking u = id(src(c)) we must hâve c iKc' which contradicts Kw> k. This complète
the proof. o
Now, we shall prove the soundness and completeness of computation rules.
Let us first define H and 1= notations for computations. We write
K \- (p when y? is a G|/C-computation. That is, y) is a G-computation and cp can be
obtained by afinitenumber of application of computation rules beginning with G
and K. Similarly, K h y> means that y> is a G-computation and y> is meaningful with
respect to every model (G, //1) of K.
Theorem 3 The inference computation rules of Figure 4 are sound and
complète, i.e. for each set K of constraints over G, and for each G-computation y),
K \- (p if and only if K |= ç.
Proof The proof of soundness of computation rules is already contained in the
proof of Theorem 2. To prove completeness we use again the enriched Yoneda's
Lemma. Let y) be a G-computation such that <p is meaningful with respect to
every model (©, //1) of K. We must prove that y) is a G|/<-computation. Let X =
src(cp) and consider the model (*B9, lx) constructed in the proof of Theorem 2.
Thus, lx(<p) is meaningful in V#z>. In particular lx((p)(id(X)) = (p has a meaning in
cG\K, that is K H (p. This complètes the proof. o
US 15

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

Corollary 1 If (G, II) is a model of the spécification G\K then any two
équivalent G|K-computations hâve the same meaning with repect to

(G, II).
Proof

if (G, 11 ) is a model then, by Theorem 2, ail G|/<-computations are

meaningful. Moreover, if <psKy/ then if ç£Ky/ and y^y> then we can write

hlm+Mm*Dà

lvlm*l<ptmSO MmrMwr

Otherwise, yhas the form (<p),

id.<p or (p. id. In ail thèse cases we obviously hâve I y/^m= Içlm.

o

Spécifications are objects of a category Spec. A morphism of Speo from
G i\K j to G^K2 is a graph morphism F : Gj —> G2 such that for every constraint
eie2-.enie in K1 the constraint Fe ^Fe^.-.Fe^Fe is in K2. Let us see a semantic
universe ©as a spécification (not necessarily finite) whose constraints are ail n$ e
where n = e/.e^.-.en is a path and e = en1.en.j....eh As every semantic function
is monotonie, so there is a forgetful functor U : Sem -» Spec. Let us dénote by
Spec/G\hs category of objects over UG and by Sem/G the category of objects over
G. We dénote by G-M*d the full sub-category of Spec/G whose objects are ©models. The functor U defines a functor U/G : Sem/G -> G-M*<£. Theorem 1 and
its proof can now be extended as follows:
Theorem 1 (continued) Let © be a semantic universe. The function that
associâtes each object (G[K, 11) of G-M*d with the object (cG\K, 11^) of Sem/G
defines a functor mK/G : G-M*d -> Sem/G which is a left free adjoint to the
functor U/G : Sem/G -» G-M+d.
Proof Since I // m is a semantic function I //m is a ©-model of cG\K, so
U/G(cG\K, H In) is an object of G-M*A. Let î]^ : G\K -> U(cG\K) be the inclusion
graph morphism. As U(l Bm^qic = // //, so 77 ^ is an arrow of G-M*d from
object (G\K, 11) to U/GfcG[Kf // / / j = U/G(cG\Kt // B J. We shall prove that î]^ is
the unit of an adjunction (see Figure 5, with the same convention as in Figure 3).
Figure 5

%IK

'K
TV

-> tyfcC G \K)

U(H)
\U(T)

#

U<*'

'-

3

....

-T-

.

t

Let (G\ T) be an object of Sem/G and let F : G -> UG' be an arrow of G-M+d
from (G\K, II) to U/G(G', T) = (U(G'), U(T)). Let <pbe a G|/<-computation with

us 16

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS ...

canonical form e^ = p ; + p2 + ... + p„. As BI is a model, y) is meaningful, that is,
l<plm= IPilm0IP2lme ••• e ^Pn im e x i s t s in & As y) is obtained by the addition
rule, there is a computation n such that p, iKn for ail /, /iiin. But F is an arrow of
Q-M+d, so F(pt) *KF(n) for ail /, lit in. This implies that y>* = Ffp ,; * ... * F(pn)
exists in ©\ If we define Hfy>J = y>* then H is a semantic function and defines an
arrow of Sem/G, as it satisfies TH - / ^m. Moreover, the équation U(H)r]G[K = F is
satisfied in G-M&d and H is the unique arrow of Sem/G satisfying this équation.
This complètes the proof. o
Initial Semantics Similarly to Section 3 we can call (cG\K, 11^) the initial
semantics of (G[K, 11) because it provides an initial object in the category of Uobjects under (G\K, II).

5

CONSISTENCY AND FIXPOINT SEMANTICS

Let G\K be a spécification and let B II be an interprétation of G in some
semantic universe G. If B B is not a model of G\K then the question is: should we
discard B B ? The answer is no, provided that // B is consistent with K because, as
we shall prove, a consistent interprétation can be embedded in a model.
Définition 9 Given a spécification G\K, we say that an interprétation
f©, B II ) of G is consistent with K if every G|/<-computation is meaningful with
respect to ////. o
By Theorem 2, every model (G, B II) of G\K is consistent with K.
Proposition 5 Let G\K be a spécification and let (©, // B ) be an interprétation
of G\K. Then f ©, // ^ ; is a ©-model of G\K if and only if
(G, B B ) is consistent with K and any two équivalent and meaningful G\Kcomputations hâve the same meaning with repect to // //.
Proof The 'only if part is expressed by corollary 1 of Theorem 2. Conversely,
assume that // // is consistent and that any two équivalent and meaningful G\Kcomputations hâve the same meaning. Let me be an edge constraint in K. We can
write ezKe by reflexivity, and then by addition rules, e+^is a G|/<-computation
and e+mKeiKe+K.

Thus, e+n sKe and we hâve //e+n/l m = //e// m . That is

# e f m « f * # m « l e f m or, equivalently, Inl^hl^.
me. This complètes the proof. o
LS 17

This means that BB satisfies

DEDUCTION OVER GRAPHS U N D E R CONSTRAINTS ...

Définition 10 Let G\K be a spécification. The derivative of a G-computation (p,
denoted d(p, is defined recursively as follows:
• d(id(A)) = zero(A, A) and d(zero(A, B)) = zero(A, B),

• if y) is an edge of G then if <p is not the head of any constraint in K then d(p is
zero(src(e), tgt(e)) else d<p is the sum of the bodies of ail constraints in K
with head y>,
• if (p = (q>j) then d(<p) = (à<pj),
• if (p = y>/.y>2 then d(ç) = ç j.dç2+(dç\).(p2+d<pi-d<p2, and
• ify> = <Pi+<p2 then <9(y>J = dçj+dç2. o
Now, for every iïO and for every computation (p, define ^/;y> as follows:
d(0>ç = y), <9nV = d(p, dMç = d(da'nç)
*

Lemma 1 If (p is a G|K-computation then so is c/l)(p and d'l)<piK<p, for ail HO.
Proof It is enough to prove the proposition for i' = 1. We prove it by structural
induction. If d(p = zero(src((p), tgt(q>)) then, by the zéro rule, d(p is a G\Kcomputation and d<piK(p. If y) is an edge of G and dy> * zero(src(ç), tgt(<p)) then
y) is the head of some constraint, d(p is obtained by the addition rule and d(p£Kq>.
Now, let y? be a derived G|K-computation such that, for each component e of y>, de
is a G|K-computation and de*Ke (structural induction hypothesis). If (p has the
form u.i/ then du anddv are G|/<-computations and duiKu and dvïKv by the
induction hypothesis. So by augmentation du.viKu.v, u.dviKu.v and du.dviKu.v.
Thus, <?<p = u.dv + du.v + <?u.<?v is a G|K-computation and d(piKu.v = (p, by the
addition rule. Similarly, if <p has the form u + v, where du and dv are G|/<computations satisfying duiKu and <?v:^v, then du <Ku£Kcp and dviKviK(p, sodcp =
du+dv is a G|K-computation and dç£Ku.v = (pby addition rules. This complètes the
proof. o
Définition 11 An edge e in a spécification G\K is said to be non recursive if
there is an integer k ï0 such that dfk+1)e = zero(src(e), tgt(e))\ otherwise e is
called a recursive edge. A spécification with no recursive edges is called acyclic,
otherwise is said to be cyclic. For a non recursive edge e the smallest integer /e
satisfying àfie* ne = zero(src(e), tgt(e))\ is called the depth of e, and is denoted
depthfe). o

US 18

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

We stress that acyclicity refers to constraints K and not to graph G. The way
edges in K dépend on one another, may be represented as a graph 3C called the
dependency graph. This graph is defined as follows:
• the nodes of îft are the edges of G, and
• there is an edge from f to e in 3C whenever e is the head of a constraint in 9C
and f is the body of that constraint.
Note that for every edge e of G the edges which appear in de are the
immédiate sons of e in i t . In particular, leaves of 3C are those edges of G, which
appear only in the body of constraints. This allows to state the following
proposutions and lemmas which express important properties of cyclic
spécifications.
Proposition 6 G\K is cyclic if and only if its dependency graph is cyclic.
Proof If the dependency graph 3C of G\K is cyclic then there is an edge e of G
(i.e. a node of «%) such that à(0e contains e for some / (in fact / is the length of a
cycle in Zfc traversing e). This means that d(k)e * zero(src(e), tgt(e)) for every
k, that is G\K is cyclic. Conversely, if ifC is acyclic then an edge e of G cannot be a
son of e in the graph 3C. Thus, for some k, d(k)e is formed by leaves of «%. This
means that d(k+,)e = zero(src(e), tgt(e)). This complètes the proof. o
Lemma 2 If G\K is cyclic then there is at least one edge e which is head of a
constraint in K, and two paths le and re such that K H le.e.re <ze. Moreover, 1e and
re are cycles of G, but /e and re are not necessarily unique nor with positive
length.
Proof Note that when we write K h- le.e re£ e, the paths 1e and re are cycles in
G. Indeed, le.e.re and e are parallel so src(1e) = src(1e.e.re) = src(e) and tgt(le)
= src(e) so 1e is a cycle. Similarly re is a cycle. Now, assume that the spécification
is cyclic. From Lemma 2, there are edges e, e,, ..., en in G such that the
constraints l0.e.r0 £ e7j /, .e,.r,* ehl (/ = /, 2, ..., n-/)and lnenrn £ eaieinK,
where /, or r, may be the empty path for / = 0, 1, ..., n.lt follows that K\-Iee.re £ e,
where re = r0r} ...rn_,rn and le = /n/n_; .../,/ 0 . Of course, the paths le and re
dépend on the given cycle c but the last equalities show how to construct them
from K. o
Now, if 1e and re in the above lemma are unique for every recursive edge e
then G\K is said to be linearly cyclic. Note that uniqueness of 1€ and re means that
they are formed by non recursive edges. Now the notion of depth can be
generalized for recursive edges.
Définition 12 The depth of a recursive edge e is the smallest integer le> I such
that cft^e contains e. o
us 19

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS ...

Lemma 3 In a linear cyclic spécification G\K, for every recursive edge e, and
for ail integers n and k, if / <n and 0£k<depth(e) then
#(nxdepth(e)+k)e = j n #(k)e

r

n

/*\

Proof We shall prove (*) by induction on k and n. From the proof of Lemma 2
we can see that d(depth(e))e = le.e.re. This means that the equality (*) stands for k=0
and n= /. Assume that for a given n>l, equality (*) stands for 0£k<depth(e)-1
(induction hyopothesis for k). As le and re are formed by non recursive edges, we
can write
n
d(nxdepth(e)hk+1)e = af//\a<*'e.re ; = ^njk* 1)er^
Similarly, assume that for a given k, 0£k£depth(e), equality (*) stands for nA
(induction hypothesis for n). We can then write,
£((n*l)xdepth(e)+k)e

=

^(deph(e))^(nxdepth(e)*k)j

=

^(deph(e))/j n ^(k)Q r n*

= len.d(depth(e)+k).ren = len.(le.d(k)e.re)ren
This complètes the proof. o

= len+1.d(k)e.ren+1.

Lemma 4 For every edge e in an acyclic or in a linearly cyclic spécification and
for every natural number iïO, the G-computation
is a G|K-computation and Tf(e)£Ke. Moreover,
Tt(e)'TM(e)^f^^erlf
where Xj(e) = / div depth(e), r\j(e) = i mod depth(e).

Proof The first part is an immédiate conséquence of Lemma 1 and addition
rule. The second part is a resuit of Lemma 3. o
An important remark at this point is that, even for iïdepth(e), the G\Kcomputation Tf(e) uses only d(k)e, for 0£i<depth(e). Moreover, since the
spécification is assumed to be linearly cyclic, the cycles le and re and ail d(k)e,
0<k<dep th(e), do not contain any recursive edge. o
Now, we shall prove that every consistent interprétation can be embedded in
a model, and that this model can be constructed by a fixpoint operator. To this
end, let us first define an ordering on the class of ail ©-interprétations of a given
spécification G\K as follows:
• B Ihll B 'if and only if 1) /M// = /M//'for every nodeA,and2) Bell £ Bell'
for every edge e.
Définition 13 Given a cycle u .• X -> X in a semantic universe, we say that u is
finitely representable if there is integer n such that (u, u2, ... , un']) is consistent

us 20

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...

and u1 £ u + u2 + ... + i/1"' for every Un. The least n satisfying this inequality is
called the height of u and is denoted he ight(u). o
For example, every finite multivalued function is finitely representable (see
[LeSp93] for more détails).
Let G\K be acyclic or linearly cyclic spécification. Let © be a semantic
universe in which everv cycle isfinitelyrepresentable. and let (G, Il) be a given
interprétation of G which is consistent with K. Let S be the set of ail ©interprétations / which are consistent with K and 11£l. Each / in û can be
extended to ail G|/C-computations. For simplicity, let us dénote the extension of /
also by /. Then l(e+de) exists and is equal to l(e)*l(de), for every edge e in G.
Now, we define T • ô -> ô by :
• 1(1)(A) = I(A), for every node A, and
• T(l)(e) = l(e)&l(de), for every edge e.
Theorem 4 With the above hypothèses, ^is a wposet with least élément // //,
and the function T is continuous and has a least fixpoint I ls which is a model of
G\K.

Proof From the définition of the ordering of â, it is clear that I // is the least
élément of â. Moreover, â is a wposet, because the ordering of â is defined
pointwise and ©is a semantic universe. Let lJt l2 be in âand assume that lubd h l2)
exists in û. This means that for every edge e in G, lj(e)el2(e) exists in ©. Thus we
hâve T(1ub(lltl2))(e) = lj(e) * i2(e) e it(de) el2(de) = T(lj)(e)<BT(l2)(e) =
lub(T(lj), T(l2))(e). That is, the function T is continuous.
As usual, the least fixpoint is obtained by iterating T on the least élément of â.
That is, for every edge e, lels is the limit of the séquence (\\e\\, \\e\\®\\de\\,
Il eB e BdeB e Bd2eB, ...). Using the above notation we can write Bell5 =
ltm,lT,(e)l.
We must show that //eBs can be computed in afinitenumber of steps. i.e. we
must show that BeBsis bouded by an arrow of ©. Using the above Lemmas, if e is
not recursive then Bells = Ile ll&lldeB... e//^eptnre;-/;e//.
Otherwise, consider /e and re as in Lemma 2 and dénote
he = max(height(Blell),

Le=
Re =

height(BrJ)),

IlehllJh.-.ollle"-1!,^
lrehlre2h...0lrenll.

Now, for ail n>0 and ail k, 0£k<depth(e) we can write
IUVI3k)ellreV=*
L e //^e//R e for every i>0.
From Lemma 4 we can write

T,(e) = r T f ' * * * + l ï I Ï T ' l / à«>e.rei

US 21

(*)

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS...
Now,from(*) and (**) we can write

lel5£ edeTt'là(k)ell*Re(

^deToh1llà(k)el)L^

This inequality prove that leI is bounded which complètes the proof. o
In [LeSp93] we show that I ls can be computed by an effective algorithm, in the
semantic universe mSU.
Fixpoint Semantics Using Theorem 1, the model / / s can be extended to cG\K
as a semantic function 11^. This semantic function provides meaning for ail
computations under the constraints of K. Let us consider the functor U : Sem -*
Spec seen earlier and let us consider the full sub-category of the category of Uobjects under (G\K, 11), whose object are consistent interprétations. The pair
(cG\K, I lsJ is an initial object in this sub-category, on the one hand, and is
obtained by a fixpoint operator, on the other hand. We call (cG\K, 11%) the
fixpoint semantics of (G\K, //1).

6

CONCLUSION AND FURTHER RESEARCH

We hâve considered computations over a graph as spécial subgraphs, and we hâve
introduced a set of inference rules for deducing new constraints and new
computations from old. Thèse notions received interprétations in an enriched
category. We proved that the inference rules are sound and complète.
One aspect of our approach that has not been developped hère is its possibility of
incrémental spécification. This aspect, is of particular interest for modular
spécification, especially in databases specifictaion. We are currently investigating
this research direction.
Acknowledgements: This paper would not hâve been written in its présent
form without several valuable discussions that S.K. Lellahi had with Christian
Lair. The authors would like to thank him. The authors would also like to thank
the référées for their comments that hâve contributed to improve the paper.

us 22

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS.

REFERENCES

[BaWe90] M. Barr, C. Wells, Category for Computing Science (Prentice Hall,
1990).
[CoMe90] M.P. Consens, A. Mendelzon, Graphlog : A Visual Formalism for Real
Life Recursion, in : Proc. ACM-SIGACT-SIGMOD-SIGART Symposium on
Principles of Database Systems (1990) 404-416.
[GPV90] M. Guyssen, J. Paredaens, D. Van Gusht, A Graph-Oriented Object
Database Model, Proc. ACM-SIGACT-SIGMOD-SIGART Symposium on
Principles of Database Systems (1990) 417-424.
[Gray74] J.W. Gray, Formai Category Theory : Adjointness for 2-categories,
Lecture Notes in Mathematics, vol 391 (Springer, Berlin, 1974).
[Gray89] J.W. Gray, The Theory of Sketches as a Model for Algebraic Semantics,
In : Category in Computer Science and Logic, Contemporary Mathematics vol. 92
(American Math. Society, 1989) 109-135
[GuSc90] C.A. Gunter, D.S. Scott, Semantic Domains, In : J.van Leeuwen éd.,
Handbook of Theoretical Computer Science vol. B (Elsevier Science Publishers,
1990) 635-674.
[Guti93] R.H. Guting, Second-Order Signature : A Tool for Specifying Data
Model, Query Processing, and Optimization, Sigmod's 93, Proc. of the ACMSigmod International Conférence on Management of Data. Washington DC may
26-28 1993, edited by P. Buneman and S. Jajodia, acm Press.
[KuVa93] G.M. Kuper, M.Y. Vardi, The Logical Model, ACM transactions on
Database Systems, vol. 18, No. 3, September 1993, pages 379-413.
[Kelly 82] G.M. Kelly, Basic Concepts of Enriched Category Theory, vol. 64 of
London Mathematical Society Lecture Note Séries (Cambridge University Press,
1982).
[Lell93] S.K. Lellahi, Une formalisation Algébrique pour la Modélisation des
Données, 5ème journées du LIPN, 6-7 septembre 1993, Univ. Parisl3, France.
[LeSp91] S.K. Lellahi, N. Spyratos, Towards a Categorical Data Model
Supporting Structured Objects and Inheritance, in : proc. Next Génération
Information System Technology, Lecture Notes in Computer Science, vol.504,
(Springer, Berlin, 1991) 86-105.
[LeSp92] S.K. Lellahi, N. Spyratos, Categorical Modelling of Database Concepts,
Esprit BRA Project 3070, Technical Report Séries, FIDE/92/38; University of
Glasgow, Dept. of Computer Science, also Research Report No 746, LRI, Univ.
Paris XI, Orsay, 1992.
[LeSp93] S.K. Lellahi, N. Spyratos, An Algebraic Semantics for Data Modelling
under Constraints, Research Report No 93-05, LIPN, Univ. Paris-Nord,
Villetaneuse, France, 1993.

us 23

DEDUCTION OVER GRAPHS UNDER CONSTRAINTS .„
[MacL71] S. Mac Lane, Catégories for the Working Mathematician (Springer,
Berlin, 1971)
[PoWe92] A J. Power, C. Wells, A formalism for the spécification of essentiallyalgebraic structures in 2-categories, Mathematical Structures in Computer
Science Vol. 2 (1992) 1-28.
[TGP91] C. Tuijn, M. Guyssen, J. Paredaens, A Categorical Approach to ObjectOriented Data Modelling, Research Report No 91-09, University of Antwerp
(UIA), Belgium.
[TuGu92] C. Tuijn, M. Guyssen, Views and Décomposition of Databases from a
Categorical Perspective, Proc. International Conférence on Database Theory
ICDT 92, Lecture Notes in Computer Science vol. 646 (Springer, Berlin, 1992)
99-111.
[Ullm88] J.D. Ullman, Principles of Database and Knowledge-Base Systems, vol.
I (Computer Science Press, 1988).
[VaVa92] J. Van den Bussche, D. Van Gucht, A Hierarchy of Faithful Set
Création in Pure OODBfs, in : Proc. of International Conférence on Database
Theory ICDT, Lecture Notes in Computer Science vol. 646 (Springer-Verlag,
1992) 326-340.
[Wedd92] G.E. Weddell, Resoning about Functional Dependencies Generalized
for Semantic Data Models, ACM Transactions on Database Systems vol 17, No 1
(1992) 32-64.