Information Technology Reference
In-Depth Information
The paper is organized as follows. Section 2 defines the pattern unification
algorithm, and in section 3 its correctness and completeness is proved. Section 4
presents the proof search algorithm, and again its correctness and completeness
is proved. The final section 5 contains what we have to say about extensions to
and
.
2
The Unification Algorithm
We work in the simply typed
-calculus, with the usual conventions. For instance,
whenever we write a term we assume that it is correctly typed. Substitutions
are denoted by
λ
ϕ, ψ, ρ
. The result of applying a substitution
ϕ
to a term
t
or a formula
, with the understanding that after the
substitution all terms are brought into long normal form.
Q
A
is written as
or
always denotes a
∀∃∀
-prefix, say
x y z
, with distinct variables. We call
x
the signature variables ,
y
the flexible variables and
z
the forbidden variables
of
Q
,andwrite
Q for the existential part
y
of
Q
.
Q
-terms are inductively defined by the following clauses.
-
If
u
is a universally quantified variable in
Q
or a constant, and
r
are
Q
-terms,
then
u r
is a
Q
-term.
-
For any flexible variable
y
and distinct forbidden variables
z
from
Q
,
y z
is
a
Q
-term.
-
If
r
is a
Q∀z
-term, then
λzr
is a
Q
-term.
Explicitely,
r
is a
Q
-term iff all its free variables are in
Q
, and for every subterm
y r
of
r
with
y
free in
r
and flexible in
Q
,the
r
are distinct variables either
λ
-bound in
r
(such that
y r
is in the scope of this
λ
) or else forbidden in
Q
.
Q
-goals and
Q
-clauses are simultaneously defined by
-
If
r
are
Q
-terms, then
P r
is a
Q
-goal as well as a
Q
-clause.
-
If
D
is a
Q
-clause and
G
is a
Q
-goal, then
D → G
is a
Q
-goal.
G
Q
D
Q
G → D
Q
-
If
is a
-goal and
is a
-clause, then
is a
-clause.
-
If
G
is a
Q∀x
-goal, then
∀xG
is a
Q
-goal.
-
If
D
[
y
:=
Y z
]isa
x y ,Y∀ z
-clause, then
∀yD
is a
x y z
-clause.
A
Q
Q
Explicitely, a formula
is a
-goal iff all its free variables are in
,andfor
y r
A
y
A
y r
every subterm
of
with
either existentially bound in
(with
in the
scope) or else free in
A
and flexible in
Q
,the
r
are distinct variables either
λ
-
or universally bound in
A
(such that
y r
is in the scope) or else free in
A
and
forbidden in
Q
.
A
Q
-substitution is a substitution of
Q
-terms.
A unification problem
U
consists of a
∀∃∀
-prefix
Q
and a conjunction
C
of
-terms of the same type, i.e., i =1 r i =
equations between
Q
s i . We may assume
that each such equation is of the form
λ x r
=
λ x s
with the same
x
(which may
be empty) and
of ground type.
A solution to such a unification problem
r, s
U
is a
Q
-substitution
ϕ
such that
for every
i
,
r i ϕ
=
s i ϕ
holds (i.e.,
r i ϕ
and
s i ϕ
have the same normal form). We
Search WWH ::

Custom Search