- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

Date: Wed, 25 Apr 2007 08:36:36 +0200

* Am 24.04.07 schrieb Claus Reinke:

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).

Doesn't a notion of nested computations make one strive for monadic

encapsulation which always allows to collapse layers with a join

operation?

[...]

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.

[...]

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.

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

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

*
This archive was generated by hypermail 2.3.0
: So Sep 20 2020 - 07:15:03 CEST
*