Information Technology Reference
In-Depth Information
5.1
Soundness, Completeness and Almost Minimality
In this section we assume that
un
(
Γ
)forasyntactic
sequence unification problem
Γ
. The soundness theorem is not hard to prove:
X
=
V
ar
(
Γ
)and
Q
=
SF
+
Theorem 6 (Soundness).
If
∈U
∅
(
Γ
)
.
Completeness can be proved by showing that for any unifier
ϑ
of
Γ
there
exists a derivation from
Γ
;
ε
=
⇒
∅
;
ϑ
,then
ϑ
that terminates with success and the substitution
in the last system of the derivation is strongly more general than
ϑ
:
Γ
;
ε
Lemma 1.
For any
ϑ
∈U
∅
(
Γ
)
there exists a derivation of the form
Γ
0
;
σ
0
⇒
X
=
Γ
1
;
σ
1
⇒
BT
Γ
2
;
σ
2
⇒
BT
···
⇒
BT
∅
;
σ
n
with
Γ
1
=
Γ
and
σ
1
=
ε
such
=
=
=
then
X
=
P
,otherwise
X
=
BT
,and
σ
n
X,Q
∅
that if
ϑ
is erasing on
X
ϑ
.
X,
E
⊆≤
X,Q
From Theorem 6, Lemma 1, and the fact that
, by Defini-
E
tion 17 and Definition 15 we get the completeness theorem:
Theorem 7 (Completeness).
S
ol
∅
(
Γ
)
is a complete set of unifiers of
Γ
.
The set
S
ol
∅
(
Γ
), in general, is not minimal with respect to
V
ar
(
Γ
)and
?
∅
SF
un
(
Γ
) modulo the free theory. Just consider
Γ
=
{
f
(
x
)
≈
f
(
y
)
}
,then
S
ol
∅
(
Γ
)=
{{
x
→
y
}
,
{
x
→
, y
→
}}
. However, it can be shown that
S
ol
∅
(
Γ
) is almost minimal. In fact, the following stronger statement holds:
Theorem 8 (Almost Disjointness).
S
ol
∅
(
Γ
)
is almost disjoint wrt
X
and
Q
.
Theorem 7, Theorem 8 and Proposition 2 imply the main result of this sec-
tion:
Theorem 9 (Main Theorem).
S
ol
∅
(
Γ
)=
amcu
∅
(
Γ
)
.
6
Conclusions and Related Work
We showed that general syntactic unification with sequence variables and se-
quence functions is decidable and has the infinitary type. We developed a unifi-
cation procedure and showed its soundness, completeness and almost minimality.
Historically, probably the first attempt to implement unification with se-
quence variables (without sequence functions) was made in the system MVL [7].
It was incomplete because of restricted use of widening technique. The restriction
was imposed for the eciency reasons. No theoretical study of the unification
algorithm of
, to the best of our knowledge, was undertaken.
Richardson and Fuchs [16] describe another unification algorithm with se-
quence variables that they call vector variables. Vector variables come with their
length attached, that makes unification finitary. The algorithm was implemented
but its properties have never been investigated.
Implementation of first-order logic in
MVL
[14] is based on sequent cal-
culus formulated using sequence variables (on the meta level). Sequence meta-
variables are used to denote sequences of formulae, and individual meta-variables
Isabelle
Search WWH ::
Custom Search