Information Technology Reference
In-Depth Information
→U -solutions. For a
2. Definition of
Φ
:
U
-solutions
U
-solution
ϕ
define
v (
Φϕ
):=
λ w 1 , w 2 .
(
)
w 1 0
w 2
v ,v
w
(
Φϕ
):=
otherwise, i.e.,
w
=
flexible.
Since by assumption (
)
y
=
, the normal form of
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 .
w 1 0
w 2 )
w 1 w 2
=
(
(
)
=
λ w 1 ,z, w 2 .
(
)
w 1 0
w 2
=
λ w 1 ,z, w 2 .
(
)
w 1 z w 2
=
vϕ.
ϕ
)
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
)
y
=
Q
ρ
=[
u
:=
λ y t
],
is obtained from
Q
by
U
Q
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ρϕ
=
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 =
λ y
=
uϕ,
vρϕ =
and clearly
for all other flexible
ϕ
.For(
r
=
s
)
∈ C
,from
=
we
=
.
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