Information Technology Reference
In-Depth Information
sometimes write
C
as
r
=
s
, and (for obvious reasons) call it a list of unification
pairs.
We now define the unification algorithm. It takes a unification problem
U
=
U
=
QC
and returns a substitution
ρ
and another patter unification problem
Q
C
.Notethat
Q
-substitution, but
ρ
will be neither a
Q
-substitution nor a
will have the property that
-
ρ
only, and its value terms have no free
occurrences of forbidden variables from
is defined on flexible variables of
Q
Q
,
Q
-goal, and
-
if
G
is a
Q
-goal, then
Gρ
is a
ϕ
is an
U
-solution, then (
ρ ◦ ϕ
)
-
whenever
Q
∃
is an
U
-solution.
To define the unification algorithm, we distinguish cases according to the form
of the unification problem, and either give the transition done by the algorithm,
or else state that it fails.
Case
identity, i.e.,
Q.r
=
r ∧ C
.Then
Q.r
r ∧ C
⇒
ε
QC.
=
=
Case
ξ
, i.e.,
Q.λ
x
r
=
λ
x
s∧C
. We may assume here that the bound variables
x
are the same on both sides.
Q.λ
x
r
=
λ
x
s ∧ C
=
⇒
ε
Q∀
x
.r
=
s ∧ C.
Q.f
r
f
s
∧ C
Case
rigid-rigid, i.e.,
=
.
Q.f
r
=
f
s
∧ C
=
⇒
ε
Q.
r
=
s
∧ C.
Case
flex-flex with equal heads, i.e.,
Q.u
y
=
u
z
∧ C
.
⇒
ρ
Q
.Cρ
Q.u
y
=
u
z
∧ C
=
λ
y
.u
w
Q
is
∃u
,and
with
ρ
=[
u
:=
],
Q
with
∃u
replaced by
w
an enumeration
λ
y
.u
w
λ
z
.u
w
of
{ y
i
| y
i
=
).
Case
flex-flex with different heads, i.e.,
z
i
}
(note
=
Q.u
y
=
v
z
∧ C
.
⇒
ρ
Q
Cρ,
Q.u
y
=
v
z
∧ C
=
Q
are defined as follows. Let
where
ρ
and
w
be an enumeration of the variables
y
z
ρ
u, v
λ
y
.u
w
,λ
z
.u
w
Q
is
Q
∃u, ∃v
both in
and in
.Then
=[
:=
], and
with
∃u
inserted.
Case
flex-rigid, i.e.,
removed and
Q.u
y
=
t ∧ C
with
t
rigid, i.e., not of the form
v
z
with
flexible
.
Subcase
occurrence check:
v
t
contains (a critical subterm with head)
u
. Fail.
Subcase
pruning:
t
contains a subterm
v
w
1
z
w
2
with
∃v
in
Q
,and
z
free in
t
but not in
y
.
⇒
ρ
Q
.u
y
Q.u
y
=
t ∧ C
=
=
tρ ∧ Cρ
λ
w
1
,z,
w
2
.v
w
1
w
2
],
Q
is
∃v
.
where
ρ
=[
v
:=
Q
with
∃v
replaced by
Search WWH ::
Custom Search