Re: New PAKCS release (Version 1.8.0)

From: Sebastian Hanowski <>
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

> (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:

Good luck,



Simply typed functional programming seems to be very happy with
non-terminating computations. And so can functional-logic programming be
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

curry mailing list
Received on Mi Apr 25 2007 - 09:01:33 CEST

This archive was generated by hypermail 2.3.0 : So Jan 26 2020 - 07:15:09 CET