Database Reference
In-Depth Information
n T s E (p i + 1 ) ,...,
T s E (p i + n )
=+
= T s E
n (p i + 1 ,...,p i + n ) .
Thus, the replacing of the non-flattened equation
p i =
n ass(p i + 1 ).p i + 1 ,...,ass(p i + n ).p i + n
n (p i + 1 ,...,p i + n ))
with the flattened equation (p 1 =
E is valid.
=
=
Consider that, from the fact that ass(p i + k )
ass(p i ) for k
1 ,...,n , each state-
ass(p i + k )
p i + k is the instance-database of a schema
transition p i
in G and hence
this state-transition corresponds to an identity schema mapping for
A
. Thus, this
transition does not change this node state ass(p i ) (i.e., instance-database of
A
), that
is, such an action is without any effect, and hence we can extend the diagram on the
left into the (equivalent to it (up to bisimulation)) diagram on the right.
A
In an abstract algebra, a congruence relation (or simply congruence) is an equiv-
alence relation on an algebraic structure that is compatible with the structure. Every
congruence relation has a corresponding quotient structure, whose elements are the
equivalence classes (or congruence classes) for the relation.
We are interested in the congruences on the set of terms in
T P X that can be
generated from the set of equations in E . Let us denote a congruence relation by
≡⊆ T P X
× T P X , which is an equivalence relation on
T P X , so that: if (t 1 ,t 2 )
E
∈≡
(written also as t 1
then (t 1 ,t 2 )
t 2 ), and for each n -ary algebraic operation σ
t i implies σ(t 1 ,...,t n )
σ(t 1 ,...,t n ) .
in the signature Σ P , t i
is a congruence relation if it is an equivalence relation (which includes
equations in E ) and a subalgebra of the product
Thus,
× T P X .
The set of congruences of an algebraic system is a complete lattice. The meet is
the usual set intersection. The join (of an arbitrary number of congruences) is the
join of the underlying equivalence relations. This join corresponds to the subalgebra
(of
T P X
× T P X ) generated by the union of the underlying sets of the congruences.
In what follows, we are interested in a particular congruence based on the
guarded set of equations E on
T P X
T P X and the equivalence classes with representa-
tion elements in X .
Given a guarded equation (p k =
t)
E , where p k
X
T P X and t
T P X ,we
denote the equivalence class equal to the set of terms
{
t
T P X
|
p k =
t
}
by
[
p k ] E ,
so that p k ∈[
p k ] E , as follows:
Definition 55
T P X , of a program P
obtained from the algorithm DBprog , we define the following set of equivalence
classes in
For a given guarded set of equations E on
T P X :
1. The equivalence class
p k ] E of p k T P X determined by the guarded set of equa-
tions in E , for each variable p k
[
X
T P X , with k
1.
2. The last equivalence class
[
p 0 ] E = T P X
\
D , for the variable p 0
X , where D
=
p k X,k 1 [
p k ] E .
Search WWH ::




Custom Search