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

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

Date: Fri, 28 Aug 2009 23:35:53 +0200

On Aug 28, 2009, at 5:31 PM, Bernd Brassel wrote:

*> Okay, then how about the following example: for the declarations
*

*>
*

*> data C a = C ?a
*

*> plus (C x) (C y) = x+y
*

*>
*

*> do the following expressions all have the same semantics?
*

*>
*

*> e1 = let x=C (0?1) in plus x x
*

*> e2 = let y=0?1 in let x=C y in plus x x
*

*> e3 = let y=0?1 in let x=C y in const (plus x x) y
*

Instead of trying the implementation again, I express these examples

monadically and use the equational laws from [1] to reason about their

meaning. The extension to the laws that implements annotated arguments

is in the (HNF) rule. Specialised to the data type above, the (HNF)

rule is:

share (return (C a)) = return (return (C a))

instead of the original deeply sharing version:

share (return (C a)) = share a >>= \a' -> return (return (C a'))

Your datatype and functions are translated as follows:

data C m a = C (m a)

plus a b = a >>= \ (C c) ->

b >>= \ (C d) ->

c >>= \ x ->

d >>= \ y ->

return (x+y)

const x _ = x

e1 = share (return (C (return 0 `mplus` return 1))) >>= \x ->

plus x x

-- y is not shared (does not occur more than once)

e2 = let y = return 0 `mplus` return 1

in share (return (C y)) >>= \x -> plus x x

-- now, y is shared

e3 = share (return 0 `mplus` return 1) >>= \y ->

share (return (C y)) >>= \x -> const (plus x x) y

We can see that e1 = e2 by substituting the let bound variable y and

evaluating the const call. However, for e3 we must apply the (Choice)

rule on the first occurrence of share which yields:

share (return 0) >>= \y -> share (return (C y)) >>= \x -> plus x x

`mplus`

share (return 1) >>= \y -> share (return (C y)) >>= \x -> plus x x

This reduces (in several steps) to:

plus (return (C (return 0))) (return (C (return 0)))

`mplus`

plus (return (C (return 1))) (return (C (return 1)))

and finally to: return 0 `mplus` return 2

On the other hand, e1---using the adjusted (HNF) rule---reduces to:

return (return (C (return 0 `mplus` return 1))) >>= \x -> plus x x

= plus (return (C (return 0 `mplus` return 1)))

(return (C (return 0 `mplus` return 1)))

= ...

= return 0 `mplus` return 1 `mplus` return 1 `mplus` return 2

So, e1 and e2 have the same semantics but e3 has a different semantics

when using the changed (HNF) rule (with the original (HNF) rule (that

is, without annotations) e3 has the same semantics as e1 and e2). I

have added your examples to [2].

They show that my interpretation of Wolfgangs proposal in the explicit

sharing framework is probably inaccurate (I think, also with

annotations, e1, e2, and e3 should have the same semantics.)

The question is then: what is the intended meaning of Wolfgangs

proposal and how can we formalise it?

If the translation scheme to monadic code would introduce 'share' for

let-bound variables regardless of whether they are shared then e2

would have the same meaning as e3 under the new (HNF) rule. But the

semantics of e1 would still be different -- as intended by the

annotation. In fact, I suspect that Wolfgang's intuition behind his

proposal is that all expressions e1, e2, and e3 can yield the result

1, so this change in the translation scheme would go into the wrong

direction.

Cheers,

Sebastian

[1]: http://www.cs.rutgers.edu/~ccshan/rational/lazy-nondet.pdf

[2]: http://gist.github.com/176983

Date: Fri, 28 Aug 2009 23:35:53 +0200

On Aug 28, 2009, at 5:31 PM, Bernd Brassel wrote:

Instead of trying the implementation again, I express these examples

monadically and use the equational laws from [1] to reason about their

meaning. The extension to the laws that implements annotated arguments

is in the (HNF) rule. Specialised to the data type above, the (HNF)

rule is:

share (return (C a)) = return (return (C a))

instead of the original deeply sharing version:

share (return (C a)) = share a >>= \a' -> return (return (C a'))

Your datatype and functions are translated as follows:

data C m a = C (m a)

plus a b = a >>= \ (C c) ->

b >>= \ (C d) ->

c >>= \ x ->

d >>= \ y ->

return (x+y)

const x _ = x

e1 = share (return (C (return 0 `mplus` return 1))) >>= \x ->

plus x x

-- y is not shared (does not occur more than once)

e2 = let y = return 0 `mplus` return 1

in share (return (C y)) >>= \x -> plus x x

-- now, y is shared

e3 = share (return 0 `mplus` return 1) >>= \y ->

share (return (C y)) >>= \x -> const (plus x x) y

We can see that e1 = e2 by substituting the let bound variable y and

evaluating the const call. However, for e3 we must apply the (Choice)

rule on the first occurrence of share which yields:

share (return 0) >>= \y -> share (return (C y)) >>= \x -> plus x x

`mplus`

share (return 1) >>= \y -> share (return (C y)) >>= \x -> plus x x

This reduces (in several steps) to:

plus (return (C (return 0))) (return (C (return 0)))

`mplus`

plus (return (C (return 1))) (return (C (return 1)))

and finally to: return 0 `mplus` return 2

On the other hand, e1---using the adjusted (HNF) rule---reduces to:

return (return (C (return 0 `mplus` return 1))) >>= \x -> plus x x

= plus (return (C (return 0 `mplus` return 1)))

(return (C (return 0 `mplus` return 1)))

= ...

= return 0 `mplus` return 1 `mplus` return 1 `mplus` return 2

So, e1 and e2 have the same semantics but e3 has a different semantics

when using the changed (HNF) rule (with the original (HNF) rule (that

is, without annotations) e3 has the same semantics as e1 and e2). I

have added your examples to [2].

They show that my interpretation of Wolfgangs proposal in the explicit

sharing framework is probably inaccurate (I think, also with

annotations, e1, e2, and e3 should have the same semantics.)

The question is then: what is the intended meaning of Wolfgangs

proposal and how can we formalise it?

If the translation scheme to monadic code would introduce 'share' for

let-bound variables regardless of whether they are shared then e2

would have the same meaning as e3 under the new (HNF) rule. But the

semantics of e1 would still be different -- as intended by the

annotation. In fact, I suspect that Wolfgang's intuition behind his

proposal is that all expressions e1, e2, and e3 can yield the result

1, so this change in the translation scheme would go into the wrong

direction.

Cheers,

Sebastian

[1]: http://www.cs.rutgers.edu/~ccshan/rational/lazy-nondet.pdf

[2]: http://gist.github.com/176983

-- Underestimating the novelty of the future is a time-honored tradition. (D.G.) _______________________________________________ curry mailing list curry_at_lists.RWTH-Aachen.DE http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curryReceived on Mo Aug 31 2009 - 09:29:57 CEST

*
This archive was generated by hypermail 2.3.0
: Mo Okt 26 2020 - 07:15:04 CET
*