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