it seems that there are a few loose ends in my discussion starter, which i
should tie up before the discussion gets under way:
> let x = 0 ? 1 in <.. x ..> --a--> <.. (0?1) ..>
>
> let x = 0 ? 1 in <.. x ..> --b--> <.. 0 ..> ? <.. 1 ..>
as depicted here, alternative (a) corresponds to strong, and alternative (b)
to weak encapsulation. by this naming, the authors of [1] imply that (b)
does not completely encapsulate non-determinism, and that (a) is their
preferred option. i disagree with the implication, and with the preference.
the non-determinism in x does not escape the capsule, it is already
outside the capsule. so what strong encapsulation attempts to achieve
is to force non-determinism from outside the capsule into the capsule.
the main motivation seems to be that strong encapsulation generates
less restricted search spaces than weak encapsulation. however, the
fact that strong encapsulation needs to break a core feature of the
language (sharing of bindings), and runs into serious trouble doing so
(evaluation order and context dependency), is the main reason for
the suggested explicit ordering of search primitives, and should be
a strong indicator that there is something wrong with this approach.
there is, however, the issue that attempting to use definitions from
outside a capsule inside the capsule will strip them of their non-
determinism, so it seems as if weak encapsulation could never
generate the full search spaces.
let us step back for a moment, and survey our starting points:
call-by-need (cbn) lambda calculus (lc) improves on both normal-order
(no) and applicative-order (ao) lambda calculus, as follows: no-lc delays
evaluation of expressions until needed, avoiding needless evaluation, but
copies parameters, and might thus duplicate work; ao-lc shares evaluation
of parameters, avoiding duplication of work, but evaluates early, and thus
possibly needlessly; cbn-lc delays both evaluation and substitution, so
that it avoids both duplication of work (evaluation precedes substitution)
and needless work (evaluation is demand-driven). the key to avoiding
duplication of work (modulo optimal reduction, which i'll ignore here)
is to substitute only values.
since non-deterministic expressions are not values, cbn cannot substitute
them, so non-determinism is propagated outwards prior to substitution.
instead of bypassing this fundamental restriction, we should think about
turning non-deterministic expressions into values. but that is exactly what
we are doing when introducing encapsulated search! we turn an implicit
search space into an explicitly represented search tree.
if we were to represent the implicit non-determinism in types, we might
consider any type 'a' as implicitly annotated: '{ND} a', any function of
type 'a -> b' as implicitly annotated: 'a -> {ND} b', and function
application as including implicit lifting, propagating implicit non-determinism
outwards in order to get at the values to pass as function arguments:
($) :: ( a -> {ND}b ) -> {ND}a -> {ND} b
f $ (a1?a2) = (f $ a1) ? (f $ a2) -- pseudo- notation, non-det case
f $ (det a) = f a -- pseudo-notation, deterministic case
we can then consider explicitly represented search trees as an explicit
type constructor, and encapsulation as a type coercion:
encap :: {ND}a -> ND a -- encapsulate an implicit search
it will be useful to consider the reverse coercion as well:
uncap :: ND a -> {ND} a -- non-deterministically extract results
as near as possible, both 'encap . uncap' and 'uncap . encap' ought to
be identities.
now, we should have all the components for making encapsulated
search work with so-called weak encapsulation, by a two-step process:
- implicit search spaces can be turned into values, which can be
passed as parameters, so we can pass non-determinism into a
capsule, without having the non-determinism propagated away.
- explicit search spaces can be turned back into implicit search
spaces, so we can allow results from explicit search trees to
propagate implicitly inside a capsule.
in terms of the example:
let coin = 0 ? 1 in encap coin
--> {propagate implicit non-det}
let coin = 0 in encap coin ? let coin = 1 in encap coin
--> {substitute}
encap 0 ? encap 1
but
let coin = encap (0 ? 1) in encap (uncap coin)
--> {substitute}
encap (uncap (encap (0 ? 1)))
--> {uncap . encap = id; propagate explicit to implicit non-det}
encap (0 ? 1)
so we have full control over whether to keep non-determinism implicit
or explicit, and unlike the 'clone' primitive discussed here back in June
2004, we avoid order-dependency.
this may all have to be extended to take logic variables into account, but
does this first part make sense to you?-)
claus
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Apr 27 2007 - 15:16:49 CEST