Information Technology Reference
In-Depth Information
The formal denition of unication completeness requires some basic notions
related to unication wrt. equational theories. Let
E
be an equational theory,
i.e., a set of universally quantied equations. Two terms
s
and
t
are said to be
E-equal
, written
s
=
E
t
,i
s
=
t
is entailed by
E
plus the standard equality
axioms (2.18). A substitution
is called
E-unier
of
s
and
t
i
s
=
E
t
.A
set
cU
E
(
s; t
)of
E
-uniers of
s
and
t
is called
complete
if it contains, for each
E
-unier of
s
and
t
, a more or equally general substitution. That is to say, for
each substitution
such that
s
=
E
t
there exists some
0
2 cU
E
(
s; t
) with
(
0
E
)
j
Var
(
s
)
[Var
(
t
)
. Here,
Var
(
t
) denotes the set of variables occurring in
term
t
, and (
0
E
)
j
V
means the existence of a substitution
such that
(
0
=
E
)
j
V
. The latter holds i for each variable
x 2 V
the two terms (
x
0
)
and
x
are
E
-equal. A
unication complete theory
wrt.
E
is a consistent set
of formulas
E
containing the following:
1. The axioms in
E
.
2. The standard equality axioms (2.18).
3. Equational formulas, i.e., formulas with \ = " as the only predicate, such that
for any two terms
s
and
t
with variables
x
the following holds:
a) If
s
and
t
are not
E
-uniable, then
E
j
=
:9x: s
=
t
.
b) If
s
and
t
are
E
-uniable, then for each complete set of
E
-uniers
cU
E
(
s; t
),
2
3
_
4
s
=
t
5
E
j
=
8x
9y:
=
(2.19)
2cU
E
(
s;t
)
where
y
denotes the variables which occur in
=
but not in
x
.By
=
we denote the equational formula
x
1
=
t
1
^ :::^ x
n
=
t
n
constructed
from substitution
=
fx
1
7! t
1
;:::;x
n
7! t
n
g
.If
is the empty sub-
stitution, then
=
evaluates to formula
>
.
Unication wrt. theory AC1N is well-understood. Whether two terms are AC1N-
uniable is decidable in general, and uniable terms always admit a nite (but not
necessarily singleton) complete set of uniers. Several complete AC1-unication
algorithms are known. Extension to AC1N is straightforward. A unication com-
plete theory AC1N
can be obtained by computing, for any two terms
s; t
, some
complete set
cU
AC1N
(
s; t
) of AC1N-uniers and adding the corresponding equa-
tional formula which is to the right of the entailment symbol in (2.19). As a
small example, consider the terms
up
(
x
)
z
and
up
(
s
1
)
up
(
s
2
)
:
light
. The
set
ffx 7!
s
1
;z 7!
up
(
s
2
)
:
light
g; fx 7!
s
2
;z 7!
up
(
s
1
)
:
light
gg
is a com-
plete set of AC1N-uniers of these terms. According to (2.19), axioms AC1N
therefore entail
8x; z
[
up
(
x
)
z
=
up
(
s
1
)
up
(
s
2
)
:
light
x
=
s
1
^ z
=
up
(
s
2
)
:
light
_ x
=
s
2
^ z
=
up
(
s
1
)
:
light
]
Annotation 2.1.
Unication completeness.
Before entering the axiomatization of our action theory, we prove some
crucial properties of
EUNA
. These properties will be exploited later on to
model, on the term level, the subset relation and the two set operations
dierence and union.
