Database Reference
In-Depth Information
in
G
OP
in the deletion case, respectively. Notice that
[
p
k
]=
(ass(p
k
),
∅
)
∈
S
×
P
fin
(Act
X)
if
S
(A,α
∗
)
is the empty set (there is no branch from this state).
In general, this transition relation is not well-founded since, for instance, the
cyclic database mapping programs
P
(that is, graphs
G
) are allowed.
The dual of foundation amounts to postulating that “the universe
V
×
=
P
S
(V )
is a final
P
S
-coalgebra”, which is equivalent to Peter Aczel's “anti-foundation ax-
iom” yielding non-well-founded sets [
2
]. Aczel's theory of non-well founded sets
was driven by the quest for a set-theoretic foundation for the abstract semantics of
Milner's CCS [
34
].
But one does not need to resort to non-standard foundation: as already clear
in [
2
], coinductive definitions can be founded on final coalgebras and these exist also
in the standard category
Set
of ordinary sets. What the anti-foundation axiom gives
is the non-standard fact that the greatest (strict) fixed point
gfp(F)
F(gfp(F))
of
an endofunctor
F
on
SET
is a final
F
-coalgebra, provided
F
satisfies some mild
conditions. In particular, the special final coalgebra theorem holds for the endofunc-
tor mapping a class
Y
to the class
=
Y)
having as elements (small) sets of
pairs
(a,y)
with
a
∈
A
and
y
∈
Y
. The behavior of CCS programs can be seen as
a coalgebra of this endofunctor by taking for
A
the set
Act
of actions performed by
programs.
If the anti-foundation axiom is not assumed then one cannot apply the special
final coalgebra theorem of Aczel in order to obtain final coalgebras from greatest
(strict) fixed points. The solution, adopted here, consists in taking the
finite
powerset
endofunctor
P
S
(A
×
P
fin
(Y)
of its finite subsets.
In particular, since each database mapping program (a graph
G
) has only finitely
many inter-schema mappings from a given database schema,
P
fin
:
Set
→
Set
mapping a set
Y
to the set
×
X)
, and it yields a semantics in the ordinary category
Set
of sets which is “almost”
the same as Aczel's one by
abstract
behavior endofunctor
[
p
k
]∈
S
×
P
fin
(Act
B
P
=
P
fin
(Act
×
:
_
)
Set
Set
(when we abstract from the names (states) of the programs involved in
the transitions and fo
cu
s to the actions which can be performed), and the general
behavior endofunctor
B
P
=
S
×
B
P
:
−→
(X)
.
The difference is in the fa
ct
that th
e
final c
oa
lgebra is an isomorphism (bij
ec
tion)
in
Set
, d
en
oted by
Set
−→
Set
, so that
[
p
k
]∈
S
×
B
P
B
:
gfp(B
P
)
→
B
P
(gfp(B
P
))
, rather than equality
gfp(B
P
)
=
B
P
(gfp(B
P
))
in
Set
.
Concretely, the final coalgebra for the behavior
S
×
B
P
is the set of rooted,
finitely branching trees, i.e., LTS with the
states
in
S
and labeled by the actions
a
∈
Act
, factored by the largest bisimulation relation. These (equivalence classes
of) trees can be seen as the
abstract
global behaviors corresponding, for a given
set
X
,to
B
P
(X)
=
P
fin
(Act
×
X)
: the root
A
=
ass(p
k
)
(of a process
p
k
)ofatree
L
A
∈
S
×
B
P
)
is the starting point of an abstract computation with behavior
B
P
. The quotient modulo bisimulation is needed in order to identify trees with
the
same paths
. (Notice that the bisimulations may be understood as coalgebraic dual
of 'algebraic' congruences, and they are relations which are closed under algebraic
operations).
gfp(
