Next: Encoding of SLD-resolution
Up: Additive Interaction Nets as
Previous: Basic Concepts
Figure:
A visualization of Proposition 1
|
The next proposition guarantees results of reduction are independent of orders of reduction
in additive interaction nets without guarded unification variables.
Proposition 1
Let N be a net without guarded unification variables.
If reducible two agents a and
b are reduced
by a rewrite rule r1
(mgu q1)
and after the one-step reduction reducible immediately two agents
g and t
are reduced by a rewrite rule r2
(mgu q2) in a net N ,
there is a reduction in N such that
g and t
are reduced by r2
(mgu q'2 )
and after the one-step reduction immediately
a and
b are
reduced by r1 (mgu q'1 )
and
q2 q1 = q'1q'2 ,
where we assume that r1 and r2 do not have guarded unification variables.
(see Figure ![[*]](cross_ref_motif.gif)
).
Proof. have
q2q1g
=
q2g'
=
q2q1g' and
q2q1t
=
q2t'
=
q2q1t'.
So we can unify
g =. g' and
t =. t'.
Let q'2 be the mgu of the equation.
Then
xq'2
=
q2q1
for some substitution x.
Moreover we have
xa'
=
xq'2a'
=
q2 q1a'
=
q2 q1a
=
x
q'2
a
and
xb'
=
xq'2b'
=
q2 q1b'
=
q2 q1b
=
x
q'2
b.
So we can unify
a' =.
q'2
a
and
b' =.
q'2
b.
Let q'1 be the mgu of the equation.
So, we have
x'
q'1
=
x
for some substitution x' .
Then
x'
q'1
q'2 =
q2
q1.
Hence there is a reduction in the reverse order.
By the way, note that
q'1
q'2
a
=
q'1
q'2
a'
and
q'1
q'2
b
=
q'1
q'2
b'
and
q1
is the mgu of
a =. a' and
b =. b'.
Hence
z
q1
=
q'1
q'2
for some substitution z.
Furthermore,
we have
z
q1
g
=
q'1
q'2
g
=
q'1
q'2
g'
=
z
q1
g'
=
z
g'
and
z
q1
t
=
q'1
q'2
t
=
q'1
q'2
t'
=
z
q1
t'
=
z
t'
So we can unify
q1
g
=.
g'
and
q1
t
=.
t'.
Since q2 is the mgu of the equation,
z'
q2
= z for some substitution z'.
Since
z'
q'1
q'2
=
q2
q1
and
z'
q2
q1
=
q'1
q'2,
we have
q2
q1
=
q'1
q'2.
The above proposition does not guarantee the confluence of
two different reducible pairs of agents.
For example, there is a counterexample of the middle part of Figure under the
rewrite rules of Figure .
As in the right part of Figure by introducing a guarded unification variable
we can avoid such a nondeterminism (we can apply only r1 to the shown net).
Next: Encoding of SLD-resolution
Up: Additive Interaction Nets as
Previous: Basic Concepts
Satoshi Matsuoka
11/14/1999