Re: New PAKCS release (Version 1.8.0)

From: Claus Reinke <claus.reinke_at_talk21.com>
Date: Tue, 24 Apr 2007 10:30:49 +0100

>> 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 Tue Apr 24 2007 - 14:16:49 CEST

This archive was generated by hypermail 2.3.0 : Thu Sep 19 2019 - 07:15:07 CEST