>> 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]
actually, only the second set bears resemblance to parallel-or, with no
sequential evaluation order being sufficient to avoid non-termination. for the
first set of equations, either left-right or right-left evaluation should do. taking
left-right evaluation of (a `amb` b), if a evaluates to fail, amb can return b, if
a doesn't evaluate to fail, the first equation isn't relevant; if a evaluates to
something different from fail, amb can return a, if a's evaluation doesn't
terminate, a `amb` fail is not observably different from a, so the second
equation is still fullfilled. sorry about the misinterpretation.
> 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.
and this would be a lot clearer if there were three constructors, with
an explicit type coercion from deterministic to non-deterministic values
rather than an implicit coercion. since amb/fail combines composition
of alternatives with non-deterministic selection from them, it will always
represent non-local choice, so let me use a different set of constructors
for local search-trees and nested non-determinism:
mzero :: ND a
mplus :: ND a -> ND a -> ND a
return :: a -> ND a
(think of sets being represented by empty, union, and singleton; but
by not flattening the structure into a set, we keep a tree representation
of the search space that may be searched in different orders)
(return e) deterministically returns e, without making any assertions
about e itself being deterministic, mzero is a local fail, mplus is a local
version of the collection aspect of amb, without the selection aspect
(note the different types).
now we can distinguish bottom non-determinism from deterministically
returned bottom:
bottom :: ND ()
<= -- less defined than
(return (bottom :: ())) :: ND ()
<= -- less defined than
(return ()) :: ND ()
and nesting would be straightforward, too, at the inconvenience of
having those explicit return wrappers:
return (return 1 `mplus` return 2 `mplus` mzero) :: ND (ND Integer)
constructing local search spaces this way seems unproblematic, the
question is what happens when we try to observe results. lets use a
fold for that:
foldND :: (b -> b -> b) -> (a -> b) -> b -> ND a -> b
now, there are operations we can fold over a local search tree without
letting the local non-determinism escape, such as
idND = foldND mplus return mzero
mapND f = foldND mplus (return . f) mzero
filterND p = foldND mplus (\x->if p x then return x else mzero) mzero
existsND p = foldND (||) p False
functions like existsND are particularly interesting for the current discussion,
as a naive implementation would result in depth-first search; but a more
clever (and more expensive) implementation based on bottom-avoiding
(parallel) breadth-first search would be possible while keeping the
non-determinism localised.
alternatively, if filterND can be used to reduce a search-space to a singleton,
we should be able to extract the single solution:
theND = case foldND (++) (\it->[it]) [] of
{ [it] -> it;
_ -> error "no unique solution" }
the usual static type system is insufficient to guarantee safe encapsulation of
non-determinism, but if that was a goal, one might want to define a collection
of safe functions based on foldND, without exporting foldND itself. otherwise,
one could do things like this
localToGlobalND = foldND amb id fail
i hope this is less confusing than my previous attempt?-)
claus
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Di Apr 24 2007 - 14:16:49 CEST