Hi Bernd!
> This is a really good point. Thus convinced, I would like to add some
> definitions to the proposal, as this is how we handle non-determinism
> in
> the prelude of the new Curry implementation, following the proposal of
> the mentioned paper:
> [...]
> data SearchTree a
> = Fail
> | Value a
> | Or [SearchTree a]
> | Suspend
IIUC, the main difference between the paper and your proposal is the
introduction of the Suspend constructor in SearchTree. Looking at the
definitions of allValuesD and allValuesB, Suspend is always handled like
a failure. Furthermore, PAKCS' implementation of getSearchTree cannot
return Suspend at all. On the other hand, MCC could return Suspend when
an encapsulated search suspends, but the underlying implementation can
do
better: It resumes a suspended search once the uninstantiated non-local
variable, which was causing the suspension, is bound.
Here is a little contrived example that demonstrates why a simple
Suspend
constructor is not general enough (at least for MCC's implementation of
encapsulated search).
> import AllSolutions
>
> data Nat = Z | S Nat
>
> le Z _ = success
> le (S m) (S n) = le m n
>
> notAbove n | m `le` n = m where m free
>
> main =
> do
> t <- getSearchTree (notAbove lim)
> let solns = allValuesD t
> doSolve (x =:= head solns)
> print x
> doSolve (y =:= head (tail solns) & lim =:= S (S Z))
> print y
> where x, y, lim free
This will print the two lines
Z
S Z
However, this wouldn't work if getSearchTree returned Suspend when an
encapsulated search suspends (unless of course the compiler is smart
enough to figure out that is should perform the unification lim =:=
S (S Z) *before* computing the second solution).
Regards
Wolfgang
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Okt 14 2005 - 12:23:00 CEST