Information Technology Reference
In-Depth Information
However, almost disjointness does not imply minimality: Again, take the set
{
in Example 7. On the other hand, minimality does not imply almost
disjointness: Let
σ
=
σ, η
}
{
x
→
f
(
a, y
)
}
,
ϑ
=
{
x
→
f
(
y, b
)
}
,
X
=
{
x
}
,
Q
=
∅
,and
E
=
∅
.Then
{
σ, ϑ
}
is minimal but not almost disjoint with respect to
X
and
Q
X,Q
E
X,Q
E
modulo
E
, because
σ
=
ϑ
.
The same example can be used to show that almost minimality does not imply
almost disjointness either. From these observations we can also conclude that
neither minimality nor almost minimality imply disjointness.
The equational theory
E
=
ϕ
and
ϑ
ϕ
,with
ϕ
=
{
x
→
f
(
a, b
)
}
, but
σ
is called the
free theory with sequence variables
and sequence function symbols
. Unification in the free theory is called the
syn-
tactic sequence unification
.Thetheory
E
=
∅
that we
first encountered in Example 5 is called
the flat theory
,where
f
is the flat flexible
arity individual function symbol. We call unification in the flat theory the
F
-
unification
. Certain properties of this theory will be used in proving decidability
of the syntactic sequence unification.
{
f
(
x, f
(
y
)
, z
)
≈
f
(
x, y, z
)
}
3
Decidability and Unification Type
We show decidability of a syntactic sequence unification problem in three steps:
First, we reduce the problem by unifiability preserving transformation to a uni-
fication problem containing no sequence function symbols. Second, applying yet
another unifiability preserving transformation we get rid of all free flexible arity
(individual) function symbols, obtaining a unification problem whose signature
consists of fixed arity individual function symbols and one flat flexible arity in-
dividual function symbol. Finally, we show decidability of the reduced problem.
Let
Γ
be a general syntactic sequence unification problem and let
Q
=
SF
. We transform
Γ
performing the following steps: (1)
Introduce for each
n
-ary
f
un
(
Γ
). Assume
Q
=
∅
Fix
∈Q
anew
n
-ary symbol
g
f
∈F
Ind
. (2) Introduce
for each flexible arity
f
Ind
. (3) Replace
each sequence function symbol
f
in
Γ
with the corresponding
g
∈Q
a new flexible arity symbol
g
f
∈F
Flex
.
The transformation yields a new unification problem
Λ
that does not con-
tain sequence function symbols. We impose the
first restriction on individual
variables
,shortly
RIV1
,on
Λ
demanding that for any syntactic unifier
λ
of
Λ
and for any
x
f
ead
(
xλ
) must be different from any newly introduced
individual function symbols.
∈V
Ind
,
H
Theorem 1.
Γ
is syntactically unifiable iff
Λ
with the
RIV1
is syntactically
unifiable.
Remark 1.
Unifiability of
Λ
without the
RIV1
does not imply unifiability of
Γ
:
Let
Γ
be
?
∅
?
∅
{
f
(
x
)
≈
f
(
c
)
}
.Then
Λ
=
{
f
(
x
)
≈
f
(
c
c
)
}
.
Γ
is not unifiable, while
{
x
→
c
c
}
is a unifier of
Λ
, because
x
∈V
Ind
can be bound with
c
c
∈T
Ind
(
F
,
V
).
Next, our goal is to construct a general syntactic sequence unification prob-
lem without sequence function symbols that is unifiable (without restrictions)
Search WWH ::
Custom Search