- 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, 17 Dec 2010 00:13:14 +0900

On Thu, 2010-12-16 at 15:42 +0100, Julio Mariņo wrote:

*> negation would subtract a given amount of copies of
*

*> positive results...
*

Yes, this happens if (?) is not idempotent and I agree that this is more

interesting.

On Thu, 2010-12-16 at 15:47 +0100, Jan Christiansen wrote:

*> > 1. In a lazy language with call-time choice, choice is idempotent.
*

*>
*

*> This is only the case if you consider sets but in fact all
*

*> implementations use "multisets".
*

I concluded this independently from an implementation using the law

f (a ? b) = f a ? f b

and laziness.

Current Curry implementations neither adhere to this law nor to

idempotence because they will typically yield two results for (0?0) but

only one for (const 0 (1?1)). I used this equation as characterization

of call-time choice because it is hard to characterize the behaviour of

Curry systems equationally, that is, without fixing an evaluation order.

CRWL comes close, but it uses a set model and implies idempotence. I

used CRWL to derive the above equation from the more general CRWL

theorem:

|[ C[e] ]| = U { |[ C[t] ]| | t <- |[e]| }

The laws of the Sharing monad for lazy nondeterministic programming in

Haskell (ICFP'09) also hold only modulo idempotence of mplus.

*> Furthermore if you want to assign a
*

*> denotational semantics to encapsulation you probably need a multiset
*

*> model anyway.
*

Why? My impression is that an evaluation-order independent formalism for

laziness with call-time choice that does not imply idempotence is not

easy to define. A denotational semantics should probably be evaluation

order independent and model laziness so I think it is more difficult to

use multisets there than it is to use sets.

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Do Dez 16 2010 - 16:50:47 CET

Date: Fri, 17 Dec 2010 00:13:14 +0900

On Thu, 2010-12-16 at 15:42 +0100, Julio Mariņo wrote:

Yes, this happens if (?) is not idempotent and I agree that this is more

interesting.

On Thu, 2010-12-16 at 15:47 +0100, Jan Christiansen wrote:

I concluded this independently from an implementation using the law

f (a ? b) = f a ? f b

and laziness.

Current Curry implementations neither adhere to this law nor to

idempotence because they will typically yield two results for (0?0) but

only one for (const 0 (1?1)). I used this equation as characterization

of call-time choice because it is hard to characterize the behaviour of

Curry systems equationally, that is, without fixing an evaluation order.

CRWL comes close, but it uses a set model and implies idempotence. I

used CRWL to derive the above equation from the more general CRWL

theorem:

|[ C[e] ]| = U { |[ C[t] ]| | t <- |[e]| }

The laws of the Sharing monad for lazy nondeterministic programming in

Haskell (ICFP'09) also hold only modulo idempotence of mplus.

Why? My impression is that an evaluation-order independent formalism for

laziness with call-time choice that does not imply idempotence is not

easy to define. A denotational semantics should probably be evaluation

order independent and model laziness so I think it is more difficult to

use multisets there than it is to use sets.

Sebastian

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Do Dez 16 2010 - 16:50:47 CET

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