> With possibly non-terminating computations this is not only an issue of
> datastructure traversal. You must also prepare for the case of one of
> your computations failing to return a constructor rooted expression due
> to looping.
> Non-determinism is set to deal with finite, hence observable failure.
>
> fail `amb` x = x
> x `amb` fail = x
>
> But to have choice expressing real alternatives one would also like it
> to cope with unobservable failure.
>
> bot `amb` x = x
> x `amb` bot = x
[any amb actually conforming to the first two equations would already have
to cope with unobservable failure, wouldn't it? that is Berry's parallel-or]
if we reify amb and fail as constructors, we have an object-language
representation of the global search tree (if we also interpret logic variable
binding as (multi-)set quantification, and amb/fail as (multi-)set union/empty
representations, we get a representation of local search trees). but as you
point out, we do not yet have an object-language representation of the
computation of that search tree.
at the meta-language level, we can group computations into several
classes: (1) terminate successfully with a deterministic value, amb, or fail,
(2) terminate unsuccessfully with an exception, (3) fail to terminate. in a
language with fail, exceptions are just parameterised failures, so we only
need to concern ourselves with (1) and (3).
in (1), we either have a representation of success, or of failure, so no
problem wrt interpreting amb/fail, whereas in (3), we have a representation
of a computation on the way to (1) (assuming a language-level operational
semantics, that is simply a partially evaluated program, not yet in the
intended normal form).
by simply looking at the representation, we can see whether or not a
program has been reduced to a value, but, in general, we cannot decide
whether an intermediate program will end up in (1) or in (3). so we have
to distribute our computational resources evenly over all intermediate
programs (all branches in the amb/fail-search tree).
at the meta-level, that is fairly straightforward, and amounts to a
breadth-first expansion of the search tree. but if we want to reify this
at the object-language level, we have a small problem: we can expand
the search-tree in breadth-first manner, and we can "see" the evaluation
status of branches at the meta-level, but how do we reify this observation
at the object-level?
we do not want our equational theory to collapse into the identity, so
our object-level programs should not be able to distinguish program
representations at different stages of evaluation (1+1+1==1+2==3).
but we do want our object-level programs to be able to extract early
solutions from a partially expanded search tree.
if we accept committed choice evaluation of non-deterministic semantics,
we could leave it to the meta-level to commit to the earliest available
branches in the search tree (by time, or by number of reductions). if we
insist on no-choice evaluation (full representation of solution multisets),
we could still leave it to the meta-level to expand search trees in breadth-
first manner, but we wouldn't be able to observe the results in the order
they become available at the object-language level (at the meta-level, it
would be apparent that (bot `amb` x) has at least as much information
as x, but most implementations these days do not let us see intermediate
programs in non-terminating reduction sequences..).
i hope these non-deterministic ramblings of mine have not been completely
off-topic. it is just that this discussion reminded me of things that were
going through my mind in the context of my ancient MSc work (1991, in
pre-Curry Kiel;-).
claus
ps. once one makes non-determinism explicit, one also has nested
non-determinism. in non-local search, local non-determinism simply
propagates to the top, so it isn't locally observable, but with local
(encapsulated) search, non-determinism becomes locally observable.
which raises the issue of distinguishing determinism types a from
non-determinism types ND a from nested non-determinism types
ND (ND a). in particular, one might want to distinguish between
(bottom :: ND a) and (bottom :: a) (if a is deterministic), so that
(bottom :: a `amb` y) could, in principle, reduce to (bottom :: a)
(avoiding fail, but not non-termination). whether or not that is
desirable/practical is another question, though.
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Apr 20 2007 - 18:07:12 CEST