Re: Invertible nondeterminism?

From: Jan Christiansen <>
Date: Thu, 16 Dec 2010 23:08:17 +0100

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

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
Received on Fr Dez 17 2010 - 11:10:17 CET

This archive was generated by hypermail 2.3.0 : Do Aug 06 2020 - 07:15:05 CEST