* Am 24.04.07 schrieb Claus Reinke:
> >> 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.
I only wanted to point out that due to non-determinism FLP must be very
sensitive to non-termination. Even more than FP. And of course the
second set of equations wasn't meant as a definition although one would
like these to hold definitionally (when x terminates).
> > 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.
Doesn't a notion of nested computations make one strive for monadic
encapsulation which always allows to collapse layers with a join
operation?
[...]
> (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)
There's interesting work by Antoy/Tolmach on using datastructures other
than lists. I think their trick is to use possibly infinitely branching
trees to collect output which allow to surpass an infinity of values in
a single step like a limit construction.
[...]
> 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
Your issues relate to the Curry topics of using trees to collect output
and to 'encapsulated search'. But I am the wrong person to say something
about this. Seems to have largely to do with concealing
non-determinism with IO.
> localToGlobalND = foldND amb id fail
Doesn't Sergio Antoy have posted an equivalent of this lately?
getAllValues x = findall (=:= x)
chooseValue (u:v) = u ? chooseValue v
Such that
localToGlobalND = chooseValue . getAllValues
> i hope this is less confusing than my previous attempt?-)
> claus
Sorry for having answered only very selectively. Claus, if you feel like
trying out your ideas in Curry, there's a quite usable web-interface:
http://www-ps.informatik.uni-kiel.de/~mh/pakcs/curryinput_c2p.cgi
Good luck,
Sebastian
PS
Simply typed functional programming seems to be very happy with
non-terminating computations. And so can functional-logic programming be
too.
But when it comes to non-determinism this is more crucial.
As it is too in dependently typed programming where typecheching relies
on computations.
Thus Altenkirch/Capretta/Uustalu have suggested to encapsulate programs
which can loop in a monad.
Looks like that would allow to make the behaviour of non-det choice in
presence of bottom more explicit.
But as of now I'm far from beeing able to say anything more concrete on
this.
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Apr 25 2007 - 09:01:33 CEST