Information Technology Reference
In-Depth Information
where
forward
))
succ
=
df
(
succ
1
(
true
forward
))
error
=
df
(
error
1
(
true
((
v
=
v
)
forward
)
rollback
=
df
true
∧¬
where
stands for the disjoint parallel operator [14]
(
b
R
)
(
c
S
)=
df
(
b
∧
c
)
(
R
∧
S
)
We introduce the following mappings to link the design matrix model with the
design model. For any design
D
and design matrix
Q
, define
G
(
D
)=
df
H
(
D
;
succ
)
(
v
=
v
))
F
(
Q
)=
df
Q
[
true, false/forward, eflag
]; ((
forward
∧¬
eflag
)
Theorem 3.5
⎛
⎞
eflag
∧
forward
)
b
(
R
∧¬
⎝
⎠
true
true
(1)
G
(
b
R
)=
⎛
⎞
c
1
S
1
⎝
⎠
(2)
F
c
2
S
2
=(
c
1
∧¬
c
2
∧¬
c
3
)
S
1
c
3
S
3
G
distributes over the standard programming combinators.
Theorem 3.6
(Homomorphism)
(1)
G
(
D
1
;
D
2
)=
G
(
D
1
);
G
(
D
2
)
(2)
G
(
D
1
D
2
)=
G
(
D
1
)
G
(
D
2
)
(3)
G
(
D
1
b
D
2
)=
G
(
D
1
)
b
G
(
D
2
) provided that
b
is well-defined.
Proof
G
(
D
1
b
D
2
)
{
Def of
G}
=
H
((
D
1
b
D
2
);
succ
)
{
; distributes over
b
}
=
H
((
D
1
;
succ
)
b
(
D
2
;
succ
))
{
Theorem 3.4
}
=
G
(
D
1
)
b
G
(
D
2
)
F
form a retraction
Theorem 3.7
(Retraction)
(
F,
and
G
G
) is a Galois connection, satisfying
(1)
F
(
G
(
D
)) =
D
(2)
G
(
F
(
Q
)
Q
Search WWH ::
Custom Search