Information Technology Reference
In-Depth Information
Example 7.
Let
σ
=
{
x
→
y
}
,
ϑ
=
{
x
→
a, b
, y
→
a, b
}
,
η
=
{
x
→
, y
→
≤
X,Q
E
X,Q
E
≤
X,Q
E
X,Q
E
}
,
X
=
{
x, y
}
,
Q
=
∅
,
E
=
∅
.Then
σ
ϑ
,
σ
ϑ
,
σ
η
,
σ
η
.
A substitution
ϑ
is an
E
-instance
(resp.
strong
E
-instance
)of
σ
on
X
and
≤
X,Q
E
X,Q
E
≤
X,Q
E
Q
iff
σ
ϑ
(resp.
σ
ϑ
). The equivalence associated with
(resp.
) is denoted by =
X,Q
E
≈
X,Q
E
X,Q
E
≤
X,Q
E
with
(resp. by
). The strict part of
(resp.
X,Q
E
X,
E
⊆≤
X,Q
) is denoted by
<
X,Q
E
≺
X,Q
E
(resp.
). Definition 13 implies
.
E
S
Definition 14.
A set of substitutions
is called
minimal
(resp.
almost min-
X
Q
modulo
E
iff two distinct elements of
S
imal
) with respect to
and
are
≤
X,Q
E
X,Q
E
incomparable with respect to
(resp.
).
Minimality implies almost minimality, but not vice versa: A counterexample
is the set
{
σ, η
}
from Example 7.
Definition 15.
A
complete set of
E
-unifiers
of an
E
-unification problem
Γ
is
aset
S
of substitutions such that (1)
S⊆U
E
(
Γ
)
,and(2)foreach
ϑ
∈U
E
(
Γ
)
≤
X,Q
E
there exists
σ
∈S
such that
σ
ϑ
,where
X
=
V
ar
(
Γ
)
and
Q
=
SF
un
(
Γ
)
.
is a
minimal
(resp.
almost minimal
)
complete set of
E
-unifiers
of
Γ
,denoted
mcu
E
(
Γ
)
(resp.
amcu
E
(
Γ
)
) iff it is a complete set that is minimal
(resp. almost minimal) with respect to
The set
S
X
and
Q
modulo
E
.
Proposition 1.
An
E
-unification problem
Γ
has an almost minimal complete
set of
E
-unifiers iff it has a minimal complete set of
E
-unifiers.
. A minimal (resp.
almost minimal) complete set of
E
-unifiers of
Γ
, if it exists, is unique up to the
equivalence =
X,Q
E
If
Γ
is not
E
-unifiable, then
mcu
E
(
Γ
)=
amcu
E
(
Γ
)=
∅
≈
X,Q
E
(resp.
), where
X
=
V
ar
(
Γ
)and
Q
=
SF
un
(
Γ
).
?
∅
Example 8.
1.
Γ
=
{
f
(
x
)
≈
f
(
y
)
}
.Then
mcu
∅
(
Γ
)=
{{
x
→
y
}}
,
amcu
∅
(
Γ
)=
{{
x
→
y
}
,
{
x
→
, y
→
}}
.
2.
Γ
=
{
f
(
x, x, y
)
≈
?
∅
f
(
f
(
x
)
,x,a,b
)
}
.Then
mcu
∅
(
Γ
)=
amcu
∅
(
Γ
)=
{{
x
→
f
()
, x
→
, y
→
f
()
,a,b
}}
.
?
∅
3.
Γ
=
{
f
(
a, x
)
≈
f
(
x, a
)
}
.Then
mcu
∅
(
Γ
)=
amcu
∅
(
Γ
)=
{{
x
→
}
,
{
x
→
a
}
,
{
x
→
a, a
}
,...
}
.
?
∅
4.
Γ
=
{
f
(
x, y, x
)
≈
f
(
c, a
)
}
.Then
mcu
∅
(
Γ
)=
amcu
∅
(
Γ
)=
{{
x
→
, y
→
c, x
→
a
}
,
{
x
→
c, y
→
,x
→
a
}
,
{
x
→
c
1
, y
→
c
2
,x
→
a, c
→
c
1
, c
2
}}
.
Definition 16.
A set of substitutions
S
is
disjoint
(resp.
almost disjoint
)wrt
X
and
Q
modulo
E
iff two distinct elements in
S
have no common
E
-instance
(resp. strong
E
-instance) on
X
and
Q
, i.e., for all
σ, ϑ
∈S
,ifthereexists
ϕ
≤
X,Q
E
X,Q
E
≤
X,Q
E
X,Q
E
such that
σ
ϕ
(resp.
σ
ϕ
)and
ϑ
ϕ
(resp.
ϑ
ϕ
), then
σ
=
ϑ
.
Disjointness implies almost disjointness, but not vice versa: Consider again
the set
{
σ, η
}
in Example 7.
Proposition 2.
If a set of substitutions
S
is disjoint (almost disjoint) wrt
X
and
Q
modulo
E
, then it is minimal (almost minimal) wrt
X
and
Q
modulo
E
.
Search WWH ::
Custom Search