Information Technology Reference
In-Depth Information
⇒
ρ
U
,and
-
the unification algorithm makes a transition
U
=
Φ
:
U
-solutions
→U
-solutions
ϕ
→
ρ ◦ ϕ
)
(
Q
∃
→U
-solutions such that
Φ
is
is well-defined and we have
Φ
:
U
-solutions
Φ
(
inverse to
Φ
, i.e.
Φϕ
)=
ϕ
,orelse
-
the unification algorithm fails, and there is no
U
-solution.
Q.r
r ∧ C
⇒
ε
QC
Φ
Proof. Case
identity, i.e.,
=
=
.Let
be the identity.
ξ
Q.λ
x
r
λ
x
s ∧ C
⇒
ε
Q∀
x
.r
s ∧ C
Φ
Case
, i.e.,
=
=
=
. Let again
be the
identity.
Case
rigid-rigid, i.e.,
Q.f
r
=
f
s
∧ C
=
⇒
ε
Q.
r
=
s
∧ C
. Let again
Φ
be the
identity.
Case
flex-flex with equal heads, i.e.,
⇒
ρ
Q
.Cρ
Q.u
y
=
u
z
∧ C
=
with
ρ
=
λ
y
.u
w
Q
is
∃u
,and
[
u
:=
],
Q
with
∃u
replaced by
w
an enumeration of those
y
i
which are identical to
z
i
(i.e., the variable at the same position in
z
). Notice
λ
y
.u
w
λ
z
.u
w
that
=
.
Φ
ϕ
U
-solution, i.e., assume that
Cρϕ
1.
is well-defined: Let
be a
holds.
ρ ◦ ϕ
)
We must show that
ϕ
:= (
Q
∃
is a
U
-solution.
uρϕ
=(
λ
y
.u
w
ϕ
.
For
u
y
=
u
z
: We must show (
uϕ
)
y
=(
uϕ
)
z
.But
uϕ
=
)
Hence (
uϕ
)
y
=(
uϕ
)
z
by the construction of
w
.
ρϕ
For (
r
=
s
)
∈ C
: We need to show (
r
=
s
)
ϕ
. But by assumption (
r
=
s
)
holds, and
r
=
s
has all its flexible variables from
Q
∃
.
→U
-solutions. Let a
2. Definition of
Φ
:
U
-solutions
Q
-substitution
ϕ
be
u
(
given such that (
u
y
=
u
z
)
ϕ
and
Cϕ
. Define
Φϕ
):=
λ
w
.
(
uϕ
)
w
0
(w.l.o.g),
and
v
(
Φϕ
):=
v
foreveryothervariable
v
in
Q
∃
.
ϕ
is a
U
-solution: Let (
Φϕ
=:
r
=
s
)
∈ C
.Then(
r
=
s
)
ϕ
by assumption,
for
ϕ
is a
Q
-substitution such that
Cϕ
holds. We must show
ρϕ
.
(
r
=
s
)
Notice that our assumption (
uϕ
)
y
=(
uϕ
)
z
implies that the normal form of both
sides can only contain the variables in
w
. Therefore
uρϕ
=(
λ
y
.u
w
ϕ
)
=
λ
y
.
(
λ
w
.
(
uϕ
)
w
0
)
w
=
λ
y
.
(
uϕ
)
w
0
=
λ
y
.
(
uϕ
)
y
=
uϕ
ρϕ
.
and hence (
r
=
s
)
Φ
(
ϕ
:=
3.
Φϕ
)=
ϕ
:Solet
ϕ
be an
U
-solution, and
Φϕ
.Then
u
Φ
ϕ
=
u
(
Q
∃
ρ ◦ ϕ
)
uρϕ
=
=
uϕ,
as proved in 2.
Search WWH ::
Custom Search