Information Technology Reference
In-Depth Information
iff
Λ
with the
RIV1
is syntactically unifiable. We construct a finite set of in-
dividual terms
consisting of a new individual constant
c
, exactly one term of
the form
h
(
y
1
,...,y
n
) for each fixed arity
h
I
∈IF
un
(
Γ
) such that
n
=
A
r
(
h
)
and
y
1
,...,y
n
are distinct individual variables new for
I
and
Λ
,andexactly
one term of the form
h
(
x
) for each flexible arity
h
∈IF
un
(
Γ
) such that
x
is a
sequence variable new for
I
and
Λ
.
?
∅
Theorem 2.
Let
Λ
have the form
{
s
≈
t
}
with
IV
ar
(
Λ
)=
{
x
1
,...,x
n
}
and
Fix
g
r
(
g
)=
n
+1
.Then
Λ
with the
RIV1
is
syntactically unifiable iff there exist
r
1
,...,r
n
∈I
∈F
be a new symbol with
A
such that the general syntac-
tic unification problem (without sequence function symbols)
{
g
(
s, x
1
,...,x
n
)
≈
?
∅
g
(
t, r
1
,...,r
n
)
}
is unifiable.
Thus, we have to show that unifiability of a general syntactic unification
problem
∆
without sequence function symbols is decidable. We assume that
F
,otherwise
∆
would be a Robinson unification problem. We trans-
form
∆
performing the following steps: (1) Introduce a new flat symbol
seq
lex
(
∆
)
=
∅
∈
Flex
Ind
Fix
Ind
F
. (2) Introduce a new unary symbol
g
f
∈F
for each
f
∈F
lex
(
∆
). (3)
Replace each term
f
(
r
1
,...,r
m
),
m
0, in
∆
by
g
f
(
seq
(
r
1
,...,r
m
)).
The transformation yields a new general flat unification problem
Θ
. Sequence
variables occur in
Θ
only as arguments of terms with the head
seq
.Weimpose
the
second restriction on individual variables
,
RIV2
,on
Θ
demanding that, for
any
F
-unifier
ϑ
of
Θ
and for any
x
≥
∈V
Ind
,
H
ead
(
xϑ
)
=
seq
.
Theorem 3.
∆
is syntactically unifiable iff
Θ
with the
RIV2
is
F
-unifiable.
Remark 2.
F
-unifiability of
Θ
without the
RIV2
does not imply syntactic unifi-
ability of
∆
:Let
∆
be
?
∅
Flex
.Then
Θ
=
?
F
{
f
(
x
)
≈
f
(
a, b
)
}
,
f
∈F
{
g
f
(
seq
(
x
))
≈
g
f
(
seq
(
a, b
))
}
. Obviously
∆
is not unifiable, while
{
x
→
seq
(
a, b
)
}
is an
F
-unifier
of
Θ
, because
seq
(
seq
(
a, b
))
≈
F
seq
(
a, b
).
Next, our goal is to construct a general
F
-unification problem that is
F
-
unifiable (without restrictions) iff
Θ
with the
RIV2
is
F
-unifiable. First, we
construct a finite set
of individual terms consisting of a new individual con-
stant
d
and exactly one term of the form
h
(
y
1
,...,y
n
)foreach
h
J
∈F
ix
(
Θ
)such
that
n
=
A
r
(
h
)and
y
1
,...,y
n
are distinct individual variables new for
J
and
Θ
.
Theorem 4.
Let
Θ
be
{
s
≈
?
F
t
}
with
IV
ar
(
Θ
)=
{
x
1
,...,x
n
}
and
h
∈F
Fix
be a new symbol with
r
(
h
)=
n
+1
.Then
Θ
with the
RIV2
is
F
-unifiable iff
for some
r
1
,...,r
n
∈J
A
?
F
the general
F
-unification problem
{
h
(
s, x
1
,...,x
n
)
≈
h
(
t, r
1
,...,r
n
)
}
is
F
-unifiable.
Thus, we are left with proving that unifiability of an
F
-unification problem
Φ
, whose signature consists of fixed arity individual function symbols and the
only flexible arity flat individual function symbol
seq
, is decidable.
Let
Ψ
be an
F
-unification problem obtained from
Φ
by replacing each
x
∈
SV
ar
(
Φ
) with a new individual variable
x
Ψ
. It is easy to see that
Φ
is unifiable
Search WWH ::
Custom Search