Re: Invertible nondeterminism?

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 Thu Dec 16 2010 - 16:50:47 CET

This archive was generated by hypermail 2.3.0 : Mon Nov 11 2019 - 07:15:08 CET