Information Technology Reference
In-Depth Information
→U
-solutions. For a
2. Definition of
Φ
:
U
-solutions
U
-solution
ϕ
define
v
(
Φϕ
):=
λ
w
1
,
w
2
.
(
vϕ
)
w
1
0
w
2
v
,v
w
(
Φϕ
):=
wϕ
otherwise, i.e.,
w
=
flexible.
Since by assumption (
uϕ
)
y
=
tϕ
, the normal form of
tϕ
cannot contain
z
free.
ϕ
:=
Therefore, for
Φϕ
,
vρϕ
=(
λ
w
1
,z,
w
2
.v
w
1
w
2
)
ϕ
λ
w
1
,z,
w
2
.
λ
w
1
,
w
2
.
vϕ
w
1
0
w
2
)
w
1
w
2
=
(
(
)
=
λ
w
1
,z,
w
2
.
(
vϕ
)
w
1
0
w
2
=
λ
w
1
,z,
w
2
.
(
vϕ
)
w
1
z
w
2
=
vϕ.
ϕ
uϕ
)
tρϕ
.For
Hence
=
Φϕ
satisfies (
y
=
r
=
s
this follows by the same
Φ
(
argument.
can again be proved as in the previous case.
Subcase
pruning impossible: Then
Φϕ
)=
ϕ
λ
y
t
has an occurrence of a universally
quantified (i.e., forbidden) variable
z
. Therefore clearly there is no
Q
-substitution
ϕ
such that (
.
Subcase
explicit definition. Then
uϕ
)
y
=
tϕ
Q
ρ
=[
u
:=
λ
y
t
],
is obtained from
Q
by
U
Q
Cρ
Q
-substitution, for we have
removing
∃u
,and
=
.Notethat
ρ
is a
performed the pruning steps.
1.
Φ
is well-defined: Let
ϕ
be a
U
-solution, i.e.,
rρϕ
=
sρϕ
for (
r
=
s
)
∈ C
.
ρ ◦ ϕ
)
We must show that
ϕ
:= (
Q
∃
is an
U
-solution.
uρϕ
)
tρϕ
.But
For
u
y
=
t
: We need to show (
y
=
uρϕ
)
ϕ
)
(
y
=((
λ
y
t
)
y
tϕ
=
tρϕ
=
since
u
does not appear in
t
.
For (
r
=
s
)
∈ C
: We need to show (
r
=
s
)
ϕ
. But this clearly follows from
ρϕ
.
2. Definition of
(
r
=
s
)
Φ
:
U
-solutions
→U
-solutions, and proof of
Φ
(
Φϕ
)=
ϕ
.For
a
U
-solution
ϕ
define
Φϕ
=
ϕ
Q
∃
.Then
uρϕ
=
λ
y
tϕ
=
λ
y
tϕ
=
uϕ,
vρϕ
=
and clearly
vϕ
for all other flexible
ϕ
.For(
r
=
s
)
∈ C
,from
rϕ
=
sϕ
we
rϕ
=
sϕ
.
easily obtain
It is not hard to see that the unification algorithm terminates, by defining a
measure that decreases with each transition.
Corollary 2.
Given a unification problem
U
=
QC
, the unification algorithm
Q
,ρ
either returns
#
f
,andthereisno
U
-solution, or else returns a pair
(
)
Q
(i.e., a unification problem
U
with a “transition” substitution
ρ
and a prefix
Search WWH ::
Custom Search