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