Re: Suspending in or-nodes

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Fri, 6 Nov 1998 09:45:56 +0100

Sven Panne wrote:
> Perhaps someone on this list can enlighten me a little bit: It's not
> clear to me why an entire disjunction must suspend when one disjunct
> suspends.

The main problem is that it is not allowed to commit to the
non-suspending branch and ignore the suspended branch (as somebody
familiar with concurrent logic programming might think)
since then you would loose completeness (as you already pointed out).
Taking Sergio's remarks into account, a more appropriate example
is the following (using the new syntax):

f 0 x = success
f x 1 = success

g eval rigid
g 0 = 0

h eval flex
h 1 = 1

The goal to solve is: f (g x) (h x) & x=:=0

Now, if we ignore the suspending alternative caused by the evaluation
of (g x), we could bind x to 1 by evaluating (h x) and thus run
into a failure, so we loose the answer {x=0}.

Hence, your remark is right:
> Of course things get incomplete when you simply commit to the
> non-suspending disjunct and forget about the suspending one. Simply
> keep the latter one as it is, as flexible branches similarly keep
> suspending RHSs.

BTW, this is also done in our Java-based implementation where
or-branches are immediately executed by different threads.
The main problem w.r.t. the formal definition is a matter
of presentation. Since there is only a reduction function
on entire expressions (Eval[expr]) and not a representation
of suspended expressions with their definitional trees,
it is simpler to evaluate an or-node only if both
branches can be evaluated further. A formal description
of your proposal might require the explicit representation
of suspended expressions with definitional trees in the goals.
Any suggestions to improve it?

Another options is to describe your proposed extension informally
in the report.

Best regards,

Michael
Received on Fr Nov 06 1998 - 09:49:00 CET