On 16.12.2010, at 16:13, Sebastian Fischer wrote:
> 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.
So, would it be bad if you only have a weaker form of this law?
Something like
remove-dup (f a ? b) = remove-dup (f a ? f b)
> The laws of the Sharing monad for lazy nondeterministic programming in
> Haskell (ICFP'09) also hold only modulo idempotence of mplus.
I am not sure whether i am getting this correctly. That is, the mplus
operator of a sharing monad has to be idempotent? Even if f (a ? b) =
f a ? f b does not hold generally? This would contradict a statement I
have made below.
>> Furthermore if you want to assign a
>> denotational semantics to encapsulation you probably need a multiset
>> model anyway.
>
> Why?
I concluded this from the behaviour of the encapsulation in kics. But
maybe this behaviour does not show up for other approaches to
encapsulation.
test1 = (\[x] -> allValuesB (searchTree x)) [0?1]
test2 = (\[x] -> allValuesB (searchTree x)) ([0]?[1])
We get test1 = [0,1] and test2 = [0]?[1]. That is, although [0?1] and
[0]?[1] have the same set-valued semantics we can distinguish them
using encapsulation. Do others think that encapsulation should behave
differently in this example?
> 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.
I definitely second this. In fact, I think that a "denotational"
semantics with multisets would be quite similar to your Sharing monad
approach. While a set-valued semantics can employ the multialgebraic
model (that is, all non-determinism is flattened out) a multiset-
valued semantics has to employ the poweralgebraic model (that is, data
structures contain non-determinism). But while the multialgebraic
model models call-time choice you have to do extra work to get call-
time choice in the poweralgebraic model.
By the way right now I think that you also have to use multisets if
you want to assign a denotational semantics to recursive let
expressions like they are implemented by Kics and PAKCS.
Cheers, Jan
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Dez 17 2010 - 11:10:17 CET