Database Reference
In-Depth Information
LTS (in Definitions
48
and the algorithm
DBprog
) up to the end of such a back-
ward/forward chaining, or up to the moment when the execution is stopped (by a
'nil' operation) by a DB administrator of this database mapping system.
From Proposition
35
, for a given database mapping graph
G
(a program), and
the a database-mapping
process-program P
, we have assignment of the process-
variables into the
states
,
ass
are the coalgebraic (ob-
servational) duals to the algebraic process variables in
X
of the guarded system of
equations
E
. For example, for a process
p
k
∈
:
X
→
S
(the 'states' in
S
X
, i.e., with a given state (instance
database)
A
=
ass(p
k
)
), and with its unique solution
T
(
s
E
(p
k
))
(from Proposi-
tion
37
),
p
k
represents the 'process in the state
A
'.
The operational
meaning
of this process
p
k
at the state
A
=
ass(p
k
)
, denoted by
[
Act
by passing then into the
corresponding set of processes
p
k
+
1
,p
k
+
2
,...
(specified by the algorithm
DBprog
and based on the set
S
(A,α
∗
)
during a forward propagation of database insertions,
and on the set
S
OP
p
k
]
, from above is to execute the set of actions
a
∈
(A,α
∗
)
during a backward propagation of database deletions).
Consequently, the meaning of a process
p
k
is that of a finitely branching LTS
with the root in the process
p
k
(at the state (instance-database)
A
=
ass(s
k
)
of
the schema
A
∈
V
G
, that is an object in
DB
), and with the set of transitions
a
i
p
k
+
i
|
{
p
k
1
≤
i
≤
n
}
, expressed equivalently by
(p
k
,
{
(a
1
,p
k
+
1
),...(a
n
,
p
k
+
n
)
}
)
∈
S
×
P
fin
(Act
×
X)
, where
P
fin
is a finite powerset operation (such that for
any set
Y
,
∅∈
P
fin
(Y)
, with
P
fin
(
∅
)
={∅}
) and '
×
' is the Cartesian product (such
that for any set
Y
,
Y
).
The meaning of the process denoted by the variable
p
k
at the state (instance-
database)
A
×∅=∅
ass(p
k
)
should abstract from the name of the process involved in
the transitions and focus to the actions which can be performed. It should be the
following 'coinductively' defined set of ordered pairs in the following two basic
cases (from Definition
54
and the algorithm
DBprog
), for the assignment
ass
=
:
X
→
S
, and branching
℘
:
X
→
P
fin
(Act
×
X)
, that is,
[
_
]=
ass,℘
(introduced by
Proposition
34
):
1. The meaning of an 'Insertion' process.
p
k
]=
ass(p
k
),℘ (p
k
)
=
ass(p
k
),
(A,p
k
+
1
),...(A,p
k
+
n
)
,
[
α
∗
(
with
ass(p
i
)
=
A
=
A
)
for
i
=
k,...,k
+
n
, where
n
=|
S
(A,α
∗
)
|≥
2, and
1
,...,n
;
2. The meaning of a 'Deletion' process (analogous).
[
p
k
+
i
]=
(ass(p
k
+
i
),
{
(a
i
,p
k
+
n
+
i
)
}
)
for
i
=
p
k
]=
ass(p
k
),℘ (p
k
)
=
ass(p
k
),
(A,p
k
+
1
),...(A,p
k
+
n
)
,
[
with
ass(p
i
)
=
A
=
α
∗
(
A
)
for
i
=
k,...,k
+
n
, where
n
=|
S
OP
(A,α
∗
)
|≥
2, and
1
,...,n
.
Note this direct connection of each possible action
a
i
in the state
A
with the inter-
schema mapping
[
p
k
+
i
]=
(ass(p
k
+
i
),
{
(a
i
,p
k
+
n
+
i
)
}
)
for
i
=
M
AB
i
B
i
,
i
A
=
1
,...,n
, in the database system given by a graph
OP
B
i
A
M
B
i
G
(a program) in the insertion case, and with the inter-schema mapping
A
