Database Reference
In-Depth Information
a
s
with
a
Act
, where
s,s
∈
Definition 47
A transition is a triple
s
∈
S
.An
LTS is a (possibly infinite) set of transitions.
An LTS is finitely branching if each of its states has only finitely many outgoing
transitions.
General Preliminary Considerations
In this section, we consider the programs for
execution of the schema-database mappings in a given schema database-mapping
system given by a graph
G
as defined in Definition
14
of Sect.
2.6
. Obviously,
the programming language for the mapping system in a graph
G
is different from
the low-level programming “select-project-join
union” language (SPJRU lan-
guage [
1
], with the signature
Σ
R
used in order to define the queries
q(
x
)
in the im-
plications of an SOtgd
Φ
of each schema-database mapping
+
M
AB
={
}:
A
→
B
Φ
(see Proposition
27
and Corollaries
18
,
19
in Sect.
5.4
).
Consequently, the programming language signature
Σ
P
here is different from the
relational algebra signatures
Σ
R
and
Σ
RE
(in Definition
31
) and used for algebraic
and coalgebraic considerations in Sect.
8.3
. The signature
Σ
P
will have, as we will
see in what follows, a number of constants (i.e., actions in
Act
), only one unary
operation to stop execution of programs, and two binary operators for the sequential
and parallel execution of the database mapping programs. Now we can define a
process graph, as follows:
Definition 48
A process graph
P
is an LTS in which one state
s
∈
S
is elected to
a
a
B
, then
P
P
where
P
be the root. If the LTS contains a transition
A
has a root state
s
.
•
A process
P
0
is finite if there are only finitely many sequences
a
1
a
2
a
k
P
1
···
P
k
.
P
0
•
A process
P
0
is regular if there are only finitely many processes
P
k
such that
P
0
a
1
a
2
a
k
P
1
···
P
k
.
The signature of a basic framework for a database-mapping
process algebra
con-
sists of a given set of states
S
and the following operators:
•
First of all, we assume a finite nonempty set
Act
of atomic actions, representing
indivisible behavior. Each action
a
∈
Act
is constant (nullary operation) that can
execute itself, after which it terminates successively.
•
We assume a binary operator '
' called
branching
(parallel) composition. If two
terms
t
1
and
t
2
represent processes
P
1
and
P
2
, respectively, then the term
t
1
t
2
(the infix notation for
(t
1
,t
2
)
) represents the process that executes in parallel
both processes
P
1
and
P
2
. In other words, the process graph of
t
1
t
2
is obtained
by joining
P
1
and
P
2
at their root states. It is a commutative and associative
operator.
•
We assume a set of unary operators '
a.
_' called
action prefixing
composition
with
a
∈
Act
is an action then
the term
a.t
1
represents the process that executes the action
a
and then the process
Act
.Ifaterm
t
1
represents a process
P
1
and
a
∈
