B) Dipartimento di Informatica, Università di Pisa, Pisa, Italy...
16
Appl Categor Struct (2008) 16:389–419 DOI 10.1007/s10485-008-9127-6 Subobject Transformation Systems Andrea Corradini · Frank Hermann · Paweł Soboci ´ nski Received: 13 October 2006 / Accepted: 22 January 2008 / Published online: 20 February 2008 © Springer Science + Business Media B.V. 2008 Abstract Subobject transformation systems (STS) are proposed as a novel formal framework for the analysis of derivations of transformation systems based on the algebraic, double-pushout (DPO) approach. They can be considered as a simplified variant of DPO rewriting, acting in the distributive lattice of subobjects of a given object of an adhesive category. This setting allows a direct analysis of all possible notions of dependency between any two productions without requiring an explicit match. In particular, several equivalent characterizations of independence of pro- ductions are proposed, as well as a local Church–Rosser theorem in the setting of STS. Finally, we show how any derivation tree in an ordinary DPO grammar leads to an STS via a suitable construction and show that relational reasoning in the resulting STS is sound and complete with respect to the independence in the original derivation tree. Keywords Graph transformation systems · Adhesive categories · Occurrence grammars Mathematics Subject Classifications (2000) 18B35 · 68Q10 · 68Q42 Research partially supported by EU IST-2004-16004 SEnSOria and MIUR PRIN 2005015824 ART. The third author acknowledges the support of EPSRC grant EP/D066565/1. A. Corradini ( B ) Dipartimento di Informatica, Università di Pisa, Pisa, Italy e-mail: [email protected] F. Hermann Department of Electrical Engineering and Computer Science, Technical University of Berlin, Berlin, Germany P. Soboci ´ nski ECS, University of Southampton, Southampton, UK 390 A. Corradini et al. 1 Introduction Graph transformation systems (GTSs) [21] are a powerful specification formalism for concurrent and distributed systems, generalising another classical model of concurrency, namely Place/Transition Petri nets [19]. The concurrent behaviour of GTSs has been thoroughly studied and a consolidated theory of concurrency is now available. In particular, several constructions associated with the concurrent semantics of nets, such as processes and unfoldings, have been extended to GTSs. Intuitively, a deterministic process of a Petri net is a partial-order representation of a concurrent computation of the net, while the unfolding represents a branching and acyclic structure of all its possible concurrent computations. Interestingly, the processes and the unfolding of a net are themselves Petri nets of a particular kind, called occurrence nets. The generalization of these notions to GTSs (see, e.g., [1, 3, 7, 20]) follows a similar pattern, introducing occurrence grammars as a partial-order representation of GTSs computations. Recently, several constructions and results of the classical theory of the algebraic double-pushout (DPO) approach to graph transformation have been extended to rewriting in arbitrary adhesive categories [10, 16]. In a joint effort with other re- searchers, the authors are working on the generalization of the concurrent semantics of nets and GTS to this more abstract setting: first results concerning deterministic processes appeared in [2]. It turns out that a key ingredient in the definition of processes and unfoldings for a given transformation system, is the analysis of the relationships that arise between the occurrences of rules in the possible computations of the system. Such relations include the parallel and sequential independence, deeply studied in the classical theory of the algebraic approaches to graph rewriting [8, 11]; the standard causality and conflict relations; the asymmetric conflict, studied for formalisms able to model read-only operations; and the less known co-causality, disabling and co- disabling, introduced in [2]. Actually, such relations are meaningful for restricted classes of transformation systems only, including the occurrence systems (nets and grammars) mentioned above. Even if the possible ways in which the rules of an occurrence system can be related are quite well understood, to our knowledge a systematic study of this topic is still missing: This is the main goal of the present paper. To this aim, we introduce the notion of a Subobject Transformation System (STS), which can be understood, intuitively, as a DPO rewriting system in the category of subobjects of a given object of an adhesive category (corresponding to the type graph in the typed approaches to DPO rewriting [7]). In this framework, the usual pushout and pullback constructions are replaced by union and intersection of subobjects. Thus, in general, one can work with a set-theoretical syntax rather than with a categorical one. Known examples of STSs in the area of DPO graph transformation systems are the graph processes as defined in [3, 7], and the unfolding presented in [1], but STSs are more general, because no acyclicity constraint is enforced in their definition. Interestingly, it turns out that STSs in category Set with rules having empty interfaces correspond precisely to Elementary Net Systems [22], a class of Petri nets widely studied in the literature. However, the present paper focuses on the core of the new theory only, while the precise relationships among STSs and the mentioned
Transcript of B) Dipartimento di Informatica, Università di Pisa, Pisa, Italy...
App
lCat
egor
Stru
ct(2
008)
16:3
89–4
19D
OI
10.1
007/
s104
85-0
08-9
127-
6
Subo
bjec
tTra
nsfo
rmat
ion
Syst
ems
And
rea
Cor
radi
ni·F
rank
Her
man
n·P
aweł
Sobo
cins
ki
Rec
eive
d:13
Oct
ober
2006
/Acc
epte
d:22
Janu
ary
2008
/Pub
lishe
don
line:
20F
ebru
ary
2008
©Sp
ring
erSc
ienc
e+
Bus
ines
sM
edia
B.V
.200
8
Abs
trac
tSu
bobj
ect
tran
sfor
mat
ion
syst
ems
(ST
S)ar
epr
opos
edas
ano
vel
form
alfr
amew
ork
for
the
anal
ysis
ofde
riva
tion
sof
tran
sfor
mat
ion
syst
ems
base
don
the
alge
brai
c,do
uble
-pus
hout
(DP
O)
appr
oach
.The
yca
nbe
cons
ider
edas
asi
mpl
ified
vari
ant
ofD
PO
rew
riti
ng,a
ctin
gin
the
dist
ribu
tive
latt
ice
ofsu
bobj
ects
ofa
give
nob
ject
ofan
adhe
sive
cate
gory
.T
his
sett
ing
allo
ws
adi
rect
anal
ysis
ofal
lpo
ssib
leno
tion
sof
depe
nden
cybe
twee
nan
ytw
opr
oduc
tion
sw
itho
utre
quir
ing
anex
plic
itm
atch
.In
part
icul
ar,
seve
ral
equi
vale
ntch
arac
teri
zati
ons
ofin
depe
nden
ceof
pro-
duct
ions
are
prop
osed
,as
wel
las
alo
cal
Chu
rch–
Ros
ser
theo
rem
inth
ese
ttin
gof
STS.
Fin
ally
,w
esh
owho
wan
yde
riva
tion
tree
inan
ordi
nary
DP
Ogr
amm
arle
ads
toan
STS
via
asu
itab
leco
nstr
ucti
onan
dsh
owth
atre
lati
onal
reas
onin
gin
the
resu
ltin
gST
Sis
soun
dan
dco
mpl
ete
wit
hre
spec
tto
the
inde
pend
ence
inth
eor
igin
alde
riva
tion
tree
.
Key
wor
dsG
raph
tran
sfor
mat
ion
syst
ems·
Adh
esiv
eca
tego
ries
·O
ccur
renc
egr
amm
ars
Mat
hem
atic
sSu
bjec
tCla
ssifi
cati
ons
(200
0)18
B35
·68Q
10·6
8Q42
Res
earc
hpa
rtia
llysu
ppor
ted
byE
UIS
T-2
004-
1600
4SE
nSO
ria
and
MIU
RP
RIN
2005
0158
24A
RT
.The
thir
dau
thor
ackn
owle
dges
the
supp
orto
fEP
SRC
gran
tEP
/D06
6565
/1.
A.C
orra
dini
( B)
Dip
arti
men
todi
Info
rmat
ica,
Uni
vers
ità
diP
isa,
Pis
a,It
aly
e-m
ail:
andr
ea@
di.u
nipi
.it
F.H
erm
ann
Dep
artm
ento
fEle
ctri
calE
ngin
eeri
ngan
dC
ompu
ter
Scie
nce,
Tec
hnic
alU
nive
rsit
yof
Ber
lin,B
erlin
,Ger
man
y
P.S
oboc
insk
iE
CS,
Uni
vers
ity
ofSo
utha
mpt
on,S
outh
ampt
on,U
K
390
A.C
orra
dini
etal
.
1In
trod
ucti
on
Gra
phtr
ansf
orm
atio
nsy
stem
s(G
TSs
)[2
1]ar
ea
pow
erfu
lsp
ecifi
cati
onfo
rmal
ism
for
conc
urre
ntan
ddi
stri
bute
dsy
stem
s,ge
nera
lisin
gan
othe
rcl
assi
cal
mod
elof
conc
urre
ncy,
nam
ely
Pla
ce/T
rans
itio
nP
etri
nets
[19]
.The
conc
urre
ntbe
havi
our
ofG
TSs
has
been
thor
ough
lyst
udie
dan
da
cons
olid
ated
theo
ryof
conc
urre
ncy
isno
wav
aila
ble.
Inpa
rtic
ular
,se
vera
lco
nstr
ucti
ons
asso
ciat
edw
ith
the
conc
urre
ntse
man
tics
ofne
ts,
such
aspr
oces
ses
and
unfo
ldin
gs,
have
been
exte
nded
toG
TSs
.In
tuit
ivel
y,a
dete
rmin
isti
cpr
oces
sof
aP
etri
net
isa
part
ial-
orde
rre
pres
enta
tion
ofa
conc
urre
ntco
mpu
tati
onof
the
net,
whi
leth
eun
fold
ing
repr
esen
tsa
bran
chin
gan
dac
yclic
stru
ctur
eof
all
its
poss
ible
conc
urre
ntco
mpu
tati
ons.
Inte
rest
ingl
y,th
epr
oces
ses
and
the
unfo
ldin
gof
ane
tar
eth
emse
lves
Pet
rine
tsof
apa
rtic
ular
kind
,ca
lled
occu
rren
cene
ts.
The
gene
raliz
atio
nof
thes
eno
tion
sto
GT
Ss(s
ee,
e.g.
,[1
,3,
7,20
])fo
llow
sa
sim
ilar
patt
ern,
intr
oduc
ing
occu
rren
cegr
amm
ars
asa
part
ial-
orde
rre
pres
enta
tion
ofG
TSs
com
puta
tion
s.R
ecen
tly,
seve
ralc
onst
ruct
ions
and
resu
lts
ofth
ecl
assi
calt
heor
yof
the
alge
brai
cdo
uble
-pus
hout
(DP
O)
appr
oach
togr
aph
tran
sfor
mat
ion
have
been
exte
nded
tore
wri
ting
inar
bitr
ary
adhe
sive
cate
gori
es[1
0,16
].In
ajo
int
effo
rtw
ith
othe
rre
-se
arch
ers,
the
auth
ors
are
wor
king
onth
ege
nera
lizat
ion
ofth
eco
ncur
rent
sem
anti
csof
nets
and
GT
Sto
this
mor
eab
stra
ctse
ttin
g:fir
stre
sult
sco
ncer
ning
dete
rmin
isti
cpr
oces
ses
appe
ared
in[2
].It
turn
sou
tth
ata
key
ingr
edie
ntin
the
defin
itio
nof
proc
esse
san
dun
fold
ings
for
agi
ven
tran
sfor
mat
ion
syst
em,
isth
ean
alys
isof
the
rela
tion
ship
sth
atar
ise
betw
een
the
occu
rren
ces
ofru
les
inth
epo
ssib
leco
mpu
tati
ons
ofth
esy
stem
.Suc
hre
lati
ons
incl
ude
the
para
llel
and
sequ
entia
lin
depe
nden
ce,
deep
lyst
udie
din
the
clas
sica
lthe
ory
ofth
eal
gebr
aic
appr
oach
esto
grap
hre
wri
ting
[8,1
1];t
hest
anda
rdca
usal
ityan
dco
nflic
tre
lati
ons;
the
asym
met
ric
confl
ict,
stud
ied
for
form
alis
ms
able
tom
odel
read
-onl
yop
erat
ions
;an
dth
ele
sskn
own
co-c
ausa
lity,
disa
blin
gan
dco
-di
sabl
ing,
intr
oduc
edin
[2].
Act
ually
,su
chre
lati
ons
are
mea
ning
ful
for
rest
rict
edcl
asse
sof
tran
sfor
mat
ion
syst
ems
only
,in
clud
ing
the
occu
rren
cesy
stem
s(n
ets
and
gram
mar
s)m
enti
oned
abov
e.E
ven
ifth
epo
ssib
lew
ays
inw
hich
the
rule
sof
anoc
curr
ence
syst
emca
nbe
rela
ted
are
quit
ew
ellu
nder
stoo
d,to
our
know
ledg
ea
syst
emat
icst
udy
ofth
isto
pic
isst
illm
issi
ng:T
his
isth
em
ain
goal
ofth
epr
esen
tpa
per.
To
this
aim
,we
intr
oduc
eth
eno
tion
ofa
Subo
bjec
tT
rans
form
atio
nSy
stem
(ST
S),w
hich
can
beun
ders
tood
,in
tuit
ivel
y,as
aD
PO
rew
riti
ngsy
stem
inth
eca
tego
ryof
subo
bjec
tsof
agi
ven
obje
ctof
anad
hesi
veca
tego
ry(c
orre
spon
ding
toth
ety
pegr
aph
inth
ety
ped
appr
oach
esto
DP
Ore
wri
ting
[7])
.In
this
fram
ewor
k,th
eus
ualp
usho
utan
dpu
llbac
kco
nstr
ucti
ons
are
repl
aced
byun
ion
and
inte
rsec
tion
ofsu
bobj
ects
.Thu
s,in
gene
ral,
one
can
wor
kw
ith
ase
t-th
eore
tica
lsyn
tax
rath
erth
anw
ith
aca
tego
rica
lone
.K
now
nex
ampl
esof
STSs
inth
ear
eaof
DP
Ogr
aph
tran
sfor
mat
ion
syst
ems
are
the
grap
hpr
oces
ses
asde
fined
in[3
,7],
and
the
unfo
ldin
gpr
esen
ted
in[1
],bu
tST
Ssar
em
ore
gene
ral,
beca
use
noac
yclic
ity
cons
trai
ntis
enfo
rced
inth
eir
defin
itio
n.In
tere
stin
gly,
ittu
rns
outt
hatS
TSs
inca
tego
rySe
twit
hru
les
havi
ngem
pty
inte
rfac
esco
rres
pond
prec
isel
yto
Ele
men
tary
Net
Syst
ems
[22]
,a
clas
sof
Pet
rine
tsw
idel
yst
udie
din
the
liter
atur
e.H
owev
er,
the
pres
ent
pape
rfo
cuse
son
the
core
ofth
ene
wth
eory
only
,w
hile
the
prec
ise
rela
tion
ship
sam
ong
STSs
and
the
men
tion
ed
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
391
com
puta
tion
alm
odel
sal
read
ypr
opos
edin
the
liter
atur
eis
left
asa
topi
cof
futu
rein
vest
igat
ion.
Aft
erin
trod
ucin
gST
Ssin
Sect
ion
2,w
eex
ploi
tth
emin
Sect
ion
3in
orde
rto
iden
tify
the
poss
ible
basi
cre
lati
ons
amon
gru
les,
and
we
use
thes
eto
defin
eot
her
deri
ved
rela
tion
sw
hich
are
show
nto
coin
cide
wit
hth
ose
intr
oduc
edin
the
liter
atur
efo
rST
Ssar
isin
gas
proc
esse
sof
DP
Ore
wri
ting
syst
ems.
Her
ew
esh
allr
ely
ona
usef
ulau
xilia
rygr
aphi
cal
“Ven
n-di
agra
m”
like
nota
tion
for
reas
onin
gab
out
depe
nden
cyre
lati
ons.
The
zone
sof
the
diag
ram
sar
eno
tin
gene
rals
ubob
ject
san
din
orde
rto
reas
onab
out
them
form
ally
we
intr
oduc
eth
eno
tion
ofre
gion
whi
chis
,ro
ughl
y,a
com
plem
ent
ofa
subo
bjec
t.T
heba
sic
theo
ryof
regi
ons
allo
ws
usto
show
that
reas
onin
gw
ith
the
aid
ofth
eV
enn-
diag
ram
sis
soun
d.N
ext,
inSe
ctio
n4,
we
disc
uss
the
cond
itio
nsun
der
whi
chtw
opr
oduc
tion
sof
anST
Sha
veto
beco
nsid
ered
asin
depe
nden
t,an
dw
ech
arac
teri
zeth
isre
lati
onin
seve
ral
equi
vale
ntw
ays;
alo
cal
Chu
rch–
Ros
ser
theo
rem
clos
esth
ese
ctio
n.In
Sect
ion
5w
epr
esen
ta
colim
itco
nstr
ucti
onth
atbu
ilds
anST
Sfr
oma
give
nde
riva
tion
tree
ofa
DP
Osy
stem
,gen
eral
izin
gth
eco
nstr
ucti
onof
the
proc
ess
ofa
linea
rde
riva
tion
prop
osed
in[3
,7]
.F
inal
lyin
Sect
ion
6w
esh
owth
atth
ean
alys
isof
the
rela
tion
ship
sam
ong
rule
occu
rren
ces
inth
ede
riva
tion
tree
can
bere
duce
dfa
ithf
ully
toth
ean
alys
isof
such
rela
tion
ship
sin
the
gene
rate
dST
S.In
the
conc
ludi
ngse
ctio
nw
elis
tsom
eto
pics
offu
ture
rese
arch
.
2Su
bobj
ectT
rans
form
atio
nSy
stem
s
As
men
tion
edab
ove,
Subo
bjec
tT
rans
form
atio
nSy
stem
sca
nbe
cons
ider
ed,
con-
cept
ually
,as
tran
sfor
mat
ion
syst
ems
base
don
the
DP
Oap
proa
chin
the
cate
gory
ofsu
bobj
ects
Sub(
T)
ofso
me
obje
ctT
ofa
cate
gory
C.W
esh
all
assu
me
that
Cis
anad
hesi
veca
tego
ry:t
his
ensu
res
that
Sub(
T)
isa
dist
ribu
tive
latt
ice.
The
choi
ceis
just
ified
byth
ein
tend
edus
eof
STSs
asa
form
alfr
amew
ork
for
anal
ysin
gde
riva
tion
sof
DP
Osy
stem
s(a
sde
taile
din
Sect
ions
5an
d6)
,whi
chth
emse
lves
are
defin
edov
erad
hesi
veca
tego
ries
in[1
6].
Defi
niti
on1
(Adh
esiv
eca
tego
ries
)A
cate
gory
isca
lled
adhe
sive
if
–It
has
push
outs
alon
gm
onos
;–
Itha
spu
llbac
ks;
–P
usho
uts
alon
gm
onos
are
Van
Kam
pen
(VK
)sq
uare
s.
Ref
erri
ngto
Fig
.1,
aV
Ksq
uare
isa
push
out
(1)
whi
chsa
tisfi
esth
efo
llow
ing
prop
erty
:if
we
draw
aco
mm
utat
ive
cube
(2)
whi
chha
s(1
)as
its
bott
omfa
cean
dw
hose
back
face
sar
epu
llbac
ksth
enth
efr
ont
face
sof
the
cube
are
pullb
acks
ifan
don
lyif
its
top
face
isa
push
out.
Rec
all
that
give
na
cate
gory
Can
dan
obje
ctT
∈C,
the
cate
gory
ofsu
bobj
ects
Sub(
T)
isde
fined
tobe
the
full
subc
ateg
ory
ofth
esl
ice
cate
gory
C/
Tw
ith
obje
cts
the
mon
omor
phis
ms
into
T.
We
deno
tean
obje
cta
:A�
Tof
Sub(
T)
sim
ply
asA
,lea
ving
the
mon
omor
phis
mim
plic
it.N
otic
eth
atSu
b(T
)is
apr
eord
er;t
here
isat
392
A.C
orra
dini
etal
.
Fig
.1A
push
outs
quar
e(1
)an
da
com
mut
ativ
ecu
be(2
)
mos
ton
ear
row
betw
een
any
two
obje
cts
Aan
dB
,de
note
dA
⊆B
.In
part
icul
ar,
this
impl
ies
that
alld
iagr
ams
(in
Sub(
T))
are
com
mut
ativ
e.If
Cha
spu
llbac
ksth
enSu
b(T
)ha
sbi
nary
prod
ucts
(als
oca
lled
inte
rsec
tions
):th
epr
oduc
tof
two
subo
bjec
tsis
give
nby
the
diag
onal
ofth
epu
llbac
ksq
uare
ofth
etw
om
orph
ism
sin
C.
IfC
isad
hesi
ve,
then
Sub(
T)
also
has
bina
ryco
prod
ucts
(uni
ons)
:the
copr
oduc
tof
two
subo
bjec
tsis
give
nby
the
med
iati
ngm
orph
ism
from
the
push
out
inC
ofth
epr
ojec
tion
sof
thei
rin
ters
ecti
on[1
6].
Fur
ther
mor
e,in
this
case
Sub(
T)
isa
dist
ribu
tive
latt
ice,
i.e.p
rodu
cts
dist
ribu
teov
erco
prod
ucts
,and
vice
-ve
rsa.
We
shal
lden
ote
the
prod
ucta
ndco
prod
ucti
nSu
b(T
)by
∩and
∪,re
spec
tive
ly.
Thr
ough
out
the
pape
rw
esh
all
ofte
nus
eV
enn
diag
ram
sto
depi
ctsu
bobj
ects
,re
pres
enti
ngun
ion
and
inte
rsec
tion
inth
eus
ual
way
.F
orex
ampl
e,in
Fig
.2a
subo
bjec
tA
isre
pres
ente
dby
the
area
delim
ited
byth
ele
ftro
unde
dsq
uare
(mad
eof
“zon
es”
aan
dc)
,B
isre
pres
ente
dby
ban
dc,
A∩
Bby
c,an
dA
∪B
bya,
can
db
.It
isw
orth
stre
ssin
gth
atth
isgr
aphi
calr
epre
sent
atio
nof
subo
bjec
tsis
soun
dbe
caus
eSu
b(T
)is
dist
ribu
tive
.In
fact
,for
exam
ple,
inF
ig. 2
bsu
bobj
ects
A∩(
B∪C
)
and
(A
∩B
)∪(
A∩C
),w
hich
are
equa
lby
dist
ribu
tivi
ty,
are
both
repr
esen
ted
byth
ear
eam
ade
ofd,
e,an
df;
sim
ilarl
y,A
∪(B
∩C)
(=(A
∪B
)∩(
A∪C
))is
repr
esen
ted
bya,
d,e,
fan
dg.
Not
ice
that
cate
gory
Sub(
T)
inge
nera
lis
not
adhe
sive
,ev
enif
Cis
.In
fact
,le
tA
⊆B
bean
arro
win
Sub(
T)
whi
chis
not
anis
omor
phis
m;t
hen
the
push
out
obje
ctof
the
span
B⊇
A⊆
Bis
easi
lysh
own
tobe
Bit
self
,but
the
resu
ltin
gsq
uare
isno
ta
pullb
ack,
cont
radi
ctin
gth
efa
ctth
atpu
shou
tsal
ong
mon
osin
anad
hesi
veca
tego
ryar
epu
llbac
ks[1
6]. a
b
Fig
.2V
enn
diag
ram
sre
pres
enti
ngtw
o(a
)an
dth
ree
(b)
subo
bjec
ts,t
heir
unio
nsan
din
ters
ecti
ons
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
393
Defi
niti
on2
(Sub
obje
cttr
ansf
orm
atio
nsy
stem
s)A
Subo
bjec
tT
rans
form
atio
nSy
s-te
m(S
TS)
over
anad
hesi
veca
tego
ryC
isa
trip
leS
=〈 T
,P,π
〉 ,w
here
T∈C
isa
type
obje
ct,
Pis
ase
tof
prod
uctio
nna
mes
,π:P
→Su
b(T
)·←·→
· map
sa
prod
ucti
onna
me
pto
apr
oduc
tion
Lp
⊇K
p⊆
Rp,i
.e.,
asp
anin
Sub(
T),
whe
reL
p,K
pan
dR
p
are
calle
d,re
spec
tive
ly,t
hele
ft-h
and
side
,the
inte
rfac
ean
dth
eri
ght-
hand
side
ofp.
Apr
oduc
tion
will
ofte
nbe
deno
ted
sim
ply
asa
trip
le⟨ L
p,
Kp,
Rp⟩ ,
impl
icit
lyas
sum
ing
that
Kp
⊆L
p∩
Rp.
Defi
niti
on3
(Dir
ect
deri
vati
ons)
Let
S=
〈 T,
P,π
〉 be
aSu
bobj
ect
Tra
nsfo
rmat
ion
Syst
em,π
(q)=
〈 L,
K,
R〉 b
ea
prod
ucti
on,a
ndle
tG
bean
obje
ctof
Sub(
T).
The
nth
ere
isa
dire
ctde
riva
tion
from
Gto
G′ u
sing
q,w
ritt
enG
⇒q
G′ ,
ifG
′ ∈Su
b(T
)an
dth
ere
exis
tsan
obje
ctD
∈Sub
(T)
such
that
:
(a)
L∪
D∼ =
G;
(c)
D∪
R∼ =
G′ ;
(b)
L∩
D∼ =
K;
(d)
D∩
R∼ =
K.
Ifsu
chan
obje
ctD
exis
ts,w
esh
all
refe
rto
itas
the
cont
ext
ofG
w.r
.t.q
oras
the
cont
exto
fthe
dire
ctde
riva
tion
G⇒
qG
′ .A
sw
esh
alls
eela
ter
inP
ropo
siti
on7,
give
na
prod
ucti
onq
and
asu
bobj
ectG
,aco
ntex
tofG
w.r
.t.q
isun
ique
upto
isom
orph
ism
,if
itex
ists
.G
iven
subo
bjec
tsL
and
R,c
onsi
dere
das
left
-an
dri
ght-
hand
side
sof
apr
oduc
-ti
on,t
here
isa
cano
nica
lcho
ice
for
the
inte
rfac
eK
,nam
ely
K=
L∩
R.
Defi
niti
on4
(Pur
eST
S)W
esh
alls
ayth
atan
STS
ispu
rew
hen
K=
L∩
Rin
allo
fit
spr
oduc
tion
s.
Intu
itiv
ely,
ina
pure
STS
nopr
oduc
tion
dele
tes
and
prod
uces
agai
nth
esa
me
part
ofa
subo
bjec
t:th
iste
rmin
olog
yis
adap
ted
from
the
theo
ryof
Ele
men
tary
Net
Syst
ems,
whe
rea
syst
emw
hich
does
not
cont
ain
tran
siti
ons
wit
ha
self
-loo
pis
calle
d“p
ure”
.T
hene
xtte
chni
call
emm
aw
illbe
used
seve
ralt
imes
alon
gth
epa
per:
Itpr
ovid
esa
sim
ple
set-
theo
reti
cals
ynta
xfo
rex
pres
sing
the
fact
that
aco
mm
utat
ive
squa
rein
Sub(
T)
isa
push
outi
nC
.
Lem
ma
5A
ssum
eth
atC
isan
adhe
sive
cate
gory
,tha
tT∈C
,and
that
(†)
isa
squa
rein
Sub(
T)
(equ
ival
ently
,it
isa
com
mut
ativ
esq
uare
ofm
onos
inC
and
ther
eis
am
onom
orph
ism
D→
T).
The
nth
efo
llow
ing
are
equi
vale
nt:
(1)(†
)is
apu
shou
tin
C(2
)B
∩C∼ =
Aan
dD
∼ =B
∪C(3
)B
∩C⊆
Aan
dD
⊆B
∪C.
A��
��
�� ��(†
)
B �� ��C
����
D
Pro
of
(1⇒
2)T
hesq
uare
(†)
isa
push
out
inC
alon
ga
mon
o,th
eref
ore
apu
llbac
k[1
6].
Sinc
eB
∩Cis
also
apu
llbac
kof
C→
Dan
dB
→D
(giv
enth
atth
ere
isa
mor
phis
mD
→T
),w
eha
veB
∩C∼ =
Aan
dth
usD
∼ =B
∪C.
394
A.C
orra
dini
etal
.
(2⇔
3)T
heis
omor
phis
ms
impl
yth
ein
clus
ions
.F
orth
eot
her
impl
icat
ion,
itis
suffi
cien
tto
obse
rve
that
,giv
en(†
),A
⊆B
∩Can
dB
∪C⊆
Dho
ldby
the
univ
ersa
lpro
pert
ies
of∩a
nd∪,
resp
ecti
vely
.(1
⇐2)
Dia
gram
(†)i
sa
push
outi
nC
byth
ech
arac
teri
sati
onof
unio
nsof
subo
bjec
tsin
adhe
sive
cate
gori
es.
��
Itis
inst
ruct
ive
toco
nsid
erth
ere
lati
onsh
ipbe
twee
na
dire
ctde
riva
tion
inan
STS
and
the
usua
lnot
ion
ofa
DP
Odi
rect
deri
vati
onin
anad
hesi
veca
tego
ry.I
tis
poss
ible
tom
ake
this
com
pari
son,
sinc
eon
eca
nco
nsid
era
prod
ucti
onL
p⊇
Kp
⊆R
pas
the
unde
rlyi
ngsp
anof
mon
omor
phis
ms
inC
.W
esh
all
say
that
ther
eis
aco
ntac
tsi
tuat
ion
for
apr
oduc
tion
〈 L,
K,
R〉 a
ta
subo
bjec
tG
⊇L
∈Sub
(T)
ifG
∩R
�⊆L
.In
tuit
ivel
yth
ism
eans
that
part
ofth
esu
bobj
ect
Gis
crea
ted
but
not
dele
ted
byth
epr
oduc
tion
:if
we
wer
eal
low
edto
appl
yth
epr
oduc
tion
atth
ism
atch
via
aD
PO
dire
ctde
riva
tion
,the
resu
ltin
gob
ject
wou
ldco
ntai
nth
eco
mm
onpa
rttw
ice
and
cons
eque
ntly
the
resu
ltin
gm
orph
ism
toT
wou
ldno
tbe
am
onom
orph
ism
;i.e
.,th
ere
sult
wou
ldno
tbe
asu
bobj
ect
ofT
.T
hene
xtre
sult
clar
ifies
the
rela
tion
ship
betw
een
the
defin
itio
nof
dire
ctde
riva
tion
inSu
b(T
)an
dth
est
anda
rdde
finit
ion
used
inth
eD
PO
appr
oach
[8]:
esse
ntia
lly,t
hetw
ode
riva
tion
sco
inci
deif
ther
eis
noco
ntac
t.
Pro
posi
tion
6(S
TS
deri
vati
ons
are
cont
act-
free
doub
lepu
shou
ts)
LetS
=〈 T
,P,π
〉be
anST
Sov
eran
adhe
sive
cate
gory
C,π
(q)=
〈 L,
K,
R〉 b
ea
prod
uctio
n,an
dG
bean
obje
ctof
Sub(
T).
The
nG
⇒q
G′ i
ffL
⊆G
,G∩
R⊆
L,a
ndth
ere
isan
obje
ctD
inC
such
that
the
follo
win
gdi
agra
mco
nsis
tsof
two
push
outs
inC
.
L ��m
��(1
)
K��
l��
��r
��
��k
��(2
)
R ��n
��G
D��
f
����
g��
G′
Pro
of
(⇒)
Supp
ose
that
G⇒
qG
′ .T
hen
byD
efini
tion
3th
ere
exis
tsan
obje
ctD
∈Sub
(T)
such
that
(a)
L∪
D∼ =
Gan
d(b
)L
∩D
∼ =K
,so
clea
rly
L⊆
Gan
dby
the
conc
lusi
onof
Lem
ma
5,th
ele
ftsq
uare
(1)
isa
push
out
inC
.Fur
ther
mor
e,(c
)D
∪R
∼ =G
′ and
(d)
D∩
R∼ =
K,a
ndth
us(2
)is
apu
shou
tin
Cas
wel
l.T
hefa
ctth
atG
∩R
⊆L
can
besh
own
asfo
llow
s,us
ing
(a)
and
(d):
G∩
R(a
) ∼ =(L
∪D
)∩
R(∗) ∼ =
(L∩
R)∪(
D∩
R)
(d) ∼ =(L
∩R
)∪
K⊆
L
whe
re(∗)
hold
sby
dist
ribu
tivi
tyof
Sub(
T).
(⇐)
Supp
ose
that
the
squa
res(1
)an
d(2
)ar
epu
shou
tsin
C,L
⊆G
(3)
and
G∩
R⊆
L(4
).Si
nce
G∈S
ub(T
)an
d(3
),al
larr
ows
of(1
)ar
ein
Sub(
T)
and
byL
emm
a5
we
have
(b)
L∩
D∼ =
Kan
d(a
)L
∪D
∼ =G
.
Cle
arly
K⊆
D∩
R.N
owD
∩R
∼ =D
∩G∩
R⊆ (
4)D
∩L
∼ =K
and
thus
we
con-
clud
eth
atco
ndit
ion
(d):
K∼ =
D∩
Rho
lds.
Bec
ause
squa
re(2
)is
apu
shou
titf
ollo
ws
that
(c):
D∪
R∼ =
G′ .
��
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
395
The
follo
win
gex
ampl
esh
ows
that
inth
epr
esen
ceof
aco
ntac
tsit
uati
on,a
doub
le-
push
out
diag
ram
inC
does
not
corr
espo
ndin
gene
ral
toa
dire
ctde
riva
tion
inth
eST
S.M
ore
prec
isel
y,le
tC
beth
e(a
dhes
ive)
cate
gory
ofse
tsan
dfu
ncti
ons,
and
let
T=
{•}be
asi
ngle
ton
set.
The
nth
eto
psp
anis
apr
oduc
tion
inSu
b(T
),an
dar
row
mis
inSu
b(T
)as
wel
l,bu
tco
ndit
ion
G∩
R⊆
Lis
not
sati
sfied
.The
doub
le-
push
out
diag
ram
can
beco
mpl
eted
inSe
tas
show
n,bu
tth
ere
sult
ing
set
G′ i
sno
ta
subo
bjec
tof
T.
L=
∅��
m��
(1)
K=
∅��
l��
��r
��
��k
��(2
)
R=
{•} ��n
��G
={•}
D=
{•}��
f
����
g��
G′ =
{•,•}
As
aco
nseq
uenc
eof
the
fact
that
adi
rect
deri
vati
onin
anST
Sim
plie
sa
dire
ctde
riva
tion
inth
est
anda
rdD
PO
appr
oach
,we
can
imm
edia
tely
deri
vese
vera
lpr
oper
ties
ofa
deri
vati
on;i
npa
rtic
ular
,we
prov
eit
sde
term
inac
ybe
low
.
Pro
posi
tion
7(D
eter
min
acy
ofST
Sde
riva
tion
s)Su
ppos
eth
atS
=〈 T
,P,π
〉 is
anST
Sov
eran
adhe
sive
cate
gory
,qis
apr
oduc
tion,
and
Gis
anob
ject
ofSu
b(T
).T
hen
the
cont
ext
ofG
w.r
.t.q
isun
ique
upto
isom
orph
ism
,if
itex
ists
.A
sa
cons
eque
nce
the
targ
etof
adi
rect
deri
vatio
nis
dete
rmin
edun
ique
lyup
tois
omor
phis
m:i
fG
⇒q
G′
and
G⇒
qG
′′th
enG
′ ∼ =G
′′ .
Pro
ofIf
Dis
aco
ntex
tof
Gw
.r.t.
q,by
Pro
posi
tion
6it
isa
push
out
com
plem
ent
ofK
⊆L
and
L⊆
Gin
C.
The
stat
emen
tfo
llow
sfr
omth
eun
ique
ness
upto
isom
orph
ism
ofpu
shou
tcom
plem
ents
alon
gm
onos
inad
hesi
veca
tego
ries
[16]
.
3R
elat
ions
amon
gP
rodu
ctio
ns
The
theo
ryof
the
DP
Oap
proa
chto
the
tran
sfor
mat
ion
ofgr
aphs
incl
udes
seve
ral
resu
lts
and
cons
truc
tion
sw
hich
aim
ata
high
erle
vel
ofab
stra
ctio
nin
the
anal
ysis
ofth
eco
mpu
tati
ons
(con
cret
ely,
linea
rse
quen
ces
ofdo
uble
-pus
hout
diag
ram
s)of
asy
stem
.F
orex
ampl
e,ty
pica
llyon
edo
esno
tw
ant
toco
nsid
eras
dist
inct
two
deri
vati
ons
whi
chdi
ffer
only
inth
eor
der
inw
hich
“ind
epen
dent
”pr
oduc
tion
sar
eap
plie
d:th
isle
dto
the
defin
itio
nof
shif
teq
uiva
lenc
e[1
5],
and
mor
ere
cent
lyto
noti
ons
and
cons
truc
tion
sbo
rrow
edfr
omth
eth
eory
ofP
etri
nets
,in
clud
ing
the
defin
itio
nof
proc
esse
s[7
]for
DP
Osy
stem
san
dth
eun
fold
ing
cons
truc
tion
[1,2
0].
Ake
yin
gred
ient
inth
ede
finit
ions
ofeq
uiva
lenc
eson
deri
vati
ons
and
inth
eaf
orem
enti
oned
cons
truc
tion
ssu
chas
proc
esse
san
dun
fold
ings
isth
ean
alys
isof
the
rela
tion
ship
sw
hich
hold
amon
gth
eoc
curr
ence
sof
rule
sin
the
poss
ible
com
puta
tion
sof
the
give
nsy
stem
.Su
chre
lati
ons
incl
ude
for
exam
ple
the
clas
sica
lpa
ralle
lan
dse
quen
tial
inde
pend
ence
,ca
usal
ityan
dco
nflic
t,as
ymm
etri
cco
nflic
t,an
dth
ele
sskn
own
co-c
ausa
lity,
disa
blin
gan
dco
-dis
ablin
g,re
cent
lyin
trod
uced
in[2
].T
ypic
ally
,the
sere
lati
onsh
ips
are
defin
edov
erpr
oduc
tion
occu
rren
ces
ofth
eor
ig-
inal
syst
emw
ith
resp
ectt
oei
ther
agi
ven
deri
vati
on(a
sfo
rse
quen
tial
inde
pend
ence
orca
usal
ity)
,or
abr
anch
ing
stru
ctur
eof
deri
vati
ons
(lik
eco
nflic
tan
das
ymm
etri
c
396
A.C
orra
dini
etal
.
confl
ict)
,and
they
are
dete
rmin
edby
look
ing
atth
ew
ayth
epr
oduc
tion
occu
rren
ces
over
lap.
Con
side
ra
sim
ple
exam
ple:
ifan
item
xin
anoc
curr
ence
grap
hgr
amm
aris
gene
rate
dby
prod
ucti
onq 1
(i.e
.,x
∈R
1\K
1)
and
itis
cons
umed
byq 2
(x∈
L2\K
2),
then
q 1(d
irec
tly)
caus
esq 2
.In
this
sect
ion
we
pres
ent
aco
mpl
ete
anal
ysis
ofth
ere
lati
onsh
ips
that
may
hold
amon
gth
epr
oduc
tion
sof
aSu
bobj
ect
Tra
nsfo
rmat
ion
Syst
em.
For
the
rest
ofth
epa
per,
we
shal
las
sum
eev
ery
STS
tobe
pure
,i.e
.,su
chth
atK
=L
∩R
for
each
prod
ucti
on,l
eavi
nga
deep
erst
udy
ofno
n-pu
resy
stem
sas
ato
pic
offu
ture
wor
k.F
orth
ego
als
ofth
epr
esen
tpa
per
this
assu
mpt
ion
isno
ta
limit
atio
n,be
caus
eth
eST
Ssar
isin
gas
repr
esen
tati
onof
com
puta
tion
sof
aD
PO
syst
em,i
nclu
ding
proc
esse
san
dun
fold
ings
,are
alw
ays
pure
:thi
sis
prov
edex
plic
itly
inSe
ctio
n6
for
the
STS
obta
ined
from
ade
riva
tion
tree
ofa
DP
Osy
stem
,as
desc
ribe
din
Sect
ion
5.R
ecal
lth
atgi
ven
apu
reST
SS
=〈 T
,P,π
〉 eac
hpr
oduc
tion
nam
eq
∈P
isas
soci
ated
wit
ha
prod
ucti
on,
whi
chis
atr
iple
ofsu
bobj
ects
π(q
)=
⟨ Lq,
Kq,
Rq⟩
wit
hK
q=
Lq
∩R
q.
The
Ven
ndi
agra
mof
Fig
.3
show
sth
ew
aytw
opr
oduc
tion
sq 1
=〈 L
1,
K1,
R1〉 a
ndq 2
=〈 L
2,
K2,
R2〉 c
anov
erla
p.In
gene
ral,
the
inte
rsec
tion
ofq 1
and
q 2,i
.e.,
the
subo
bjec
t(L
1∪
R1)∩(
L2∪
R2)
mar
ked
wit
ha
doub
lebo
rder
inth
edi
agra
m,i
sco
mpo
sed
ofni
nezo
nes,
deno
ted
XY
for
X,Y
∈{L
,K,R
}.P
rodu
ctio
nsq 1
and
q 2ca
nbe
cons
ider
edas
com
plet
ely
inde
-pe
nden
tift
heir
inte
rsec
tion
ispr
eser
ved
bybo
thpr
oduc
tion
s,i.e
.,if
itis
cont
aine
din
subo
bjec
tKK
=K
1∩
K2:t
hisn
otio
nof
inde
pend
ence
will
befo
rmal
ized
inSe
ctio
n4.
Eac
hzo
ne(b
utfo
rK
K)
dete
rmin
esa
basi
cre
latio
nbe
twee
nth
etw
opr
oduc
tion
s,w
hich
hold
siff
“the
zone
isno
tem
pty”
;for
exam
ple,
the
non-
empt
ines
sof
RL
wou
ldw
itne
ssth
atq 1
caus
esq 2
.Not
ice
how
ever
that
butf
orK
K,t
here
mai
ning
zone
sin
the
inte
rsec
tion
ofq 1
and
q 2ar
eno
tsub
obje
cts
inge
nera
l,be
caus
eSu
b(T
)m
ight
notb
e
Fig
.3In
ters
ecti
onof
two
pure
prod
ucti
ons
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
397
abo
olea
nla
ttic
e.A
sa
cons
eque
nce
we
intr
oduc
ere
gion
s,w
hich
corr
espo
ndin
Ven
ndi
agra
ms
toth
ezo
nes
whi
char
e“c
ompl
emen
ts”
ofsu
bobj
ects
.
Defi
niti
on8
(Reg
ion)
Let
≡be
the
smal
lest
equi
vale
nce
rela
tion
onSu
b(T
)×
Sub(
T)
whi
chco
ntai
nsth
efo
llow
ing,
for
alls
ubob
ject
sU
,V,W
such
that
W∩U
⊆V
,and
Zsu
chth
atZ
⊆U
∪V∪W
:
(U,
V)≡
(U∪
Z,
V∪W
)
Are
gion
isan
equi
vale
nce
clas
sof
pair
sof
subo
bjec
ts(U
,V
)w
ith
resp
ect
to≡;
we
shal
lwri
teU
\Vfo
rth
ere
gion
cont
aini
ng(U
,V
).
Ina
Ven
ndi
agra
mw
eca
nid
enti
fya
zone
a(w
hich
may
not
bea
subo
bjec
t)w
ith
are
gion
inth
efo
llow
ing
way
.We
first
iden
tify
asu
bobj
ect
Aw
hich
incl
udes
asu
chth
atth
eco
mpl
emen
tof
ain
A,i
nth
ege
omet
rica
lsen
se,c
orre
spon
dsto
asu
bobj
ect
C;i
fsuc
han
Aex
ists
,nex
twe
take
any
subo
bjec
tB
such
that
its
inte
rsec
tion
wit
hA
isC
.The
nw
esa
yth
ata
corr
espo
nds
tore
gion
A\B
.For
exam
ple,
inF
ig.2
a,zo
nea
repr
esen
tsre
gion
A\B
and
bre
pres
ents
B\A
.B
yex
ploi
ting
the
equi
vale
nce
rela
tion
ofD
efini
tion
8it
can
besh
own
that
the
regi
onid
enti
fied
inth
ew
ayde
scri
bed
abov
eis
uniq
ue:
for
exam
ple,
inF
ig.
3,ap
plyi
ngth
eco
nstr
ucti
onto
zone
RL
we
wou
ldge
tre
gion
R1∩
L2\K
1∪
K2,
but
also
regi
onR
1∩
L2\L
1∪
R2,
whi
char
epr
ovab
lyth
esa
me.
We
will
call
basi
cre
gion
sth
ose
repr
esen
ted,
inF
ig.
3,by
XY
for
X,
Y∈{
L,K
,R
},exc
ludi
ngK
Kw
hich
isno
ta
regi
on.N
on-b
asic
regi
ons
are
for
exam
ple
RL
+R
Kan
dK
L+
RK
,co
rres
pond
ing
toR
1∩
L2\K
1an
d(K
1∩
L2)∪(
K2∩
R1)\K
1∩
K2,
resp
ecti
vely
.Ins
tead
,for
exam
ple
RL
+K
Kdo
esno
tre
pres
ent
are
gion
,bec
ause
itis
nott
heco
mpl
emen
tofa
subo
bjec
t.
Defi
niti
on9
(Bas
icre
gion
sofi
nter
sect
ion
ofpr
oduc
tion
s)L
etq 1
=〈 L
1,
K1,
R1〉 a
ndq 2
=〈 L
2,
K2,
R2〉 b
etw
opr
oduc
tion
sof
anST
S.T
hen
the
basi
cre
gion
sof
thei
rin
ters
ecti
on(s
eeF
ig.3
)ar
eth
efo
llow
ing,
wit
hX
,Y
∈{L
,R
}:–
XY
=X
1∩Y
2\K
1∪
K2,
–K
X=
K1∩
X2\K
2,a
nd–
XK
=X
1∩
K2\K
1.
Our
mai
nto
olfo
rth
ean
alys
isof
regi
ons
isa
sim
ple
noti
onof
empt
ines
s;si
nce
regi
ons
are
equi
vale
nce
clas
ses
we
mus
tsh
owth
atth
isno
tion
ofem
ptin
ess
isin
depe
nden
tfro
mth
ech
osen
elem
ento
facl
ass.
Defi
niti
on10
(Em
ptin
ess)
Are
gion
U\V
issa
idto
beem
pty
whe
nU
⊆V
.
Lem
ma
11T
heno
tion
ofem
ptin
ess
isw
ell-
defin
ed.
Pro
ofW
esh
owth
at
U⊆
V⇔
U∪
Z⊆
V∪W
assu
min
gth
at(1
)W
∩U⊆
Van
d(2
)Z
⊆U
∪V∪W
.In
fact
,if
U⊆
V,
then
U∪
Z⊆
[by(2
)]U
∪V∪W
⊆[by
assu
mpt
ion]
V∪W
.Vic
e-ve
rsa,
U∼ =
U∩(
U∪
398
A.C
orra
dini
etal
.
Z)⊆
[byas
sum
ptio
n]U
∩(V
∪W)∼ =
[bydi
stri
buti
vity
](U
∩V)∪(
U∩W
)⊆
[by(1
)]V
.��
Inge
nera
l,“u
nion
”of
regi
ons
isdi
fficu
ltto
defin
e—ho
wev
er,
ifw
eca
nfin
dre
pres
enta
tive
sof
regi
ons
ina
part
icul
arfo
rmat
then
we
can
easi
lysh
owth
atth
eir
com
posi
tion
(int
uiti
vely
,di
sjoi
ntun
ion)
beha
ves
asex
pect
edw
ith
resp
ect
toem
ptin
ess.
For
exam
ple,
supp
ose
that
U1
⊇U
2⊇
U3
are
subo
bjec
ts.
The
nre
gion
R=
U1\U
3is
the
com
posi
tion
ofre
gion
sR
1=
U1\U
2an
dR
2=
U2\U
3:t
hene
xtre
sult
show
sth
at,a
sex
pect
ed,r
egio
nR
isem
pty
ifan
don
lyif
both
R1
and
R2
are
empt
y.
Lem
ma
12(R
egio
nco
mpo
siti
on)
Giv
ena
sequ
ence
ofsu
bobj
ects
U1
⊇U
2⊇
···⊇
Un
with
n≥
2,re
gion
U1\U
nis
empt
yif
and
only
ifre
gion
Uk\U
k+1
isem
pty
for
all
k∈{
1,..
.,n
−1}.
Pro
ofL
et(1
):U
1⊇
U2
⊇···
⊇U
nbe
subo
bjec
ts.
U1\U
nis
empt
y⇔
U1
⊆U
n⇔
[(1)]
U1
=U
n⇔
[(1)]
U1=
U2
=···
=U
n⇔
[(1)]
U1⊆
U2
⊆..
.⊆
Un
⇔U
k\U
k+1
isem
pty
for
allk
∈{1,
...,
n−
1}.��
We
shal
lnow
intr
oduc
eth
eba
sic
rela
tion
sam
ong
prod
ucti
ons
form
ally
,pro
vidi
nga
nota
tion
and
two
equi
vale
ntch
arac
teri
zati
ons
for
each
ofth
em.B
efor
eth
at,n
otic
eth
atth
ree
basi
cre
gion
s(L
K,
LR
,K
R)
dono
tin
trod
uce
new
depe
nden
cies
,as
they
are
obta
ined
bysw
itch
ing
the
role
sof
q 1an
dq 2
:th
usth
ere
rem
ain
five
basi
cre
lati
onsh
ips.
Defi
niti
on13
(Bas
icre
lati
ons)
Let
confl
ict
( �),
deac
tivat
ion
(<d),
wri
teca
usal
ity(<
wc)
,rea
dca
usal
ity(<
rc),
and
back
war
dsco
nflic
t(�
),be
defin
edas
show
nin
Fig
.4.
For
each
rela
tion
,we
give
thre
ede
finit
ions
:in
term
sof
apa
rtic
ular
non-
incl
usio
nof
subo
bjec
ts,i
nte
rms
ofa
cert
ain
com
mut
ativ
edi
agra
min
Cno
tbei
nga
push
out
and
byth
eno
n-em
ptin
ess
ofa
basi
cre
gion
.
For
each
rela
tion
the
thre
ede
finit
ions
are
easi
lysh
own
tobe
equi
vale
nt.C
onsi
der
for
exam
ple
q 1�
q 2:
the
area
LL
repr
esen
ts,
acco
rdin
gto
Defi
niti
on9,
regi
onL
1∩
L2\K
1∪
K2.
Thu
sby
Defi
niti
on10
itis
not
empt
yiff
L1∩
L2
�K
1∪
K2.
Fur
ther
mor
e,by
Lem
ma
5,th
isho
lds
ifan
don
lyif
the
diag
ram
inth
efo
urth
colu
mn
isno
ta
push
out,
beca
use
clea
rly
L1∪
L2
∼ =(L
1∪
K2)∪(
K1∪
L2).
As
indi
cate
dby
our
nota
tion
and
easi
lyse
enfr
omth
ede
finit
ion,
the
two
confl
icts
are
sym
met
ric,
whi
leth
eth
ree
form
sof
caus
alit
yar
eno
t.It
isin
stru
ctiv
eto
cons
ider
wha
tth
efiv
ere
lati
ons
mea
nin
part
icul
arse
ttin
gs,s
ayfo
rin
stan
cein
Gra
ph.
Fix
ing
anam
bien
tgr
aph
T,
the
obje
cts
ofSu
b(T
)ar
eth
esu
bgra
phs
ofT
.In
the
follo
win
g,w
ere
fer
toth
ein
divi
dual
vert
ices
ored
ges
ofT
asel
emen
ts.I
nth
isse
ttin
g,th
eba
sic
rela
tion
sca
nbe
char
acte
rise
das
follo
ws:
Con
flict
:q 1
�q 2
prec
isel
yw
hen
q 1co
nsum
esan
elem
ent,
whi
chis
also
cons
umed
byq 2
.B
oth
prod
ucti
ons
are
then
com
peti
ngw
ith
each
othe
rfo
rth
eir
appl
icat
ion.
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
399
fl fl
Fig
.4R
elat
ions
betw
een
prod
ucti
ons
inST
S;π
(qi)
=〈 L
i,K
i,R
i〉 for
i∈{1,
2}
Dea
ctiv
atio
n:q 1
<d
q 2pr
ecis
ely
whe
nq 1
pres
erve
san
elem
ent,
whi
chis
cons
umed
byq 2
.The
refo
req 2
“dea
ctiv
ates
”q 1
mea
ning
that
q 1is
nota
pplic
able
afte
rwar
d.W
rite
caus
ality
:q 1
<w
cq 2
prec
isel
yw
hen
q 1pr
oduc
esan
elem
ent,
whi
chis
cons
umed
byq 2
.R
ead
caus
ality
:q 1
<rc
q 2pr
ecis
ely
whe
nq 1
prod
uces
anel
emen
t,w
hich
isus
edbu
tnot
cons
umed
byq 2
.B
ackw
ards
confl
ict:
q 1�
q 2pr
ecis
ely
whe
nq 1
prod
uces
anel
emen
t,w
hich
isal
sopr
oduc
edby
q 2.
Giv
ena
prod
ucti
onq
wit
hπ
(q)=
〈 L,
K,
R〉 ,w
ew
rite
qopfo
rth
ein
vers
epr
oduc
tion
〈 R,
K,
L〉 :n
otic
eth
atit
follo
ws
imm
edia
tely
from
Defi
niti
on3
that
G⇒
qG
′ if
and
only
ifG
′ ⇒qop
G.
Usi
ngth
is“s
wap
ping
”of
the
left
-an
dri
ght-
hand
side
sof
the
prod
ucti
on,w
eca
nde
rive
anu
mbe
rof
usef
uleq
uiva
lenc
esam
ong
the
basi
cre
lati
ons.
Lem
ma
14(L
aws
for
rela
tion
s)
<rc
and
<d
(a)
q 1<
rcq 2
(b)
⇔q 1
<rc
qop 2
(c)
⇔q 2
<d
qop 1
(d)
⇔qop 2
<d
qop 1;
<w
c,�
,and
�
(e)
q 1<
wc
q 2(f
)⇔
qop 2<
wc
qop 1
(g)
⇔qop 1
�q 2
(h)
⇔q 1
�qop 2
;
400
A.C
orra
dini
etal
.
Pro
ofT
heeq
uiva
lenc
esfo
llow
imm
edia
tely
from
the
defin
itio
ns.
��
The
equi
vale
nces
just
liste
dsh
owth
atus
ing
the
_opop
erat
oron
prod
ucti
ons,
rela
tion
s�
,�an
d<
wc
are
mut
ually
defin
able
,and
soar
e<
rcan
d<
d.
Pro
posi
tion
15(C
ompl
eten
ess)
The
inve
rse
prod
uctio
nop
erat
or_op
toge
ther
with
any
pair
ofre
latio
nsin
{ �,�
,<
wc}
×{<
rc,<
d}f
orm
aco
mpl
ete
basi
sto
mod
elal
lpo
ssib
lere
latio
nsof
Fig
.4.
Itis
wor
thm
enti
onin
ghe
reth
atco
nsid
erin
gpo
ssib
lyno
n-pu
reST
Ss,
the
set
ofba
sic
rela
tion
sw
ould
bela
rger
.In
fact
,in
this
case
Ki
coul
dbe
apr
oper
subo
bjec
tof
Li∩
Ri,
for
i∈{1,
2},as
depi
cted
inth
eV
enn
diag
ram
belo
w,a
ndth
eref
ore
seve
nne
wre
gion
sw
ould
aris
ein
the
inte
rsec
tion
oftw
opr
oduc
tion
s,de
note
dIX
orX
Ifo
rX
∈{L
,K,R
}.For
exam
ple,
the
regi
onm
arke
dIL
isno
tem
pty
ifpr
oduc
tion
q 1co
nsum
esan
dpr
oduc
esag
ain
anit
emth
atis
cons
umed
byq 2
.How
ever
,as
disc
usse
din
the
conc
ludi
ngse
ctio
n,th
ere
leva
nce
ofsu
chne
wde
pend
ency
rela
tion
sisn
otcl
ear,
and
thei
rst
udy
goes
beyo
ndth
ego
alof
the
pres
entp
aper
.
����
���
L1
����
���R
1�� ����K
1
����
���
L2 ��
����
�R
2��
����
K2
LL
KL
ILR
L
LK
KK
IKR
K
LI
KI
IIR
I
LR
KR
IRR
R
Let
usco
nsid
erno
wa
few
mor
eco
mpl
exre
lati
ons
amon
gpr
oduc
tion
sth
atha
vebe
enin
trod
uced
in[2
].W
esh
owth
at,
asex
pect
ed,
they
can
bede
fined
easi
lyby
expl
oiti
ngth
eba
sic
rela
tion
ship
sof
Defi
niti
on13
.F
orex
ampl
e,th
e(c
ompo
und)
caus
ality
rela
tion
isbu
iltup
byta
king
the
unio
nof
the
read
caus
ality
and
the
wri
teca
usal
ityre
lati
ons.
Defi
niti
on16
(Com
poun
dre
lati
ons)
Let
caus
ality
(<),
disa
blin
g(�
),co
-cau
salit
y(<
co)
and
co-d
isab
ling
(�co
)be
defin
edas
show
nin
Fig
.5.
For
each
rela
tion
,th
eeq
uati
onal
defin
itio
nin
the
thir
dco
lum
nis
the
one
intr
oduc
edin
[2],
whi
leth
edi
agra
mm
atic
alon
ein
the
four
thco
lum
nan
dth
eno
n-em
ptin
ess
requ
irem
ent
for
the
non-
basi
cre
gion
inth
efif
thco
lum
nar
eeq
uiva
lent
byth
eco
nsid
erat
ions
afte
rD
efini
tion
13.
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
401
Fig
.5C
ompo
und
rela
tion
s;π
(qi)
=〈 L
i,K
i,R
i〉 for
i∈{0,
1}
Lem
ma
17(C
hara
cter
izat
ion
ofco
mpo
und
rela
tion
s)E
ach
one
ofth
eco
mpo
und
rela
tions
ofF
ig.5
can
beob
tain
edas
the
disj
unct
ion
oftw
oba
sic
rela
tions
ofF
ig.4
,as
follo
ws:
–(C
ausa
lity)
q 1<
q 2⇔
q 1<
rcq 2
∨q 1
<w
cq 2
;–
(Dis
ablin
g)q 1
�q 2
⇔q 1
<d
q 2∨
q 2�
q 1;
–(C
o-ca
usal
ity)
q 1<
coq 2
⇔q 1
<d
q 2∨
q 2<
wc
q 1;
–(C
o-di
sabl
ing)
q 1�
coq 2
⇔q 1
<w
cq 2
∨q 1
�q 2
.
Pro
ofW
esh
all
prov
eth
est
atem
ent
for
caus
ality
:T
heot
her
case
sof
com
poun
dre
lati
ons
are
sim
ilar.
Inte
rms
ofre
gion
s,th
est
atem
ent
can
bere
adeq
uiva
lent
lyas
regi
onR
L+
RK
isno
tem
pty
iffei
ther
RL
orR
Kis
not
empt
y,an
dth
usre
gion
RL
+R
Kis
empt
yiff
RL
and
RK
are
empt
y.N
owle
tU
1=
R1∩
L2,
U2
=(K
1∩
L2)∪(
R1∩
K2)
and
U3
=K
1∩
L2.I
tis
stra
ight
forw
ard
toch
eck
that
RL
repr
esen
tsU
1\U
2,R
Kre
pres
ents
U2\U
3,a
ndR
L+
RK
repr
esen
tsU
1\U
3;f
urth
erm
ore
sinc
eU
1⊇
U2
⊇U
3,w
eca
nco
nclu
deby
Lem
ma
12.
Itis
inst
ruct
ive
toco
mpa
reth
egi
ven
proo
fwit
hth
efo
llow
ing
one,
whi
chus
esth
eeq
uiva
lent
defin
itio
nsgi
ven
bydi
agra
ms
inC
notb
eing
push
outs
.
(⇒)
By
cont
rapo
siti
onth
isdi
rect
ion
iseq
uiva
lent
to
q 1≮
rcq 2
and
q 1≮
wc
q 2im
plie
sq 1
≮q 2
.
402
A.C
orra
dini
etal
.
Sinc
eq 1
≮rc
q 2an
dq 1
≮w
cq 2
mea
nth
atth
etw
oco
rres
pond
ing
diag
ram
sof
Fig
.4ar
epu
shou
ts,t
hey
can
beco
mpo
sed
tofo
rmth
epu
shou
tin
Fig
.5,a
sill
ustr
ated
.
K1 �� ��
����
(1)
R1 �� ��
K1∪
K2
����
�� ��(2
)
R1∪
K2
�� ��K
1∪
L2
����
R1∪
L2
(⇐)
Aga
inus
ing
cont
rapo
siti
on,
let
the
diag
ram
(1+
2)be
apu
shou
t;w
eha
veto
show
that
both
diag
ram
s(1
)an
d(2
)ar
epu
shou
ts.S
ince
(1+
2)is
apu
shou
t,us
ing
Lem
ma
5fo
rth
efir
stst
epan
ddi
stri
buti
vity
for
the
seco
nd,w
eha
ve:
(†)
K1
∼ =(K
1∪
L2)∩
R1
∼ =(R
1∩
K1)∪(
R1∩
L2)∼ =
K1∪(
R1∩
L2).
Now
,co
ncer
ning
diag
ram
(1):
(K1∪
K2)∪
R1
∼ =R
1∪
K2
and
usin
g(†
)fo
rth
ela
stst
ep:(
K1∪
K2)∩
R1
=K
1∪(
R1∩
K2)⊆
K1∪(
R1∩
L2)∼ =
K1.U
sing
Lem
ma
5(1
)
isa
push
outi
nC
.A
nalo
gous
lyfo
rdi
agra
m(2
):(K
1∪
L2)∪(
R1∪
K2)∼ =
R1∪
L2
and
wit
h(†
)fo
rth
ela
stst
ep:(
K1∪
L2)∩(
R1∪
K2)∼ =
K1∪(
K1∩
K2)∪(
R1∩
L2)∪
K2
∼ =K
1∪
K2,
thus
wit
hL
emm
a5
also
(2)
isa
push
outi
nC
.��
4In
depe
nden
cein
Subo
bjec
tTra
nsfo
rmat
ion
Syst
ems
Bas
edon
the
rela
tion
sam
ong
prod
ucti
ons
intr
oduc
edab
ove,
we
deve
lop
here
ath
eory
ofin
depe
nden
cefo
rST
Ssw
hich
follo
ws
the
outl
ine
ofth
ecl
assi
calt
heor
yof
the
DP
Oap
proa
ch.I
nter
esti
ngly
,in
our
form
alfr
amew
ork
ther
eis
asi
ngle
noti
onof
inde
pend
ence
amon
gpr
oduc
tion
s,w
hich
corr
espo
nds
tobo
thpa
ralle
land
sequ
entia
lin
depe
nden
ceof
the
DP
Oap
proa
ch,a
sm
ade
prec
ise
inSe
ctio
n6.
Tw
opr
oduc
tion
sof
anST
Sar
ein
depe
nden
tif
thei
rre
spec
tive
appl
icat
ions
dono
tin
terf
ere:
from
the
disc
ussi
onbe
fore
Defi
niti
on13
this
hold
sif
thei
rin
ters
ecti
onis
cont
aine
din
K1∩
K2.
All
alon
gth
isse
ctio
n,w
eas
sum
eth
atS
=〈 T
,P,π
〉 is
anar
bitr
ary
but
fixed
pure
STS,
and
that
for
each
prod
ucti
onna
me
q i∈
P,
the
corr
espo
ndin
gpr
oduc
tion
isπ
(qi)
=〈 L
i,K
i,R
i〉 .
Defi
niti
on18
(Ind
epen
denc
eof
prod
ucti
ons
inST
S)T
wo
prod
ucti
ons
q 1an
dq 2
ofS
are
inde
pend
ent,
deno
ted
q 1♦
q 2,i
f
(L1∪
R1)∩(
L2∪
R2)⊆
(K1∩
K2)
The
refo
re,b
yde
finit
ion,
two
prod
ucti
ons
are
inde
pend
enti
fthe
com
poun
dre
gion
LL
+K
L+
RL
+L
K+
RK
+L
R+
KR
+R
Ris
empt
y.B
yex
ploi
ting
Lem
ma
12w
esh
owth
atth
isho
lds
ifan
don
lyif
allt
heba
sic
regi
ons
are
empt
y,i.e
.,iff
the
prod
ucti
ons
are
not
rela
ted
via
any
ofth
eba
sic
caus
alit
yor
confl
ict
rela
tion
slis
ted
inF
ig.4
,nor
byan
yof
the
sym
met
ric
vari
atio
ns.
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
403
The
orem
19T
wo
prod
uctio
nsq 1
and
q 2of
Sar
ein
depe
nden
tif
and
only
ifal
lbas
icre
gion
sin
(L1∪
R1)∩(
L2∪
R2)
are
empt
y.
Pro
ofL
etq 1
and
q 2be
two
prod
ucti
ons
and
C1
=L
1∪
R1,C
2=
L2∪
R2.C
onsi
der
the
follo
win
gse
quen
ceof
nine
subo
bjec
tsU
1⊇
U2
⊇···
⊇U
9,
whe
refo
rea
chsu
bobj
ectw
elis
tthe
zone
sof
C1∩C
2th
atid
enti
fyit
:
U1
=C
1∩C
2(a
llzo
nes)
,U
2=
(R
1∪
R2)∩U
1(K
L,
RL
,L
K,
KK
,R
K,
LR
,K
R,
RR
),U
3=
(K1∪
R2)∩U
1(K
L,
LK
,K
K,
RK
,L
R,
KR
,R
R),
U4
=(C
1∩
K2)∪(
K1∩C
2)∪(
R1∩
R2)
(KL
,L
K,
KK
,R
K,
KR
,R
R),
U5
=(K
1∪
K2)∩U
1(K
L,
LK
,K
K,
RK
,K
R),
U6
=[(K
1∩
R2)∪
K2]∩
U1
(LK
,K
K,
RK
,K
R),
U7
=(K
1∩
R2)∪(
R1∩
K2)
(KK
,R
K,
KR
),U
8=
(K1∩
R2)
(KK
,K
R),
and
U9
=K
1∩
K2
(KK
).
The
eigh
tba
sic
regi
ons
ofth
eV
enn
diag
ram
,tha
tw
ere
draw
belo
wfo
rth
ere
ader
’sco
nven
ienc
e,ar
eid
enti
fied
asfo
llow
s:
LL
=U
1\U
2,
KL
=U
5\U
6,
RL
=U
2\U
3,
LK
=U
6\U
7,
RK
=U
7\U
8,
LR
=U
3\U
4,
KR
=U
8\U
9,
and
RR
=U
4\U
5.
Itis
easy
toch
eck
that
this
isco
nsis
tent
wit
hD
efini
tion
9.F
orex
ampl
e,co
nsid
erin
gzo
neK
R,
we
have
(U8,U
9)≡
(K1∩
R2,
K2)
acco
rdin
gto
Defi
niti
on8.
Lem
ma
12ap
plie
sto
the
chai
nof
subo
bjec
tsU
1,..
.,U
9.T
here
fore
,U1\U
9=
C1∩C
1\K
1∩
K2
isem
pty
ifan
don
lyif
U1\U
2,..
.,an
dU
8\U
9ar
eem
pty,
whi
char
eth
eba
sic
regi
ons.
��
����
���
L1
����
���R
1K
1=
L1∩
R1
����
���
L2 ��
����
�R
2
K2
=L
2∩
R2
LL
KL
RL
LK
KK
RK
LR
KR
RR
Dia
gram
1
Inte
rsec
tion
oftw
opu
repr
oduc
tion
s
The
next
lem
ma
show
stha
tift
wo
prod
ucti
onso
fan
STS
are
appl
icab
leto
the
sam
esu
bobj
ect,
then
inor
der
toch
eck
that
they
are
inde
pend
ent
itis
enou
ghto
cons
ider
only
asu
bset
ofth
epo
ssib
lere
lati
ons
amon
gth
em.W
eal
sopr
ovid
ean
alte
rnat
ive
404
A.C
orra
dini
etal
.
char
acte
riza
tion
ofin
depe
nden
ce,
whi
chis
anal
ogou
sto
the
clas
sica
lde
finit
ion
ofpa
ralle
lind
epen
denc
ein
the
DP
Oap
proa
ch(s
eeD
efini
tion
31).
Lem
ma
20(C
hara
cter
izat
ion
ofin
depe
nden
cein
STSs
(I))
Supp
ose
that
ther
ear
edi
rect
deri
vatio
nsG
⇒q 1
G1
and
G⇒
q 2G
2in
S.T
hen
the
follo
win
gar
eeq
uiva
lent
:
(1)
q 1♦
q 2(2
)¬(
q 1�
q 2)
∧¬(
q 1�
q 2)
∧q 1
≮d
q 2∧
q 2≮
dq 1
(3)
L1
⊆D
2∧
L2
⊆D
1∧
¬(q 1
�q 2
),w
here
D1
and
D2
are
the
cont
exts
ofth
efir
stan
dof
the
seco
nddi
rect
deri
vatio
ns,r
espe
ctiv
ely.
Pro
of
(1⇒
2)Im
med
iate
byT
heor
em19
.(1
⇒2)
We
have
tosh
owth
atif
(1)
¬(q 1
�q 2
),(2
)¬(
q 1�
q 2),
(3)
q 1≮
dq 2
and
(4)
q 2≮
dq 1
then
(L1∪
R1)∩(
L2∪
R2)⊆
(K1∩
K2).
Con
side
rDia
gram
1an
dth
ere
lati
onso
fFig
.4:(
1)im
plie
stha
treg
ion
LL
isem
pty,
and
sim
ilarl
y(2
)fo
rR
R,(
3)fo
rK
Lan
d(4
)fo
rL
K.F
urth
erm
ore,
sinc
eG
⇒q 1
G1
byhy
poth
esis
,by
Pro
posi
tion
6w
eha
veG
∩R
1⊆
L1,
and
sinc
eG
⇒q 2
G2,
we
know
that
L2
⊆G
;th
usw
ein
fer
L2∩
R1
⊆L
1,
whi
chim
plie
sth
atth
eno
n-ba
sic
regi
onR
L+
RK
isem
pty.
By
Lem
ma
12th
isim
plie
sth
atbo
thR
Lan
dR
Kar
eem
pty;
infa
ct,l
etU
1=
R1∩
L2,U
2=
(K1∪
K2)∩(
R1∩
L2),
and
U3
=K
1∩
L2:w
eha
veth
atU
1⊇
U2
⊇U
3,
RL
=U
1\U
2,
RK
=U
2\U
3,a
ndR
L+
RK
=U
1\U
3.
Asy
mm
etri
car
gum
ent,
swit
chin
gq 1
and
q 2,
show
sth
atL
Ran
dK
Rar
eem
pty
asw
ell.
The
refo
reth
eei
ghtb
asic
regi
ons
ofD
efini
tion
9ar
eal
lem
pty,
and
we
conc
lude
byT
heor
em19
.
(1⇒
3)B
yhy
poth
esis
and
Defi
niti
on3
we
know
that
G∼ =
L1∪
D1
and
G∼ =
L2∪
D2,
and
that
Li∩
Di∼ =
Ki
for
i∈{1,
2}.T
hus
obje
ctG
can
bese
enas
com
pose
dof
nine
zone
sas
draw
nin
Dia
gram
2,w
here
,for
exam
ple,
L1
ism
ade
ofth
efir
sttw
oco
lum
ns,D
1of
the
seco
ndan
dth
ird
ones
,and
K1,t
heir
inte
rsec
tion
,oft
hem
idco
lum
n.F
rom
q 1♦
q 2it
follo
ws
L1∩
L2
⊆K
1∩
K2,
thus
regi
onL
L+
LK
+K
Lis
empt
y.N
owle
tU
1=
L1∩
L2,
U2
=L
1∩
K2,
and
U3
=K
1∩
K2. D
ecom
posi
tion
ofob
ject
G
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
405
Sinc
eU
1⊇
U2
⊇U
3,
LK
+L
L+
KL
=U
1\U
3,
LL
+K
L=
U1\U
2,
and
LK
=U
2\U
3,
byL
emm
a12
we
conc
lude
that
LL
+K
Lis
empt
y,an
dth
usL
1⊆
D2.
Asi
mila
rar
gum
ents
how
sth
atL
2⊆
D1.
(3⇒
2)Si
nce
L1
⊆D
2an
dL
2⊆
D1,
we
have
L1∩
L2
⊆D
1∩
D2.
Thu
sin
Dia
-gr
am2
regi
onL
L+
KL
+L
Kis
empt
y,an
dso
are
regi
ons
LL
,KL
and
LK
byan
easy
appl
icat
ion
ofL
emm
a12
.Thi
sim
plie
s(s
eeF
ig.4
)th
at¬(
q 1�
q 2),
q 1≮
dq 2
and
q 2≮
dq 1
.��
Sim
ilar
char
acte
riza
tion
sof
inde
pend
ence
can
bepr
ovid
edif
the
two
prod
ucti
ons
can
beap
plie
din
sequ
ence
:By
usin
gth
ein
vers
eof
apr
oduc
tion
,the
proo
fis
redu
ced
toth
atof
the
prev
ious
lem
ma.
Lem
ma
21(C
hara
cter
izat
ion
ofin
depe
nden
cein
STSs
(II)
)Su
ppos
eth
atth
ere
are
dire
ctde
riva
tions
G⇒
q 1G
1⇒
q 2G
2in
S.T
hen
the
follo
win
gar
eeq
uiva
lent
:
(1)
q 1♦
q 2(2
)q 1
≮rc
q 2∧
q 1≮
wc
q 2∧
q 2≮
wc
q 1∧
q 1≮
dq 2
(3)
R1
⊆D
2∧
L2
⊆D
1∧
q 2≮
wc
q 1,w
here
D1
and
D2
are
the
cont
exts
ofth
efir
stan
dof
the
seco
nddi
rect
deri
vatio
ns,r
espe
ctiv
ely.
Pro
ofO
bser
veth
atG
⇒q 1
G1
iffG
1⇒
qop 1G
.Fur
ther
mor
e,by
Lem
ma
14w
eha
ve
q 1≮
rcq 2
⇔q 2
≮d
qop 1us
ing
(a)⇔
(c)
q 1≮
wc
q 2⇔
¬(qop 1
�q 2
)us
ing
(e)⇔
(g)
q 2≮
wc
q 1⇔
¬(qop 1
�q 2
)us
ing
(e)⇔
(h)
q 1≮
dq 2
⇔qop 1
≮d
q 2.
usin
g(c
)⇔
(d).
The
nth
est
atem
ent
follo
ws
byL
emm
a20
,ob
serv
ing
that
qop 1♦
q 2ho
lds,
byde
finit
ion,
ifan
don
lyif
q 1♦
q 2.
��
The
next
resu
ltre
phra
ses
inth
ese
ttin
gof
Subo
bjec
tT
rans
form
atio
nSy
stem
sth
ew
ell-
know
nlo
calC
hurc
h–R
osse
rth
eore
mof
the
DP
Oap
proa
ch.
The
orem
22(L
ocal
Chu
rch–
Ros
ser
for
STSs
)L
etq 1
and
q 2be
two
inde
pend
ent
prod
uctio
nsof
S.T
hen:
(1)
The
rear
edi
rect
deri
vatio
nsas
indi
agra
m(†
)be
low
.(2
)If
ther
ear
edi
rect
deri
vatio
nsG
⇒q 1
G1
and
G⇒
q 2G
2,
then
ther
eis
anob
ject
Hin
Sub(
T)
and
dire
ctde
riva
tions
G1
⇒q 2
Han
dG
2⇒
q 1H
,as
indi
agra
m(‡
)
belo
w.
(3)
Ifth
ere
are
dire
ctde
riva
tions
G⇒
q 1G
1⇒
q 2H
,th
enth
ere
isan
obje
ctG
2in
Sub(
T)
and
dire
ctde
riva
tions
G⇒
q 2G
2an
dG
2⇒
q 1H
,as
indi
agra
m(‡
).
L1∪
L2
q 1 �����
���
����
��q 2
��������
������
(†)
R1∪
L2
q 2��
������
������L
1∪
R2
q 1���
����
���
����
R1∪
R2
Gq 1
�����
���
��q 2 ������
����
(‡)
G1
q 2������
����G
2
q 1���
���
����
H
406
A.C
orra
dini
etal
.
Pro
of
(1)
Itis
easy
toch
eck
that
(L1∪
L2)⇒
q 1(R
1∪
L2)
wit
hco
ntex
tD
1de
f =L
2∪
K1.I
nfa
ct,t
heco
ndit
ions
(a–
d)of
Defi
niti
on3
redu
ceto
(a)
L1∪(
L2∪
K1)∼ =
L1∪
L2,o
bvio
usbe
caus
eK
1⊆
L1;
(b)
L1∩(
L2∪
K1)∼ =
(L1∩
L2)∪(
L1∩
K1)∼ =
K1,
bydi
stri
buti
vity
and
inde
pend
ence
;(c
)(L
2∪
K1)∪
R1
∼ =R
1∪
L2,o
bvio
usbe
caus
eK
1⊆
R1;
(d)
(L2∪
K1)∩
R1
∼ =(L
2∩
R1)∪(
K1∩
R1)∼ =
K1,
bydi
stri
buti
vity
and
inde
pend
ence
.
The
othe
rdi
rect
deri
vati
ons
are
sim
ilar,
usin
gas
cont
exts
(clo
ckw
ise)
L1∪
K2,K
1∪
R2,a
ndR
1∪
K2.
(2)
Let
Hde
f =(D
1∩
D2)∪
R1∪
R2,w
here
D1
and
D2
are
the
cont
exts
ofth
efir
stan
dof
the
seco
nddi
rect
deri
vati
ons,
resp
ecti
vely
.
Let
ussh
owth
atG
1⇒
q 2H
:th
epr
oof
that
G2
⇒q 1
His
anal
ogou
s.L
etD
′ 2de
f =(D
1∩
D2)∪
R1:w
esh
owth
atco
ndit
ions
(a–
d)of
Defi
niti
on3
hold
for
cont
ext
D′ 2.
(a)
[L2∪
D′ 2
∼ =G
1]:
We
have
L2∪
D′ 2
=L
2∪(
(D
1∩
D2)∪
R1)
byde
finit
ion,
and
(∗)
L2∪(
D1∩
D2)∼ =
D1
byin
spec
ting
Dia
gram
2(u
sing
L2
⊆D
1,
whi
chfo
llow
sby
Lem
ma
20);
thus
we
get
L2∪
D′ 2
∼ =D
1∪
R1,
but
D1∪
R1
∼ =G
1by
(c)
ofG
⇒q 1
G1,
sow
ear
edo
ne.
Mor
eex
plic
itly
,(∗
)fo
llow
sfr
omL
2∪(
D1∩
D2)∼ =
(L2∪
D1)∩(
L2∪
D2)∼ = {
byL
2⊆D
1}
D1∩G
∼ =D
1.
(b)
[L2∩
D′ 2
∼ =K
2]:
Exp
andi
ngD
′ 2an
ddi
stri
buti
ngw
ege
tL
2∩
D′ 2
=L
2∩(
(D
1∩
D2)∪
R1)∼ =
(L2∩
D1∩
D2)∪(
L2∩
R1);
the
stat
emen
tfo
l-lo
ws
obse
rvin
gth
at(†
)L2∩
D1∩
D2
∼ = {by
(b)
ofG
⇒q 2
G2}
K2∩
D1
∼ = {by
L2⊆D
1}
K2,a
ndth
atby
inde
pend
ence
we
have
L2∩
R1
⊆K
1∩
K2
⊆K
2.
(c)
[D′ 2∪
R2
∼ =H
]:Obv
ious
,by
expa
ndin
gth
ede
finit
ions
ofH
and
D′ 2.
(d)
[D′ 2∩
R2
∼ =K
2]:
Exp
andi
ngD
′ 2an
ddi
stri
buti
ngw
ege
tD
′ 2∩
R2
∼ =(D
1∩
D2∩
R2)∪(
R1∩
R2);
anal
ogou
sto
(†),
the
first
argu
men
tof
the
unio
nis
K2,
and
byin
depe
nden
ceth
ese
cond
one
isin
clud
edin
K2,
allo
win
gus
toco
nclu
de.
(3)
Thi
spo
intr
educ
esto
the
prev
ious
one
byob
serv
ing
that
G⇒
q 1G
1if
and
only
ifG
1⇒
q 1op
G,a
ndq 1
♦q 2
ifan
don
lyif
qop 1♦
q 2.
��
5F
rom
Der
ivat
ion
Tre
esto
Subo
bjec
tTra
nsfo
rmat
ion
Syst
ems
Her
ew
esh
allo
utlin
ean
appl
icat
ion
ofth
eth
eory
ofST
Sde
velo
ped
inth
epr
evio
usse
ctio
ns.I
npa
rtic
ular
,in
this
sect
ion
we
show
that
star
ting
wit
ha
deri
vati
ontr
eein
anar
bitr
ary
adhe
sive
gram
mar
G,w
eob
tain
anST
Svi
aa
fam
iliar
colim
itco
nstr
ucti
on,
that
can
beco
nsid
ered
asa
gene
raliz
atio
nto
the
non-
dete
rmin
isti
cca
seof
the
synt
hesi
sof
apr
oces
sfr
oma
linea
rde
riva
tion
[7].
As
show
nin
the
next
sect
ion,
we
are
then
able
toap
ply
the
loca
lana
lysi
sus
ing
rela
tion
sbe
twee
npr
oduc
tion
sin
the
resu
ltin
gST
Sin
orde
rto
com
plet
ely
char
acte
rise
allt
hein
depe
nden
cein
the
orig
inal
deri
vati
ontr
ee.
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
407
Inor
der
toill
ustr
ate
how
the
tran
sfor
mat
ion
from
ade
riva
tion
tree
forG
toan
STS
wor
ks,i
tis
help
fult
oco
nsid
era
conc
rete
exam
ple.
Supp
ose
thatG
isan
adhe
sive
gram
mar
cont
aini
ngpr
oduc
tion
sq 1
,q 2
and
q 3,a
ndth
atw
eha
vea
deri
vati
ontr
eeas
illus
trat
edin
Fig
.6.
Eac
hst
ep(d
irec
tde
riva
tion
)in
the
orig
inal
deri
vati
ontr
eeα
lead
sto
ane
wpr
oduc
tion
inth
eST
SP
rc(α
).T
hety
pegr
aph
Tof
Prc
(α)
isob
tain
edfr
omth
ede
riva
tion
byco
mpu
ting
ace
rtai
nco
limit
—fo
rfin
ite
tree
s,th
isty
peof
colim
itex
ists
inad
hesi
veca
tego
ries
asit
can
beob
tain
edby
cons
truc
ting
succ
essi
vepu
shou
ts.T
heob
ject
sG
i∈C
can
now
beco
nsid
ered
assu
bobj
ects
ofT
.A
ssh
own
inth
ene
xtse
ctio
n,th
eST
SP
rc(α
)de
rive
dfr
oma
deri
vati
ontr
eeα
sati
sfies
seve
ral
prop
erti
es,
whi
chco
rres
pond
clos
ely
toth
ose
ofoc
curr
ence
gram
mar
s,as
intr
oduc
edin
the
trad
itio
nald
efini
tion
ofpr
oces
ses
for
tran
sfor
mat
ion
syst
ems
like
Pet
rine
tsan
dgr
aph
gram
mar
s[3
,12]
.W
ebe
gin
byin
trod
ucin
gth
eca
tego
ryD
erT
ree(G)
ofde
riva
tion
tree
sof
anad
hesi
vegr
amm
arG
.T
heob
ject
sof
this
cate
gory
are
wor
dsof
obje
cts
ofC
and
arro
ws
are
fore
sts
ofde
riva
tion
tree
s.G
iven
anar
bitr
ary
obje
ctS
∈C,i
tis
poss
ible
tosh
owth
atth
eco
nstr
ucti
onsk
etch
edin
the
prev
ious
para
grap
hgi
ves
rise
toa
func
tor
Prc
:S/D
erT
ree(G)
→ST
S
whe
reST
Sis
the
cate
gory
ofsu
bobj
ectt
rans
form
atio
nsy
stem
san
dth
eir
mor
phis
ms,
defin
edby
suit
ably
rest
rict
ing
the
usua
lnot
ion
ofty
ped
gram
mar
mor
phis
ms.
How
-ev
er,
sinc
eth
efu
ncto
rial
prop
erty
ofth
eco
nstr
ucti
onis
not
rele
vant
for
the
mai
nre
sult
sof
the
next
sect
ion,
we
will
pres
entt
heco
nstr
ucti
onon
obje
cts
only
.T
hede
finit
ion
ofD
erT
ree(G)
uses
the
defin
itio
nof
adhe
sive
gram
mar
s,as
spec
i-fie
din
[2,1
6];h
owev
er,w
edo
not
apr
iori
assu
me
that
our
gram
mar
sar
ety
ped.
An
exte
nsio
nto
type
dgr
amm
ars
isst
raig
htfo
rwar
d.
Defi
niti
on23
(Adh
esiv
egr
amm
ars)
Let
Cbe
anad
hesi
veca
tego
ry.A
prod
uctio
nis
asp
anof
mon
omor
phis
ms
L�
K�
Rin
C.A
nad
hesi
vegr
amm
arov
erC
isa
pair
G=
〈 P,π
〉 ,whe
reP
isa
seto
fpro
duct
ion
nam
es,a
ndπ
isa
func
tion
whi
chm
aps
any
q∈
Pto
apr
oduc
tion
Lq
�K
q�
Rq.
Defi
niti
on24
(Dir
ectd
eriv
atio
n)L
etG
=〈 P
,π
〉 be
agr
amm
ar,l
etq
∈P
,let
G,
G′ ∈
ob(C
),an
dm
:Lq
�G
bea
mon
omor
phis
m,c
alle
da
mat
ch.T
hen
qre
wri
tes
Gto
Fig
.6O
btai
ning
anST
Sfr
oma
deri
vati
ontr
ee
408
A.C
orra
dini
etal
.
G′ a
tm
ifth
ere
exis
tsa
diag
ram
,illu
stra
ted
belo
w,c
onsi
stin
gof
two
push
outs
.We
shal
lwri
teG
=q,m == ⇒
G′ a
ssh
orth
and
for
such
adi
agra
m.
Lq
m��
Kq
l��
r��
k��
Rq
n��
GD
l′��
r′��
G′
The
deri
vati
ontr
ees
ofan
adhe
sive
gram
mar
Gw
illbe
obta
ined
com
posi
tion
ally
bypu
ttin
gto
geth
erbu
ildin
gbl
ocks
calle
dG-
fans
.
Defi
niti
on25
(G-f
an)
Giv
enan
adhe
sive
gram
mar
Gan
dG
,H
1,..
.,H
k(k
≥1)
obje
cts
ofC
,aG-
fan
ϕfr
omG
toH
1..
.H
k,w
ritt
enϕ
:G→
H1..
.H
k,i
sa
diag
ram
cons
isti
ngof
(one
-ste
p)di
rect
deri
vati
onsf
rom
Gto
Hi,
fore
ach
i∈[k]
def ={1,
...,
k}.A
san
exam
ple,
we
illus
trat
ea
fan
ϕ:G
→H
1H
2be
low
:
L1 m
1���
L2
m2
���
K1 k 1
�����
l 1��
r 1
GK
2
k 2
l 2��� �
�
r 2 �����
R1 n 1
�����E
1l′ 1�� � � �
r′ 1
E2
l′ 2
��� ��
r′ 2
�����R
2
n 2
H1
H2
Insi
mpl
ified
grap
hica
lnot
atio
n,w
esh
alld
enot
esu
cha
fan
assh
own
inth
ele
ftm
ost
diag
ram
ofF
ig.7
.We
shal
lwri
tear
(ϕ)
for
the
num
ber
ofpr
oduc
tion
sap
pear
ing
ina
fan
ϕ.M
oreo
ver,
we
shal
labu
seno
tati
onby
refe
rrin
gto
ϕas
afu
ncti
onϕ
:[ar(
ϕ)]
→P
,whe
reP
isth
ese
tofp
rodu
ctio
nsof
G.T
hus,
ifϕ
cons
ists
oftw
odi
rect
deri
vati
ons
G=q 1
,m1
===⇒
H1
and
G=q 2
,m2
===⇒
H2
from
left
tori
ght,
we
have
ar(ϕ
)=
2,ϕ(1
)=
q 1an
dϕ(2
)=
q 2.
We
shal
lus
eG-
fans
toco
nstr
uct
ast
rict
mon
oida
lca
tego
ryof
deri
vati
ontr
ees,
Der
Tre
e(G)
.W
efir
stne
edto
reca
llth
eno
tion
ofa
tens
orsc
hem
e[1
4]an
dth
eas
soci
ated
noti
onof
afr
eem
onoi
dalc
ateg
ory
ona
tens
orsc
hem
e.1
Ate
nsor
sche
meT
cons
ists
ofa
set
Vof
vert
ices
,ase
tE
ofed
ges,
and
func
tion
ss,
t:E
→V
∗ ,w
here
V∗ i
sthe
free
mon
oid
(the
seto
ffini
tew
ords
)on
V.E
very
tens
orsc
hem
ele
ads
toa
free
stri
ct2
mon
oida
lcat
egor
yC
—se
e[1
4]fo
rde
tails
.Int
uiti
vely
,th
eob
ject
sof
Cca
nbe
seen
asfin
ite
wor
ds(i
.e.,
the
prod
uct
inV
∗is
inte
rpre
ted
as⊗
inC
)in
Van
dth
ear
row
sof
Car
ege
nera
ted
free
lyfr
omth
eba
sic
edge
sin
E.
Con
cret
ely,
the
arro
ws
can
bese
enas
cert
ain
equi
vale
nce
clas
ses
oras
cert
ain
stri
ngdi
agra
ms;
see
also
[23]
.
1 Ten
sor
sche
mes
are
clos
ely
rela
ted
toP
etri
nets
inth
ese
nse
of[1
8],s
ee[9
].2 T
hete
nsor
prod
ucti
sas
soci
ativ
e“o
nth
eno
se”:
(A
⊗B
)⊗
C=
A⊗
(B
⊗C
).
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
409
Fig
.7A
G-fa
nϕ
:G→
H1
H2
and
anar
row
G1
→G
4⊗
G5⊗
G3⊗
G2
⊗G
3⊗
G1
inD
erT
ree(G)
For
the
purp
oses
ofth
efo
llow
ing
defin
itio
n,w
eas
sum
eth
atth
eun
derl
ying
cate
gory
Cof
Gis
asm
all
cate
gory
.Si
zepl
ays
aro
lebe
caus
ew
esh
all
cons
truc
ta
tens
orsc
hem
ew
ith
the
obje
cts
ofC
asit
sse
tofv
erti
ces.
As
usua
l,ho
wev
er,o
neco
uld
rede
fine
the
noti
onof
tens
orsc
hem
eap
prop
riat
ely
(dep
endi
ngon
the
unde
rlyi
ngse
tth
eory
)so
that
the
cons
truc
tion
mak
esse
nse
for
anar
bitr
ary
cate
gory
.
Defi
niti
on26
(Der
Tre
e (G )
)G
iven
anad
hesi
vegr
amm
arG
over
smal
lC
,le
tT G
deno
teth
ete
nsor
sche
me
wit
hse
tof
vert
ices
the
obje
cts
ofC
and
its
edge
sth
eG-
fans
.By
Der
Tre
e(G)
we
deno
teth
efr
eest
rict
mon
oida
lcat
egor
yov
erT G
.
For
exam
ple,
for
afa
nϕ
:G→
H1H
2se
enas
aned
geof
T Gw
eha
ves(
ϕ)=
Gan
dt(
ϕ)=
H1H
2.
The
obje
cts
ofD
erT
ree(G)
are
finit
ew
ords
ofob
ject
sof
C.
The
arro
ws
G1..
.G
n→
H1..
.H
mar
ete
nsor
prod
ucts
ofar
row
sG
1→
H1..
.H
i 1,
...G
n→
Hi n
−1+1
...
Hi n
whe
rei n
=m
.Suc
hba
sic
ingr
edie
nts
are
cons
truc
ted
out
offa
ns,a
nex
ampl
eis
give
nin
Fig
.7.T
enso
rpr
oduc
tis
here
ofco
urse
just
putt
ing
such
diag
ram
ssi
de-b
y-si
de.
One
can
also
thin
kof
arro
ws
ofD
erT
ree(G)
asco
ncre
tede
riva
tion
tree
s,co
nstr
ucte
dat
each
leve
lfr
omco
ncre
tefa
nde
riva
tion
diag
ram
sas
illus
trat
edin
Defi
niti
on25
.In
deed
,th
isw
illbe
our
usua
lap
proa
ch.
Fin
ally
,al
thou
ghw
eha
vede
fined
Der
Tre
e(G)
asa
stri
ctm
onoi
dalc
ateg
ory,
itw
ould
be,p
erha
ps,m
ore
natu
ral
tode
fine
itas
afr
eem
ulti
cate
gory
,se
e[1
7]fo
ran
intr
oduc
tory
acco
unt.
The
follo
win
gle
mm
are
late
sou
rpr
esen
tati
onof
Der
Tre
e(G)
wit
hco
ncre
tede
riva
tion
diag
ram
sin
C.
Lem
ma
27E
very
arro
wα
inD
erT
ree(G)
give
sri
seto
aca
noni
cald
iagr
amD
er(α
)in
Cw
hich
witn
esse
sth
ede
riva
tion
tree
.
Pro
ofR
ecal
lfro
mD
efini
tion
25th
ataG-
fan
isa
conc
rete
diag
ram
inC
.An
arro
win
Der
Tre
e(G)
isa
form
alco
nstr
ucti
onw
hich
com
bine
sfa
ns.
Usi
ngth
efa
ctth
atD
erT
ree(G)
isfr
eely
cons
truc
ted
from
the
fans
,any
arro
wα
can
bede
cons
truc
ted
(usu
ally
not
uniq
uely
)as
aα
=α
n..
.α1
whe
reea
chα
iis
ofth
efo
rmid
X′ ⊗
ϕi⊗
idX
′′
and
ϕiis
afa
n.Si
nce
the
codo
mai
nof
each
αiag
rees
wit
hth
edo
mai
nof
each
αi+
1,w
eca
nco
nstr
uctt
hedi
agra
mit
erat
ivel
y,st
arti
ngw
ith
the
fan
ϕ1,a
teac
hst
eppa
stin
gth
eco
rres
pond
ing
fan
atth
eco
rrec
tpla
ceac
cord
ing
toth
edo
mai
nan
dth
eco
dom
ain
ofth
eα
s.It
iscl
ear
that
any
deco
mpo
siti
onof
αgi
ves
rise
toth
esa
me
diag
ram
.��
410
A.C
orra
dini
etal
.
Giv
enan
obje
ctS
∈C,
the
slic
eca
tego
ryS/
Der
Tre
e(G)
has
asob
ject
sth
ede
riva
tion
tree
sfr
omS
and
asar
row
sex
tens
ions
ofsu
chtr
ees.
We
shal
lsh
owth
atea
chde
riva
tion
tree
natu
rally
lead
sto
anST
S.
The
orem
28Su
ppos
eth
atD
er(α
)is
the
cano
nica
ldi
agra
mof
ade
riva
tion
tree
α∈
S/D
erT
ree(G)
.Let
Tde
note
Col
im(D
er(α
)).T
hen
the
cano
nica
lmor
phis
mS
→T
ism
ono.
Mor
eove
r,fo
rea
chfa
nϕ
inα
and
i∈[ar
(ϕ)],
the
cano
nica
lmor
phis
ms
Lϕ(i)→
T,K
ϕ(i)→
Tan
dR
ϕ(i)→
Tar
em
ono.
Pro
ofF
irst
note
that
alla
rrow
sin
Der
(α)
are
mon
o,be
caus
epr
oduc
tion
sar
epa
irs
ofm
onos
,m
atch
esar
em
ono,
and
mon
osar
est
able
unde
rpu
shou
tsin
adhe
sive
cate
gori
es.W
epr
ocee
dby
sim
ple
indu
ctio
non
any
deco
mpo
siti
onα
=α
n..
.α1.T
heba
seca
seis
triv
ial.
For
the
indu
ctiv
est
ep,
supp
ose
that
αi=
idX
′ ⊗ϕ
i⊗
idX
′′an
dϕ
i:G
→G
1..
.G
k.L
etβ
ibe
the
deri
vati
ondi
agra
mco
rres
pond
ing
toth
ede
riva
tion
tree
atG
i.B
yth
ein
duct
ive
hypo
thes
isth
em
orph
ism
sG
i→
Ti=
Col
im(D
er(β
i))
are
mon
o,an
dth
eca
noni
cal
mor
phis
ms
from
each
prod
ucti
onap
pear
ing
inth
ose
deri
vati
ontr
ees
toT
iar
em
ono.
Giv
enth
eab
ove,
we
shal
lco
nstr
uct
anob
ject
Tw
hich
isth
eco
limit
ofth
edi
agra
mbe
low
left
.
To
calc
ulat
eth
eco
limit
ofsu
cha
diag
ram
itis
enou
ghto
cons
ider
the
solid
mor
phis
ms,
beca
use
all
squa
res
are
push
outs
and
colim
its
com
pose
.Si
nce
the
fan
isof
finit
ear
ity,
we
can
calc
ulat
eth
eco
limit
byco
nstr
ucti
ngsu
cces
sive
push
outs
.In
deed
,fo
rea
chi∈
[k]le
tT
′ ibe
the
push
out
ofl′ i
and
t ir′ i.
We
obta
inth
eso
lidpa
rtof
the
diag
ram
abov
eri
ght,
all
mor
phis
ms
are
mon
osi
nce
mon
osar
est
able
unde
rpu
shou
tsin
adhe
sive
cate
gori
es.F
inal
ly,T
isco
nstr
ucte
dby
taki
ngre
peat
edpu
shou
tsin
the
obvi
ous
way
.C
lear
ly,
G→
Tis
mon
o,an
dsi
nce
each
ofth
em
orph
ism
sT
i→
Tar
em
ono,
the
cano
nica
lm
orph
ism
sfr
omth
epr
oduc
tion
sto
Tob
tain
edby
post
com
posi
tion
wit
hT
i→
Tar
em
ono
asw
ell.
Fin
ally
,it
iscl
ear
that
the
resu
ltin
gob
ject
isth
eco
limit
ofth
eor
igin
aldi
agra
m(a
ndof
the
enti
rede
riva
tion
diag
ram
)be
caus
eco
limit
sco
mm
ute.
��
The
STS
asso
ciat
edw
ith
ade
riva
tion
tree
has
the
colim
itof
the
deri
vati
ondi
agra
mas
type
obje
ct,a
ndon
epr
oduc
tion
for
each
dire
ctde
riva
tion
inth
etr
ee.
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
411
Defi
niti
on29
(Der
ived
STS)
Let
Gbe
anad
hesi
vegr
amm
ar.L
etS
∈Cbe
arbi
trar
y.R
ecal
ltha
tth
eob
ject
sof
S/D
erT
ree(G)
are
finit
ede
riva
tion
tree
sfr
omS.
Let
αbe
such
ade
riva
tion
tree
.The
deri
ved
STS
isP
rc(α
)=
〈 T,
P,π
〉 whe
re
–T
=C
olim
(Der
(α))
;–
P=
∑ϕ∈α
ar(ϕ
)—no
teth
atw
efix
the
copr
oduc
tin
Set
and
orde
rth
efa
nsϕ
soth
at〈 i,
j〉∈
Pis
the
ith
prod
ucti
onof
the
jthfa
n.T
heor
deri
ngis
imm
ater
ial;
–π
(i,
j)=
πG(
ϕj(
i));
–T
hety
ping
for
the
prod
ucti
ons
isca
noni
cally
:
L �� ��
K��
����
��
�� ��
R �� ��G
��
��������D
����
����
�� ��
G′
��
�� ����
��
T
Usi
ngth
eco
nclu
sion
ofT
heor
em28
,Prc
(α)
isan
STS.
6A
naly
sing
Der
ivat
ions
inth
eST
S
The
goal
ofth
isse
ctio
nis
tosh
owth
atth
eco
nstr
ucti
onof
the
deri
ved
STS
for
afin
ite
deri
vati
ontr
eein
anad
hesi
vegr
amm
argi
ves
usa
sett
ing
whe
reth
elo
calr
easo
ning
abou
tth
ein
depe
nden
ceof
prod
ucti
ons
usin
gsu
bobj
ect
incl
usio
nan
din
ters
ecti
on,
deve
lope
din
Sect
ion
4,is
fully
abst
ract
wit
hre
spec
tto
corr
espo
ndin
gre
lati
ons
amon
gdi
rect
deri
vati
ons
inth
eor
igin
altr
ee.
We
first
show
how
deri
vati
ons
ofa
give
ndi
agra
mD
er(α
)ar
ere
late
dto
deri
vati
ons
inth
ede
rive
dST
SP
rc(α
).In
part
icul
ar,w
ew
illsh
owth
atal
lpro
duct
ions
inP
rc(α
)
are
pure
,tha
t,as
expe
cted
,eve
ryde
riva
tion
ofD
er(α
)(a
linea
rpa
thin
the
deri
vati
ontr
ee)
isal
soa
deri
vati
onof
Prc
(α),
and
that
ther
ear
eno
back
war
dco
nflic
tsin
Prc
(α).
Thi
sis
show
nin
the
follo
win
gpr
opos
itio
n.
Pro
posi
tion
30(P
rope
rtie
sof
the
deri
ved
STS)
LetG
bean
adhe
sive
gram
mar
,let
α
bea
deri
vatio
ntr
eein
Gw
ithro
otS
(α∈
S/D
erT
ree(G)
),an
dle
tPrc
(α)
beits
deri
ved
STS.
The
n:
(1)
Prc
(α)
ispu
re.
(2)
For
each
dire
ctde
riva
tion
G1
=q,m ==⇒
G2
inα
,let
q′ be
the
corr
espo
ndin
gpr
oduc
tion
inP
rc(α
).T
hen
G1
⇒q′
G2.
(3)
Let
G0
=q 1,m
1==
= ⇒G
1=q 2
,m2
=== ⇒
···G
n−1
=q n,m
n==
= ⇒G
nbe
ade
riva
tion
inα
with
n≥
2,an
dle
tq′ 1,q′ 2
,..
.,q′ n
beth
eco
rres
pond
ing
prod
uctio
nsin
Prc
(α).
The
nq′ n
�< wc
q′ 1.
(4)
Let
q′ 1an
dq′ 2
betw
odi
stin
ctpr
oduc
tions
ofP
rc(α
).T
hen
¬(q′ 1
�q′ 2
).
Pro
ofT
hepr
oofs
ofth
efo
urst
atem
ents
follo
wa
com
mon
patt
ern,
base
don
the
follo
win
gob
serv
atio
ns:
let
�be
the
“bot
tom
part
”of
the
diag
ram
ofde
riva
tion
sD
er(α
);i.e
.,�
isob
tain
edby
dele
ting
from
Der
(α)
all
ofth
edo
uble
-pus
hout
412
A.C
orra
dini
etal
.
diag
ram
s,le
avin
gon
lyth
eir
low
ersp
ans.
Cle
arly
,a
colim
itfo
r�
isal
soa
colim
itfo
rD
er(α
).N
owno
tice
that
�is
sim
ply
conn
ecte
d,an
dit
cons
ists
ofob
ject
sw
hich
are
eith
erth
eso
urce
ofex
actl
ytw
oar
row
s(t
he“D
”s),
orar
eth
eta
rget
ofa
finit
enu
mbe
rof
arro
ws
(the
“G”s
).T
akin
gou
tof
�an
ysi
ngle
“D”
we
obta
intw
osi
mpl
yco
nnec
ted
diag
ram
sen
joyi
ngth
esa
me
prop
erti
esof
�.
Now
cons
ider
any
doub
le-p
usho
utdi
agra
mw
ithi
nD
er(α
),ill
ustr
ated
belo
w:�
cont
ains
only
its
low
ersp
an.
L
(a)
�� ��
K
(b)
����
����
�� ��
R �� ��G
1D
����
����
G2
By
dele
ting
from
�ob
ject
Dan
dth
eou
tgoi
ngar
row
s,w
eob
tain
�1
and
�2:l
etT
1
and
T2
beth
eco
rres
pond
ing
colim
its.
By
The
orem
28th
ere
are
mon
osG
1→
T1
and
G2
→T
2.S
ince
they
are
mon
oan
dsq
uare
s(a
)an
d(b
)ar
epu
llbac
ks,t
hefo
llow
ing
diag
ram
sar
epu
llbac
ksas
wel
l:
L
(1)
�� ��
K��
��
�� ��T
1D
����
K
(2)
�� ��
����
R �� ��D
����
T2
Fur
ther
mor
e,th
eco
limit
Tof
the
orig
inal
diag
ram
�is
obta
ined
byth
efo
llow
ing
push
out,
whi
chis
also
apu
llbac
kas
we
are
inan
adhe
sive
cate
gory
:
T1
(3)
�� ��
D��
��
�� ��T
T2
����
We
can
proc
eed
now
wit
hth
epr
oofo
fthe
four
stat
emen
ts.
(1)
Let
q′ be
apr
oduc
tion
ofP
rc(α
)w
ith
π(q
′ )=
〈 L,
K,
R〉 ,a
ndle
tG
1=q,
m ==⇒G
2be
the
corr
espo
ndin
gdi
rect
deri
vati
onin
Der
(α).
By
the
obse
rvat
ions
abov
e,w
eca
nbu
ildth
edi
agra
mbe
low
.
L
(1)
�� ��
K��
��
�� ��
K��
��
�� ��T
1
(3)
�� ��
D
(2)
����
�� ��
K��
��
�� ��T
T2
����
R��
��
The
uppe
rri
ght
squa
reis
apu
llbac
ksi
nce
K→
Dis
mon
o.Si
nce
all
inte
rior
squa
res
are
pullb
acks
,so
isth
eou
ter
one.
Hen
ceK
∼ =L
∩R
and
thus
the
prod
ucti
onq′ i
spu
re.
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
413
(2)
By
Pro
posi
tion
6,w
eha
veto
show
that
ther
eis
noco
ntac
t,i.e
.,th
atG
1∩
R⊆
L.
Con
side
rth
edi
agra
mbe
low
:the
uppe
rle
ftsq
uare
isa
pullb
ack
sinc
eth
edi
agra
mco
mm
utes
and
G1
→T
1is
mon
o.T
heup
per
righ
tsqu
are
istr
ivia
llya
pullb
ack.
G1 �� ��
D��
��
�� ��
K��
��
�� ��T
1
(3)
�� ��
D
(2)
����
�� ��
K��
��
�� ��T
T2
����
R��
��
All
the
inte
rior
squa
res
are
pullb
acks
,thu
sG
1∩
R∼ =
K⊆
L,a
sde
sire
d.(3
)W
esh
owth
at,
give
nth
ehy
poth
eses
,L
1∩
Rn
∼ =K
1∩
Kn
⊆K
1∪
Kn,
and
thus
q′ n�< w
cq′ 1
.B
yth
egi
ven
deri
vati
on,i
ndi
agra
m�
(the
“bot
tom
part
”of
Der
(α))
,we
have
the
follo
win
gch
ain
ofsp
ans:
G0
←D
1→
G1
←D
2→
···G
n−1
←D
n→
Gn
By
dele
ting
D1
and
Dn
we
get
thre
ese
para
ted
sim
ply
conn
ecte
ddi
agra
ms,
wit
hco
limit
sT
1,T
′ and
Tn.I
nth
efo
llow
ing
diag
ram
,the
colim
itT
of�
isco
mpu
ted
via
the
low
erle
ftpu
shou
t,w
hich
isal
soa
pullb
ack
beca
use
ofad
hesi
vity
.T
hefo
urup
per
righ
tsq
uare
sar
eal
lea
sily
seen
tobe
pullb
acks
,si
nce
K1
→D
1,
Kn
→D
nan
dT
′ →T
are
mon
os.
Thu
sal
lth
ein
teri
orsq
uare
sar
epu
llbac
ks,
mea
ning
that
the
enti
resq
uare
isa
pullb
ack
and
L1∩
Rn
∼ =K
1∩
Kn
asde
sire
d.
Rn
(2)
�� ��
Kn
����
�� ��
Kn∩
D1
����
�� ��
Kn∩
K1
����
�� ��T
n
(3)
�� ��
Dn
����
�� ��
Dn∩
D1
����
�� ��
Dn∩
K1
����
�� ��T
′ n �� ��
T′
(3)
����
�� ��
D1
(1)
����
�� ��
K1
����
�� ��T
T′ 1
����
T1
����
L1
����
(4)
The
rear
etw
oca
ses
toco
nsid
er:
(a)
The
two
dire
ctde
riva
tion
sco
rres
pond
ing
toq′ 1
and
q′ 2be
long
todi
ffer
ent
bran
ches
ofD
er(α
),an
d(b
)th
eybe
long
toth
esa
me
linea
rde
riva
tion
.F
orth
efir
stca
se,s
ince
αis
atr
eew
ekn
owth
atin
Der
(α)
ther
ear
etw
om
inim
alde
riva
tion
s
G0
=q 1,m
1==
=⇒G
1···
Gn−
1=q n
,mn
===⇒
Gn
and
G0
=p 1,m
′ 1==
=⇒G
′ 1···
G′ k−
1=p k
,m′ k
===⇒
G′ k
such
that
q′ 1co
rres
pond
sto
Gn−
1=q n
,mn
=== ⇒
Gn,a
ndq′ 2
toG
′ k−1
=p k,m
′ k==
= ⇒G
′ k,r
espe
c-ti
vely
.In
diag
ram
�w
eha
veth
efo
llow
ing
chai
nof
span
s:
G′ k
←D
′ k→
G′ k−
1···
G′ 1
←D
′ 1→
G0
←D
1→
G1···
Gn−
1←
Dn
→G
n
414
A.C
orra
dini
etal
.
By
dele
ting
D′ k
and
Dn
we
get
thre
ese
para
ted
sim
ply
conn
ecte
ddi
agra
ms,
wit
hco
limit
sT
k,
T′ a
ndT
n,
resp
ecti
vely
.T
hefo
llow
ing
diag
ram
,w
here
all
inte
rior
squa
res
are
pullb
acks
,al
low
sus
toco
nclu
deth
atR
q′ 1∩
Rq′ 2
∼ =K
q′ 1∩
Kq′ 2
,th
usR
q′ 1∩
Rq′ 2
⊆K
q′ 1∪
Kq′ 2
,whi
chm
eans
¬(q′ 1
�q′ 2
).
Rq′ 1
=R
n
(2)
�� ��
Kn
����
�� ��
Kn∩
D′ k
����
�� ��
Kn∩
K′ k
=K
q′ 1∩
Kq′ 2
����
�� ��
Tn
(3)
�� ��
Dn
����
�� ��
Dn∩
D′ k
����
�� ��
Dn∩
K′ k
����
�� ��T
′ n �� ��
T′
(3)
����
�� ��
D′ k
(2)
����
�� ��
K′ k
����
�� ��
TT
′ k��
��T
k��
��R
′ k=
Rq′ 2
����
For
case
(b)
supp
ose,
wit
hout
loss
ofge
nera
lity,
that
q′ 1an
dq′ 2
are
the
pro-
duct
ions
ofP
rc(α
)co
rres
pond
ing
toth
efir
stan
dto
the
last
dire
ctde
riva
tion
sof
the
follo
win
gde
riva
tion
:G
0=q 1
,m1
=== ⇒
G1
=q 2,m
2==
= ⇒G
2···
Gn−
1=q n
,mn
=== ⇒
Gn:
thus
Rq′ 1
=R
1an
dR
q′ 2=
Rn.
Now
ifn
=2,
then
we
have
G1∩
R2
∼ =K
2by
the
proo
fof
poin
t(2
),an
dsi
nce
R1
⊆G
1,w
eha
veR
1∩
R2
⊆K
2⊆
K1∪
K2,t
hus¬(
q′ 1�
q′ 2).
Ifin
stea
dn
>2,
cons
ider
the
follo
win
gch
ain
ofsp
ans
in�
:
G0
←D
1→
G1
←D
2→
G2···
Gn−
1←
Dn
→G
n
By
dele
ting
D2
and
Dn
we
get
thre
ese
para
ted
sim
ply
conn
ecte
ddi
agra
ms,
wit
hco
limit
sT
2,T
′ and
Tn.R
easo
ning
asin
poin
t(3)
we
build
the
follo
win
gdi
agra
m,
whe
real
lthe
inte
rior
squa
res
are
pullb
acks
:
T2
(3)
�� ��
D2
����
�� ��
D2∩
Dn
����
�� ��
D2∩
Kn
����
�� ��T
′ 2 �� ��
T′
(3)
����
�� ��
Dn
(2)
����
�� ��
Kn
����
�� ��T
T′ n
����
Tn
����
Rn
����
The
refo
reth
eou
ter
squa
reis
apu
llbac
k,m
eani
ngth
atT
2∩
Rn
∼ =D
2∩
Kn.N
owby
The
orem
28,
we
know
that
R1
map
sin
ject
ivel
yto
the
colim
itT
2,
and
thus
R1∩
Rn
⊆D
2∩
Kn
⊆K
n⊆
K1∪
Kn,a
sde
sire
d.��
Inor
der
tosh
owth
atST
Ssca
nbe
used
for
reas
onin
gab
out
inde
pend
ence
inde
riva
tion
tree
sof
adhe
sive
gram
mar
s,w
esh
all
need
tore
call
the
stan
dard
noti
ons
ofin
depe
nden
cefr
omth
eth
eory
ofD
PO
rew
riti
ng[8
],na
mel
yse
quen
tial
and
para
llel
inde
pend
ence
for
grap
htr
ansf
orm
atio
nsy
stem
s.G
iven
the
cate
gori
cal
natu
reof
the
defin
itio
ns,t
hesa
me
defin
itio
nsar
eus
edin
the
mor
ege
nera
lset
ting
oftr
ansf
orm
atio
nsy
stem
sba
sed
onad
hesi
veca
tego
ries
[16]
.
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
415
Defi
niti
on31
(Par
alle
lan
dse
quen
tial
inde
pend
ence
)L
etG
bean
adhe
sive
grap
hgr
amm
aran
dq 1
,q2
betw
oof
its
prod
ucti
ons:
Tw
odi
rect
deri
vati
ons
G=q 1
,m1
=== ⇒
G1
and
G=q 2
,m2
=== ⇒
G2
are
para
lleli
ndep
ende
ntif
ther
eex
ist
mor
phis
ms
i:L
1→
D2
and
j:L
2→
D1
such
that
f 2◦i
=m
1an
df 1
◦j=
m2:
R1
n 1
��
K1
l 1��
r 1��
k 1��
L1
m1��
i��
L2
���
m2
����j
��
K2
l 2��
r 2��
k 2��
R2
n 2
��G
1D
1f 1
��g 1
��G
D2
f 2
��g 2
��G
2
Fur
ther
mor
e,tw
odi
rect
deri
vati
ons
G=q 1
,m1
===⇒
G1
=q 2,m
2==
=⇒H
are
sequ
entia
lin
de-
pend
ent
ifth
ere
exis
tm
orph
ism
si:
R1
→D
2an
dj:
L2
→D
1su
chth
atf 2
◦i=
n 1an
dg 1
◦j=
m2:
L1
m1
��
K1
l 1��
r 1��
k 1��
R1
���
n 1����
i��
L2
m2
�� j
��
K2
l 2��
r 2��
k 2��
R2
n 2
��G
D1
g 1
��f 1
��G
1D
2f 2
��g 2
��H
The
follo
win
gth
eore
mst
ates
that
the
cons
truc
tion
ofa
deri
ved
STS
for
afin
ite
deri
vati
ontr
eein
anad
hesi
vegr
amm
arG,
pres
ente
din
Sect
ion
5,gi
ves
usa
sett
ing
whe
reth
elo
calr
easo
ning
abou
tin
depe
nden
cew
ith
subo
bjec
ts,d
evel
oped
inSe
ctio
n3,
isfu
llyab
stra
ctw
ith
resp
ectt
oth
ein
depe
nden
cein
the
orig
inal
deri
vati
on.
The
orem
32(C
heck
ing
inde
pend
ence
inth
ede
rive
dST
S)Su
ppos
eth
atG
isan
adhe
sive
gram
mar
.Let
αbe
ade
riva
tion
tree
inG
with
root
S(α
∈S/
Der
Tre
e(G)
).
1.L
etG
1=q 1
,m1
===⇒
G2,
G1
=q 2,m
2==
=⇒G
3be
two
deri
vatio
nst
eps
inα
,w
ithq 1
=ϕ
k(i),
q 2=
ϕk(
j)fo
rso
me
fan
ϕk
inα
,an
dle
tq′ 1
=〈 i,
k〉 ,q′ 2
=〈 j,
k〉in
Prc
(α)
beth
eco
rres
pond
ing
prod
uctio
nsin
the
deri
ved
STS.
The
nth
efo
llow
ing
are
equi
vale
nt:
(1)
G1
=q 1,m
1==
=⇒G
2an
dG
1=q 2
,m2
===⇒
G3
are
para
lleli
ndep
ende
nt(2
)q′ 1
♦q′ 2
(3)
¬(q′ 1
�q′ 2
)∧q
′ 1≮
dq′ 2
∧q′ 2
≮d
q′ 1
2.L
etG
1=q 1
,m1
===⇒
G2
=q 2,m
2==
=⇒G
3be
two
deri
vatio
nst
eps
inα
,w
ithq 1
=ϕ
k(i
),q 2
=ϕ
l(j)
for
fans
ϕk,ϕ
lin
αan
dq′ 1
=〈 i,
k〉 ,q′ 2
=〈 j,
l〉 in
Prc
(α),
then
the
follo
win
gar
eeq
uiva
lent
:(1
)G
1=q 1
,m1
=== ⇒
G2
=q 2,m
2==
= ⇒G
3ar
ese
quen
tiali
ndep
ende
nt(2
)q′ 1
♦q′ 2
(3)
q′ 1≮
rcq′ 2
∧q′ 1
≮w
cq′ 2
∧q′ 1
≮d
q′ 2
416
A.C
orra
dini
etal
.
Pro
of
1.(1
)⇒
(2)
By
para
llel
inde
pend
ence
ther
ear
ear
row
si:
L1
→D
2an
dj:
L2
→D
1su
chth
atf 2
◦i=
m1
and
f 1◦j
=m
2;i
and
jare
mon
obe
caus
eso
are
f ian
dm
ifo
ri∈
{1,2}.
Itis
easy
tosh
owth
ati
and
jco
mm
ute
wit
hth
ein
ject
ions
ofth
eir
sour
cean
dta
rget
obje
cts
inth
eco
limit
obje
ctT
,th
usL
1⊆
D2
and
L2
⊆D
1in
Sub(
T).
Fur
ther
mor
e,by
Pro
posi
tion
30(4
)it
hold
s¬(
q′ 1�
q′ 2).
The
nw
eco
nclu
deby
Lem
ma
20((
3)⇒
(1))
.(2
)⇒
(1)
byL
emm
a20
((1)
⇒(3
))w
ekn
owth
atL
1⊆
D2
and
L2
⊆D
1in
Sub(
T).
Thu
sth
ere
are
mon
osi:
L1
→D
2an
dj:
L2
→D
1;
sinc
eSu
b(T
)is
apr
eord
er,i
and
jfor
mco
mm
utin
gtr
iang
les
wit
hth
eco
span
sof
inje
ctio
nsD
2→
G1
←L
1an
dD
1→
G1
←L
2,r
espe
ctiv
ely.
Thu
sth
etw
odi
rect
deri
vati
ons
inG
are
para
lleli
ndep
ende
nt.
(2)⇔
(3)
Obv
ious
byL
emm
a20
((1)
⇔(2
)),
obse
rvin
gth
at¬(
q′ 1�
q′ 2)
byP
ropo
siti
on30
(4).
2.T
hepr
oof
isan
alog
ous
toth
atof
the
prev
ious
poin
t,by
expl
oiti
ngL
emm
a21
inst
ead
ofL
emm
a20
,and
poin
t(3)
ofP
ropo
siti
on30
inst
ead
ofpo
int(
4).
��
The
form
alfr
amew
ork
we
intr
oduc
edal
low
sus
topr
ovid
ea
new
proo
foft
hew
ell-
know
nlo
calC
hurc
h–R
osse
rth
eore
mfo
rtr
ansf
orm
atio
nsw
ith
inje
ctiv
em
atch
es,b
yex
ploi
ting
the
corr
espo
ndin
gth
eore
mfo
rST
Ss.
The
orem
33(L
ocal
Chu
rch–
Ros
ser)
LetG
bean
adhe
sive
gram
mar
.
(1)
IfG
=q 1,m
1==
=⇒G
1an
dG
=q 2,m
2==
=⇒G
2ar
etw
opa
ralle
lind
epen
dent
dire
ctde
riva
tions
,
then
ther
ear
ean
obje
ctH
and
dire
ctde
riva
tions
G1
=q 2,m
′ 2==
=⇒H
and
G2=q 1
,m′ 1
===⇒
H
such
that
G=q 1
,m1
===⇒
G1
=q 2,m
′ 2==
=⇒H
and
G=q 2
,m2
===⇒
G2
=q 1,m
′ 1==
=⇒H
are
sequ
entia
lin
depe
nden
t.
(2)
IfG
=q 1,m
1==
=⇒G
1=q 2
,m′ 2
===⇒
Har
etw
ose
quen
tial
inde
pend
ent
dire
ctde
riva
tions
,the
n
ther
ear
ean
obje
ctG
2an
ddi
rect
deri
vatio
nsG
=q 2,m
2==
= ⇒G
2=q 1
,m′ 1
=== ⇒
Hsu
chth
atG
=q 1,m
1==
= ⇒G
1an
dG
=q 2,m
2==
= ⇒G
2ar
epa
ralle
lind
epen
dent
:
Gq 1
,m1 ���
���
����
q 2,m
2
����������
G1
q 2,m
′ 2������
����G
2
q 1,m
′ 1���
���
����
H
Pro
ofW
epr
ove
only
poin
t(1
),be
caus
epo
int
(2)
isco
mpl
etel
yan
alog
ous.
Giv
enG
=q 1,m
1==
= ⇒G
1an
dG
=q 2,m
2==
= ⇒G
2,
cons
ider
the
deri
vati
ontr
eeα
inG
/D
erT
ree(G)
base
don
this
span
ofdi
rect
deri
vati
ons.
The
deri
ved
STS
ofα
,Prc
(α),
cont
ains
byco
nstr
ucti
onon
lytw
opr
oduc
tion
s,sa
yq′ 1
and
q′ 2,
corr
espo
ndin
gto
the
two
dire
ctde
riva
tion
s,w
ith
G⇒
q′ 1G
1an
dG
⇒q′ 2
G2.
Sinc
eth
eor
igin
aldi
rect
deri
vati
ons
are
para
llel
inde
pend
ent
byhy
poth
esis
,by
The
orem
32.1
we
have
that
q′ 1♦
q′ 2,
and
byT
heor
em22
ther
eis
asu
bobj
ect
Hof
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
417
T,t
heco
limit
ofD
er(α
),an
ddi
rect
deri
vati
ons
G1
⇒q′ 2
Han
dG
2⇒
q′ 1H
;fro
mth
epr
oof
ofth
eth
eore
mw
eal
sokn
owth
atth
eco
ntex
tsof
thes
etw
odi
rect
deri
va-
tion
sar
eD
′ 2=
(D
1∩
D2)∪
R1
and
D′ 1
=(D
1∩
D2)∪
R2.
The
refo
reby
Pro
posi
-ti
on6
ther
ear
etw
odo
uble
-pus
hout
diag
ram
sw
itne
ssin
g,up
tois
omor
phis
ms,
that
G1
=q 2,m
′ 2==
= ⇒H
and
G2
=q 1,m
′ 1==
= ⇒H
,for
mat
ches
m′ 2
and
m′ 1
dete
rmin
edby
the
inje
ctio
nsL
2⊆
D1
⊆G
1an
dL
1⊆
D2
⊆G
2,
whi
chho
ldby
hypo
thes
is.
Fin
ally
,no
tice
that
ther
ear
ein
ject
ions
R1
⊆(D
1∩
D2)∪
R1
=D
′ 2an
dL
2⊆
D1,w
hich
mak
eth
ere
sult
-
ing
tria
ngle
sco
mm
ute
beca
use
Sub(
T)
isa
preo
rder
.Thu
sG
=q 1,m
1==
=⇒G
1=q 2
,m′ 2
===⇒
His
sequ
enti
alin
depe
nden
t,an
dso
isG
=q 2,m
2==
=⇒G
2=q 1
,m′ 1
===⇒
Hby
sim
ilar
reas
onin
g.��
7C
oncl
usio
nsan
dF
utur
eW
ork
Inth
ispa
per
we
have
intr
oduc
edsu
bobj
ect
tran
sfor
mat
ion
syst
ems
(ST
S),a
nove
lfo
rmal
fram
ewor
kfo
rth
ean
alys
isof
deri
vati
ons
ofD
PO
tran
sfor
mat
ion
syst
ems.
The
yca
nbe
cons
ider
edas
a“d
isti
lled”
vari
ant
ofD
PO
rew
riti
ng,
acti
ngin
the
dist
ribu
tive
latt
ice
ofsu
bobj
ects
ofa
give
nob
ject
ofan
adhe
sive
cate
gory
.In
this
sett
ing
the
anal
ysis
ofse
vera
lcon
flict
,cau
salit
y,an
din
depe
nden
cere
lati
ons
amon
gpr
oduc
tion
sca
nbe
carr
ied
onus
ing
ase
t-th
eore
tica
lsy
ntax
orsi
mpl
ege
omet
ric
reas
onin
gba
sed
onV
enn
diag
ram
s,th
uspr
ovid
ing
anal
tern
ativ
eto
the
usua
l“d
iagr
amch
asin
g”us
edin
the
alge
brai
cap
proa
ches
tore
wri
ting
.In
part
icul
ar,s
ince
ever
ypr
oduc
tion
inan
STS
has
aun
ique
mat
ch,i
nor
der
toan
alyz
eho
wtw
odi
ffer
ent
prod
ucti
ons
rela
teto
each
othe
r,it
isen
ough
tolo
okat
the
prod
ucti
ons
them
selv
es.
We
have
pres
ente
dse
vera
lch
arac
teri
zati
ons
ofin
depe
nden
ceof
prod
ucti
ons
inpu
reST
Ss,
asw
ell
asa
loca
lC
hurc
h–R
osse
rth
eore
mfo
rth
em,
also
show
ing
how
the
proo
fof
the
loca
lChu
rch–
Ros
ser
theo
rem
for
DP
Otr
ansf
orm
atio
n(w
ith
mon
icm
atch
es)
inan
adhe
sive
cate
gory
can
bere
duce
dto
it.
The
char
acte
risa
tion
can
beco
nsid
ered
com
plet
e,as
we
have
anal
yzed
all
the
poss
ible
way
sin
whi
chca
usal
depe
nden
cyca
nar
ise
betw
een
two
prod
ucti
ons.
Inpa
rtic
ular
,w
eha
vegi
ven
am
inim
alse
tof
basi
cre
lati
ons
and
show
nth
atre
lati
ons
whi
chha
vebe
enpr
evio
usly
cons
ider
edca
nbe
built
upof
the
basi
cse
t.A
sm
enti
oned
inth
ein
trod
ucti
on,S
TSs
over
cate
gory
Set
wit
ha
few
addi
tion
alco
nstr
aint
sar
ein
aon
e-to
-one
corr
espo
nden
cew
ith
apa
rtic
ular
clas
sof
Pet
rine
ts,
calle
dE
lem
enta
ryN
etSy
stem
s(E
NS)
[22]
.3T
hefo
rmal
izat
ion
ofth
epr
ecis
ere
lati
onsh
ipbe
twee
nST
Ssan
dE
NSs
goes
beyo
ndth
ego
alof
the
pres
entp
aper
,and
will
bea
topi
cof
futu
rere
sear
ch.N
ever
thel
ess,
letu
sst
ress
the
met
hodo
logi
calv
alue
ofth
isre
lati
onsh
ip:i
nth
esa
me
way
the
theo
ryof
Pla
ce/T
rans
itio
nne
tsha
sbe
ena
cons
tant
sour
ceof
insp
irat
ion
duri
ngth
ela
stye
ars
for
rese
arch
ers
wor
king
onbo
thth
eore
tica
land
mor
epr
acti
cala
spec
tsof
grap
htr
ansf
orm
atio
nsy
stem
s(a
sw
itne
ssed
for
exam
ple
byth
eva
riou
sco
ncur
rent
sem
anti
cspr
opos
edfo
rG
TSs
,an
dby
thei
rap
plic
atio
nto
the
veri
ficat
ion
ofsu
chsy
stem
s),
we
expe
ctth
atal
soth
eth
eory
ofE
NSs
will
prov
ide
chal
leng
ing
intu
itio
nsth
atco
uld
bege
nera
lized
,atl
east
inpa
rt,t
oth
em
ore
abst
ract
sett
ing
ofST
Ss.
3 Inde
ed,s
ome
term
sw
ein
trod
uced
are
borr
owed
from
the
EN
Ste
rmin
olog
y,lik
epu
rean
dco
ntac
tsi
tuat
ion.
418
A.C
orra
dini
etal
.
Inth
epa
per
we
mai
nly
cons
ider
edpu
resy
stem
s,be
caus
eso
are
the
STSs
aris
ing
asre
pres
enta
tion
ofth
eco
mpu
tati
ons
ofD
PO
syst
ems.
We
show
edin
Sect
ion
3th
atfo
rno
n-pu
resy
stem
sth
ese
tof
basi
cre
lati
ons
wou
ldbe
larg
er.
How
ever
,th
eth
eore
tica
lor
prac
tica
lre
leva
nce
ofsu
chsy
stem
sis
not
clea
r,be
caus
eof
ten
ase
lf-
loop
,mod
ellin
gth
efa
ctth
ata
reso
urce
can
beco
nsum
edan
dpr
oduc
edag
ain,
can
beco
nven
ient
lyre
plac
edw
ith
are
adac
cess
toth
atre
sour
ce.T
his
anal
ysis
isle
ftas
ato
pic
offu
ture
rese
arch
,to
geth
erw
ith
the
stud
yof
som
ena
tura
lge
nera
lizat
ions
ofth
eap
proa
chpr
esen
ted
inth
ispa
per,
incl
udin
gfo
rex
ampl
eth
eha
ndlin
gof
othe
ral
gebr
aic
appr
oach
esto
rew
riti
ng,
like
the
sing
le-p
usho
utan
dth
ese
squi
-pus
hout
appr
oach
es[6
,11]
.In
Sect
ion
5w
epr
esen
ted
aco
nstr
ucti
onth
at,g
iven
afin
itede
riva
tion
tree
ofa
DP
Osy
stem
,bui
lds
anST
S,a
sort
ofno
n-de
term
inis
ticpr
oces
s,w
hich
can
beus
edto
anal
yze
the
depe
nden
cies
amon
gpr
oduc
tion
occu
rren
ces
inth
egi
ven
deri
vati
ontr
ee.
On
the
othe
rha
nd,
the
clas
sica
lun
fold
ing
cons
truc
tion
defin
edfo
rP
etri
nets
and
GT
Ssin
[24]
and
[4,
20],
resp
ecti
vely
,bu
ilds
asp
ecifi
c,us
ually
infin
ite,
non-
dete
rmin
isti
cpr
oces
s,th
atre
pres
ents
all
the
deri
vati
ons
ofth
eor
igin
alsy
stem
and
enjo
ysan
inte
rest
ing
univ
ersa
lpr
oper
ty.
We
plan
toca
ptur
eth
eun
fold
ing
con-
stru
ctio
nw
ithi
nou
rfr
amew
ork:
To
this
aim
,we
inte
ndto
gene
raliz
eth
eun
fold
ing
cons
truc
tion
toan
arbi
trar
yad
hesi
vegr
amm
ar,
poss
ibly
requ
irin
gso
me
furt
her
prop
erti
eson
the
unde
rlyi
ngad
hesi
veca
tego
ry.
Inpr
acti
ce,
ofte
nth
egr
amm
ars
whi
char
ede
sign
edto
mod
ela
give
nsy
stem
are
equi
pped
wit
hap
plic
atio
nco
ndit
ions
,as
defin
edfo
rex
ampl
ein
[10,
13].
The
seco
ndit
ions
allo
wre
stri
ctin
gth
eap
plic
atio
nof
rule
san
dhe
nce,
they
mod
elre
stri
cted
cont
rol
stru
ctur
es.S
ome
prel
imin
ary
resu
lts
show
that
posi
tive
and
nega
tive
appl
i-ca
tion
cond
itio
nsca
nbe
hand
led
byex
tra
rela
tion
sin
anST
S:th
eyco
nsti
tute
afir
stst
epto
war
dsth
ege
nera
lizat
ion
ofth
eth
eory
ofST
Ssto
this
rich
ercl
ass
ofsy
stem
s.O
ccur
renc
egr
amm
ars
and
Pet
rine
tsar
eal
read
ysi
mila
rre
pres
enta
tion
sof
apr
oces
s,as
they
shar
eth
ein
tuit
ion
ofa
caus
alre
lati
onan
dit
ems,
whi
chca
nbe
prod
uced
and
cons
umed
.Pet
rine
tsof
fera
wel
lfou
nded
theo
ryfo
rana
lysi
sand
henc
ea
tran
sfor
mat
ion
ofan
STS
toan
equi
vale
ntP
etri
net
isan
inte
rest
ing
chal
leng
e.T
rans
form
atio
nsfo
rgr
amm
ars
wit
hout
appl
icat
ion
cond
itio
nsw
ere
alre
ady
defin
ed,
e.g.
,in
[1].
The
inte
grat
ion
ofre
stri
cted
nega
tive
appl
icat
ion
cond
itio
nsw
ere
hand
led
byin
[5],
buta
nin
tegr
atio
nof
gene
rala
pplic
atio
nco
ndit
ions
asth
eyar
eus
edin
mos
tpr
acti
cale
xam
ples
wou
ldbe
ofm
uch
mor
eva
lue.
And
inde
ed,t
hegi
ven
defin
itio
nof
anST
San
dit
sre
lati
ons
com
bine
dw
ith
the
men
tion
edex
tens
ion
for
appl
icat
ion
cond
itio
nsse
ems
tobe
adeq
uate
tocr
eate
aneq
uiva
lent
Pet
rine
t.
Ack
now
ledg
emen
tsW
eac
know
ledg
eP
aolo
Bal
dan
and
the
anon
ymou
sre
fere
esfo
rco
nstr
ucti
veco
mm
ents
ona
prel
imin
iary
vers
ion
ofth
epa
per.
Ref
eren
ces
1.B
alda
n,P
.:M
odel
ling
conc
urre
ntco
mpu
tati
ons:
from
cont
extu
alP
etri
nets
togr
aph
gram
mar
s.P
hDdi
sser
tati
on,
Dep
artm
ent
ofC
ompu
ter
Scie
nce,
Uni
vers
ity
ofP
isa,
Mar
ch.
Ava
ilabl
eas
tech
nica
lrep
ortn
o.T
D-1
/00
(200
0)2.
Bal
dan,
P.,
Cor
radi
ni,A
.,H
eind
el,T
.,K
önig
,B.,
Sobo
cins
ki,P
.:P
roce
sses
for
adhe
sive
rew
riti
ngsy
stem
s.In
:Ace
to,L
.,In
gólf
sdót
tir,
A.(
eds.
)F
oSSa
CS,
vol.
3921
ofL
ectu
reN
otes
inC
ompu
ter
Scie
nce,
pp.2
02–2
16.S
prin
ger
Ver
lag
(200
6)
Subo
bjec
ttra
nsfo
rmat
ion
syst
ems
419
3.B
alda
n,P
.,C
orra
dini
,A.,
Mon
tana
ri,U
.:C
onca
tena
ble
grap
hpr
oces
ses:
rela
ting
proc
esse
san
dde
riva
tion
trac
es.
In:
Pro
c.of
ICA
LP
’98,
vol.
1443
ofL
ectu
reN
otes
inC
ompu
ter
Scie
nce,
pp.2
83–2
95.S
prin
ger
Ver
lag
(199
8)4.
Bal
dan,
P.,
Cor
radi
ni,
A.,
Mon
tana
ri,
U.:
Unf
oldi
ngof
doub
le-p
usho
utgr
aph
gram
mar
sis
aco
refle
ctio
n.In
:E
hrig
,G
.,E
ngel
s,G
.,K
reow
ski,
H.J
.,R
ozen
berg
,G
.(e
ds.)
Pro
ceed
ings
ofth
eIn
tern
atio
nal
Wor
ksho
pon
The
ory
and
App
licat
ion
ofG
raph
Tra
nsfo
rmat
ions
,vo
l.17
64of
Lec
ture
Not
esin
Com
pute
rSc
ienc
e,pp
.145
–163
.Spr
inge
rV
erla
g(1
999)
5.B
alda
n,P
.,K
önig
,B
.,St
ürm
er,
I.:
Gen
erat
ing
test
case
sfo
rco
dege
nera
tors
byun
fold
ing
grap
htr
ansf
orm
atio
nsy
stem
s.In
:Ehr
ig,H
.,E
ngel
s,G
.,P
aris
i-P
resi
cce,
F.,
Roz
enbe
rg,G
.(ed
s.)
ICG
T’0
4,vo
l.32
56of
Lec
ture
Not
esin
Com
pute
rSc
ienc
e,pp
.194
–209
.Spr
inge
rV
erla
g(2
004)
6.C
orra
dini
,A.,
Hei
ndel
,T.,
Her
man
n,F
.,K
önig
,B.:
Sesq
ui-p
usho
utre
wri
ting
.In:
Cor
radi
ni,A
.,E
hrig
,H.,
Mon
tana
ri,U
.,R
ibei
ro,L
.,R
ozen
berg
,G.(
eds.
)IC
GT
’06,
vol.
4178
ofL
ectu
reN
otes
inC
ompu
ter
Scie
nce,
pp.3
0–45
.Spr
inge
rV
erla
g(2
006)
7.C
orra
dini
,A.,
Mon
tana
ri,U
.,R
ossi
,F.:
Gra
phpr
oces
ses.
Fun
d.In
form
.26,
241–
265
(199
6)8.
Cor
radi
ni,A
.,M
onta
nari
,U.,
Ros
si,F
.,E
hrig
,H.,
Hec
kel,
R.,
Löw
e,M
.:A
lgeb
raic
appr
oach
esto
grap
htr
ansf
orm
atio
n,P
artI
:bas
icco
ncep
tsan
ddo
uble
push
outa
ppro
ach.
In:R
ozen
berg
[21]
,C
hapt
er3
(199
7)9.
Dan
os,V
.,K
rivi
ne,J
.,So
boci
nski
,P.:
Gen
eral
reve
rsib
ility
.In:
Exp
ress
’06,
Ele
ctro
nic
Not
esin
The
oret
ical
Com
pute
rSc
ienc
e17
5(3)
,pp.
75–8
6.E
lsev
ier
(200
7)10
.E
hrig
,H.,
Ehr
ig,K
.,P
rang
e,U
.,T
aent
zer,
G.:
Fun
dam
enta
lsof
Alg
ebra
icG
raph
Tra
nsfo
rma-
tion
.EA
TC
SM
onog
raph
sin
The
oret
ical
Com
pute
rSc
ienc
e.Sp
ring
erV
erla
g(2
006)
11.
Ehr
ig,
H.,
Hec
kel,
R.,
Kor
ff,
M.,
Löw
e,M
.,R
ibei
ro,
L.,
Wag
ner,
A.,
Cor
radi
ni,
A.:
Alg
ebra
icap
proa
ches
togr
aph
tran
sfor
mat
ion
II:
sing
lepu
shou
tap
proa
chan
dco
mpa
riso
nw
ith
doub
lepu
shou
tapp
roac
h.In
:Roz
enbe
rg[2
1],C
hapt
er4
(199
7)12
.G
olz,
U.,
Rei
sig,
W.:
The
non-
sequ
enti
albe
havi
our
ofP
etri
nets
.Inf
.Con
trol
57,1
25–1
47(1
983)
13.
Hab
el,
A.,
Hec
kel,
R.,
Tae
ntze
r,G
.:G
raph
gram
mar
sw
ith
nega
tive
appl
icat
ion
cond
itio
ns.
Spec
iali
ssue
ofF
und.
Info
rm.2
6(3,
4),2
87–3
13(1
996)
14.
Joya
l,A
.,St
reet
,R.:
The
geom
etry
ofte
nsor
calc
ulus
.I.A
dv.M
ath.
88,5
5–11
2(1
991)
15.
Kre
owsk
i,H
.-J.:
Man
ipul
atio
nvo
nG
raph
man
ipul
atio
nen.
PhD
thes
is,
Tec
hnis
che
Uni
vers
ität
Ber
lin(1
977)
16.
Lac
k,S.
,Sob
ocin
ski,
P.:
Adh
esiv
ean
dqu
asia
dhes
ive
cate
gori
es.T
heor
.Inf
.App
l.39
(2),
511–
546
(200
5)17
.L
eins
ter,
T.:
Hig
her
Ope
rads
,H
ighe
rC
ateg
orie
s.L
ondo
nM
athe
mat
ical
Lec
ture
Not
es.
Cam
brid
geU
nive
rsit
yP
ress
(200
3)18
.M
eseg
uer,
J.,M
onta
nari
,U.:
Pet
rine
tsar
em
onoi
ds.I
nfor
m.a
ndC
ompu
t.88
,105
–155
(199
0)19
.R
eisi
g,W
.:P
etri
Net
s:A
nIn
trod
ucti
on.E
AC
TS
Mon
ogra
phs
onT
heor
etic
alC
ompu
ter
Scie
nce.
Spri
nger
Ver
lag
(198
5)20
.R
ibei
ro,
L.:
Par
alle
lC
ompo
siti
onan
dU
nfol
ding
Sem
anti
csof
Gra
phG
ram
mar
s.P
hDth
esis
,T
echn
isch
eU
nive
rsit
ätB
erlin
(199
6)21
.R
ozen
berg
,G.(
ed.)
Han
dboo
kof
Gra
phG
ram
mar
san
dC
ompu
ting
byG
raph
Tra
nsfo
rmat
ion,
Vol
.1:F
ound
atio
ns.W
orld
Scie
ntifi
c(1
997)
22.
Roz
enbe
rg,
G.,
Eng
elfr
iet,
J.:
Ele
men
tary
net
syst
ems.
In:
Rei
sig,
W.,
Roz
enbe
rg,
G.
(eds
.)L
ectu
res
onP
etri
Net
sI:
Bas
icM
odel
s,vo
l.14
91of
Lec
ture
Not
esin
Com
pute
rSc
ienc
e,pp
.12–
121.
Spri
nger
Ver
lag
(199
6)23
.St
reet
,R.:
Hig
her
cate
gori
es,s
trin
gs,c
ubes
and
sim
plex
equa
tion
s.A
ppl.
Cat
eg.S
truc
ture
s.3,
29–7
7(1
995)
24.
Win
skel
,G.:
Eve
ntst
ruct
ures
.In:
Pet
riN
ets:
App
licat
ions
and
Rel
atio
nshi
psto
Oth
erM
odel
sof
Con
curr
ency
,vol
.255
ofL
ectu
reN
otes
inC
ompu
ter
Scie
nce,
pp.3
25–3
92.S
prin
ger
Ver
lag
(198
7)
