Information Technology Reference
In-Depth Information
The paper is organized as follows: In Section 2 basic notions are introduced.
In Section 3 decidability is proved. In Section 4 relation with order-sorted higher-
order
E
-unification is discussed. In Section 5 the unification procedure is defined
and its properties are studied. In Section 6 some of the related work is reviewed.
A longer version of this paper with full proofs is available on the web [12].
2
Preliminaries
We assume that the reader is familiar with the standard notions of unification
theory [3]. We consider an alphabet consisting of the following pairwise disjoint
sets of symbols: individual variables
V
Ind
, sequence variables
V
Seq
,fixedarityin-
Fix
Flex
Ind
dividual function symbols
F
Ind
, flexible arity individual function symbols
F
,
Fix
fixed arity sequence function symbols
F
Seq
, flexible arity sequence function sym-
Flex
bols
Seq
. Each set of variables is countable. Each set of function symbols is
finite or countable. Besides, the alphabet contains the parenthesis '(', ')' and
the comma ','. We will use the following denotations:
F
V
V
Ind
∪V
Seq
;
F
Ind
:=
:=
F
Ind
∪F
Fix
Flex
Ind
;
F
Seq
:=
F
Seq
∪F
Fix
Flex
Seq
;
F
Fix
:=
F
Ind
∪F
Fix
Seq
;
Fix
F
Flex
:=
F
Ind
∪F
Flex
Flex
Seq
;
Fix
Flex
.The
arity
of
f
Fix
is denoted by
F
:=
F
Ind
∪F
Seq
=
F
∪F
∈F
A
r
(
f
). A
Fix
is called a
constant
if
function symbol
c
∈F
A
r
(
c
)=0.
Definition 1.
A
term
over
F
and
V
is either an
individual
or a
sequence
term
defined as follows:
1. If
t
∈V
Ind
(resp.
t
∈V
Seq
), then
t
is an individual (resp. sequence) term.
2. If
f
0
,and
t
1
,...,t
n
are individual
terms, then
f
(
t
1
,...,t
n
)
is an individual (resp. sequence) term.
3. If
f
∈F
Ind
(resp.
f
Fix
∈F
Fix
A
r
(
f
)=
n
,
n
≥
Seq
),
Flex
Ind
Flex
Seq
0)
are individual or
sequence terms, then
f
(
t
1
,...,t
n
)
is an individual (resp. sequence) term.
∈F
(resp.
f
∈F
)and
t
1
,...,t
n
(
n
≥
The
head
of a term
t
=
f
(
t
1
,...,t
n
), denoted by
H
ead
(
t
), is the function
symbol
f
.Wedenoteby
), respectively, the
sets of all individual terms, all sequence terms, and all terms over
T
Ind
(
F
,
V
),
T
Seq
(
F
,
V
), and
T
(
F
,
V
F
and
V
.An
equation
over
F
and
V
is a pair
s, t
, denoted by
s
≈
t
,where
s, t
∈T
Ind
(
F
,
V
).
Flex
Ind
Fix
Flex
Fix
Example 1.
Let
x, y
∈V
Ind
,
x
∈V
Seq
,
f
∈F
,
g
∈F
Ind
,
f
∈F
Seq
,
g
∈F
Seq
,
A
r
(
g
)=1.Then
f
(
x, g
(
x, y
)) and
f
(
x, f
(
x, x, y
)) are indi-
vidual terms;
f
(
x, f
(
x, x, y
)) and
g
(
f
(
x, x, y
)) are sequence terms;
f
(
x, g
(
x
)),
f
(
x, g
(
x, y
)) and
f
(
x, g
(
x, y
)) are not terms;
f
(
x, g
(
x, y
))
r
(
g
) = 2, and
A
≈
g
(
x, y
)isanequa-
tion;
f
(
x, g
(
x, y
))
≈
g
(
x, y
),
x
≈
f
(
x
)and
g
(
x
)
≈
f
(
x
)arenotequations.
If not otherwise stated, the following symbols, maybe with indices, are used
as metavariables:
x
and
y
- over individual variables;
x
,
y
,
z
- over sequence
variables;
v
- over (individual or sequence) variables;
f
,
g
,
h
- over individ-
ual function symbols;
f
,
g
,
h
- over sequence function symbols;
a
,
b
,
c
-over
individual constants;
a
,
b
,
c
- over sequence constants;
s
,
t
,
r
,
q
-overterms.
Let
T
be a term, a sequence of terms, or a set of terms. Then we denote by
IV
ar
(
T
)(resp.by
SV
ar
(
T
)) the set of all individual (resp. sequence) variables
Search WWH ::
Custom Search