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

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

Date: Tue, 24 Apr 2007 10:30:49 +0100

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.

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

*
This archive was generated by hypermail 2.3.0
: Mi Okt 21 2020 - 07:15:04 CEST
*