Information Technology Reference
In-Depth Information
Sequence Variable Elimination 2 (SVE2):
{f
(
x, s
1
,...,s
n
)
≈
?
∅
f
(
t, t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
f
(
t
1
,...,t
m
)
ϑ}∪Γ
ϑ
;
σϑ
if
x∈SVar
(
t
)and
ϑ
=
{x → t}.
Widening 1 (W1):
{f
(
x, s
1
,...,s
n
)
≈
?
∅
{f
(
s
1
,...,s
n
)
ϑ ≈
?
∅
f
(
t, t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
f
(
t
1
ϑ,...,t
m
ϑ
)
}∪Γ
ϑ
;
σϑ
if
x∈SVar
(
t
)and
ϑ
=
{x →
t, x
}.
Widening 2 (W2):
{f
(
x, s
1
,...,s
n
)
≈
?
∅
{f
(
x, s
1
ϑ,...,s
n
ϑ
)
≈
?
∅
f
(
y, t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
?
∅
f
(
y, t
1
ϑ,...,t
m
ϑ
)
}∪Γ
ϑ
;
σϑ
{f
(
s
1
ϑ,...,s
n
ϑ
)
≈
where
ϑ
=
{
y
→
x, y
}
.
Splitting (Sp):
{f
(
x, s
1
,...,s
n
)
≈
?
∅
f
(
f
(
r
1
,...,r
k
)
,t
1
,...,t
m
)
}∪Γ
;
σ
=
⇒
f
(
f
2
(
r
1
,...,r
k
)
,t
1
,...,t
m
)
ϑ}∪Γ
ϑ
;
σϑ
if
x∈SVar
(
f
(
r
1
,...,r
k
)) and
ϑ
=
{x → f
1
(
r
1
,...,r
k
)
}{f →
f
1
, f
2
}.
We may use the rule name abbreviations as subscripts, e.g.,
?
∅
{f
(
s
1
,...,s
n
)
ϑ ≈
Γ
1
;
σ
1
=
⇒
P
Γ
2
;
σ
2
for Projection. We may also write
Γ
1
;
σ
1
=
⇒
BT
Γ
2
;
σ
2
to indicate
that
by some
basic transformation
(i.e.,
non-projection) rule.
P
,
SVE2
,
W1
,
W2
,and
Sp
are non-deterministic rules.
A
derivation
is a sequence
Γ
1
;
σ
1
was transformed to
Γ
2
;
σ
2
of system trans-
formations. A derivation is
fair
if any transformation rule which is continuously
enabled is eventually applied. Any finite fair derivation
S
1
=
Γ
1
;
σ
1
=
⇒
Γ
2
;
σ
2
=
⇒ ···
⇒
S
2
=
⇒···
⇒
S
n
=
is maximal, i.e., no further transformation rule can be applied on
S
n
.
Definition 17.
A
syntactic sequence unification procedure
is any program that
takes a system
Γ
;
ε
as an input and uses the rules in
U
to generate a tree of
fair derivations, called the
unification tree for
Γ
,
UT
(
Γ
)
, in the following way:
1. The root of the tree is labeled with
;
2. Each branch of the tree is a fair derivation either of the form
Γ
;
ε
Γ
;
ε
=
⇒
P
Γ
1
;
σ
1
=
⇒
BT
Γ
2
;
σ
2
=
⇒
BT
···
or
Γ
;
ε
=
⇒
BT
Γ
1
;
σ
1
=
⇒
BT
.
The nodes in the tree are systems.
3. If several transformation rules, or different instances of the same transfor-
mation rule are applicable to a node in the tree, they are applied concurrently.
4. The decision procedure is applied to the root and to each node generated by a
non-deterministic transformation rule, to decide whether the node contains
a solvable unification problem. If the unification problem
∆
in a node
Γ
2
;
σ
2
=
⇒
BT
···
∆
;
δ
is unsolvable, then the branch is extended by
∆
;
δ
=
⇒
DP
⊥
.
The leaves of
UT
(
Γ
) are labeled either with the systems of the form
∅
;
σ
or with
⊥
. The branches of
UT
(
Γ
) that end with
∅
;
σ
are called
successful
branches
, and those with the leaves
⊥
are
failed branches
.Wedenoteby
S
ol
∅
(
Γ
)
the solution set of
Γ
, i.e., the set of all
σ
-s such that
∅
;
σ
is a leaf of
UT
(
Γ
).
Search WWH ::
Custom Search