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
= 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