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

From: Claus Reinke <claus.reinke_at_talk21.com>

Date: Fri, 27 Apr 2007 11:59:24 +0100

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

Date: Fri, 27 Apr 2007 11:59:24 +0100

it seems that there are a few loose ends in my discussion starter, which i

should tie up before the discussion gets under way:

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

*
This archive was generated by hypermail 2.3.0
: Sa Jul 24 2021 - 07:15:04 CEST
*