Database Reference
In-Depth Information
id
X
#
,
K
id
X
#
=
(t
1
,t
2
)
id
X
#
(t
2
)
∈
T
P
X
×
T
P
X
|
id
X
#
(t
1
)
=
=
(t
1
,t
2
)
g
E
(t
2
)
,
g
E
(t
1
)
∈
T
P
X
×
T
P
X
|
=
is the
congruence relation
, defined by
t
1
≡
K
id
X
#
,ofthesame
process-program (specified by
g
E
) with the following equivalence classes, such that
for a given variable
p
k
∈
t
2
iff
(t
1
,t
2
)
∈
X
⊆
T
P
X
(from Proposition
34
),
t
p
k
t
K
id
X
#
g
E
(t)
g
E
(p
k
)
[
p
k
]=
∈
T
P
X
|
=
=
=
∈
T
P
X
|
(p
k
,t)
∈
={
t
∈
T
P
X
|
t
≡
p
k
}
.
This congruence relation
≡
has a corresponding quotient structure, denoted by
T
P
X
≡
as it was specified in Definition
55
, whose elements are the equivalence
classes (or congruence classes).
The general notion of a congruence relation can be given a formal definition in
the context of
universal algebra
, a field which studies ideas common to all algebraic
structures. In this setting, a congruence relation is an equivalence relation
on an
algebraic structure that satisfies for each
n
-ary operator
o
i
∈
Σ
P
,
o
i
(t
1
,...,t
n
)
=
o
i
(t
1
,...,t
n
)
for any
n
-ary operation
o
i
∈
≡
Σ
P
and all terms
t
1
,...,t
n
,t
1
,...,t
n
sat-
t
i
for each 1
isfying
t
i
≡
n
.
Generally, this duality between the specification and the solution of the programs
can be represented by the following table:
≤
i
≤
initial
final
description
X
program variables—states
S
×
coproduct—product in
Set
∅
1
initial—terminal object in
Set
Σ
P
B
P
signature—behavior
syntax monad—observational comonad
T
P
D
P
T
P
X
D
P
S
lfp of
X
Σ
P
—gfp of
S
×
B
P
functors
(
T
P
X,
I
)
(
D
P
,
B
)
initial algebra—final coalgebra
g
E
@
=
ass
=
id
X
#
[
_
]
program specification—solution homomorphism
K
id
X
#
K
ass
congruence—bisimulation relation
7.5
Semantic Adequateness for the Operational Behavior
Z
is
adequate
w.r.t. an operational semantics if it determines the operational behavior of the pro-
gram up to observational equivalence.
A denotational model
(X
Σ
P
)
-algebra
[
f,h
]:
X
Σ
P
(Z)
