encapsulated search (Re: New PAKCS release (Version 1.8.0))

From: Claus Reinke <claus.reinke_at_talk21.com>
Date: Fri, 27 Apr 2007 01:49:20 +0100

Dear Curry fans,

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

i thought this last statement reflected a rather strange point of view (strange
to me, i mean;-), so i tried to find out more. from a search of the mailing list
archive, i was led to this paper as the likely origin:

    http://www.informatik.uni-kiel.de/~mh/publications/papers/JFLP04_findall.html
    Encapsulating Non-Determinism in Functional Logic Computations [1]
    Bernd Braßel, Michael Hanus, Frank Huch
    Journal of Functional and Logic Programming, No. 6, 2004

which i found rather exciting. first, the tree representation of search
spaces, followed by suitable traversals, as suggested in [1], is very close to
one of the main suggestions in my 1991 MSc thesis, which i abstracted here
in the earlier thread, and even if the authors weren't aware of my suggestions,
it is nice to see them validated after so long (i must be getting old;-). second,
in focussing on the interactions of encapsulation and sharing, and in giving an
operational semantics, the paper clearly went beyond my own work, and
identified some serious and unexpected issues afflicting the call-by-need
variation of these ideas, so this seemed like the ideal opportunity to link
myself back in to the current FLP research stream.

[about myself: i have focussed on functional programming in Haskell in
 recent years, but have this year restarted my language design experiments
 at the level of core calculi, and to get a basis for executable specifications
 of such calculi, i am also developing an embedding of small-step,
 language-level operational semantics in Haskell; given my background,
 it is not surprising that the first things i added after the basic call-by-need
 calculus were non-determinism and logic variables. there are several
 avenues i want to explore from here, encapsulated search based on a
 tree representation of the search spaces being one of the aspects i had
 considered solved, before seing the sharing issues raised in [1] ]

unfortunately, my enthusiasm did not last long, as the compelling analysis
of the issues was followed by design decisions that i find hard to agree
with (limitation of encapsulated search to IO), and the operational
semantics was given at the level of an abstract machine instead of the
level of the language itself. i will try to express my concerns here, in the
hope of restarting the interesting discussions that followed the paper back
in 2004. ideally, this might lead to a redesign of Curry's encapsulated
search, but if you could convince me that this ideal is not practical, that
too would be a useful outcome, for my own experiments.

since the analysis in [1] is so compelling, it would be hard to challenge,
so if i am unhappy with the conclusions, and if the analysis seems to lead
more or less directly to these conclusions, i must try to shake the
assumptions on which the analysis of the issues is based. if i can suggest
a suitably different perspective on the symptoms, then a different analysis
might lead to different conclusions, without invalidating the chain of logic
presented in that paper.

let me start with the statements i can agree with:

- in an FLPL combining sharing with non-determinism, sharing
    becomes observable

- if we want to provide encapsulated search within a pure FPL, it
    is desirable to contain all non-functional effects to the capsules

- it is possible to extend an FLP with observable sharing

    http://citeseer.ist.psu.edu/claessen99observable.html
    Observable Sharing for Functional Circuit Description [2]
    Claessen and Sands, 1999

    nevertheless, we do not want such an extension to happen
    accidentally, in the form indicated in the problematic examples
    provided in [1]

- it is possible to "contain" non-determism in the IO monad

    http://research.microsoft.com/~simonpj/Papers/imprecise-exn.htm
    A semantics for imprecise exceptions [3]
    Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow,
    Fergus Henderson. PLDI'99, Atlanta.

    as i mentioned before, exceptions can be seen as parameterised
    failure, and imprecise exceptions add non-determistic generation
    of such exceptions. the solution proposed in [3] is to contain the
    _observation_ of such non-determism to the IO monad, very much
    like the encapsulation of search in [1], which adds logic variables.

    nevertheless, we would prefer the encapsulation of search to be
    pure, not IO-bound, if at all possible.

- even if we just want to provide encapsulated search within an FLPL,
    violations of referential transparency, as demonstrated in [1], are
    highly undesirable

so far, so good, i hope? now for my first objections:

- the examples in [1] assume extensions of an FLPL, not an FPL.
    in particular, the main issue does not seem to be the interaction
    of sharing and encapsulation, but the interaction of non-local and
    local (encapsulated) non-determinism, mediated via sharing.

    the early examples assume a "function" coin, which is not a function
    at all - it is a non-deterministic expression bound to an identifier, and
    the non-determinism is not encapsulated. thus, these examples do not
    apply to an FPL with encapsulated search, and in an FLPL, the
    effects observed are due to the non-encapsulated non-determinism
    in coin.

    these distinctions might be hard to observe in Curry, where
    deterministic evaluation and generation of non-determistic alternatives
    are just two views of the same function definition. it would be helpful
    to make potential sources of non-determinism more explicit, and to
    distinguish them from deterministic code.

- strong encapsulation proposes to "cut" any sharing that might affect
    the results of encapsulated search, but [1] immediately provides
    examples that show how the sharing in effect when an encapsulated
    search is evaluated can depend on the order of evaluation outside.

    if there was no non-determinism outside the capsule, sharing would
    not seem to have any effects other than the known observability of
    sharing _of non-determinism_ _inside_ the capsule. to observe
    sharing _outside_ the capsule, we would have to probe it with
    non-determinism, which we can only obtain _inside_ the capsule,
    and can only pass to expressions from outside the capsule as
    parameters, which are _always shared_.

    what would happen if, instead of closing out sharing, we were to
    close out sources of non-determinism not originating within the
    same capsule? as a first approximation, we might chose to embed
    non-nested encapsulated search within a deterministic FPL, as a
    refinement, we might try to use different sets of operators for
    non-local and local non-determinism, and to tag non-determinism
    arising within different capsules (similar to the tagging of state
    references in local state transformer monads in Haskell).

    it seems that we could then choose whether (a) to import an
    external source of non-determinism into a capsule, or (b) to
    prevent such import, forcing propagation of such external
    non-determinism outside the capsule (depicted here as <..>):

        let x = 0 ? 1 in <.. x ..> --a--> <.. (0?1) ..>

        let x = 0 ? 1 in <.. x ..> --b--> <.. 0 ..> ? <.. 1 ..>

    variation (a) seems to suffer from evaluation order dependency,
    and is, in effect, the starting point of the discussion in [1], but
    variation (b), not mentioned in [1], does seem to be free of such
    issues. it does not matter whether or not the external non-determinism
    is propagated before the capsule is evaluated or not, because it will
    definitely be propagated outwards before any of its branches can
    enter the capsule. note the difference in approach, compared to
    strong encapsulation, eg in example 1.3 in [1]. also note that, if
    variation (b) is indeed order-independent, the main reasons for
    which [1] suggests to impose sequencing of encapsulated search
    are no longer present.

- i find it intriguing that, while [1] argues for strong and against weak
    encapsulation, it seems to provide only a single example against
    the latter (compared to several against the former). following
    variation (b) above, both expressions in that example (1.4) would
    be equivalent. to obtain a non-singleton encapsulated result, one
    would have to associate the non-determinism in coin with that of
    the capsule.

as this discussion starter has already grown rather long, i'll leave it
here, for now, to see whether it rings any bells among the list members.

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

actually, the web-interface (nice, but for somewhat terse error messages)
has to rule out IO, and thus encapsulated search in the IO-based form, right?


_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fri Apr 27 2007 - 08:25:36 CEST

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