Re: New PAKCS release (Version 1.8.0)

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>
Date: Wed, 25 Apr 2007 08:36:36 +0200

* 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 Wed Apr 25 2007 - 09:01:33 CEST

This archive was generated by hypermail 2.3.0 : Mon Sep 16 2019 - 07:15:06 CEST