Hi Jan,
On Thu, 2010-12-16 at 23:08 +0100, Jan Christiansen wrote:
> 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)
Is remove-dup a language construct or only available in the semantics?
I'm not sure about the consequences of this law. It would be nice if it
allows to have laziness, call-time choice, and anti in a single
language. On the other hand, I'd like to use only language constructs in
equational laws..
I can rephrase my previous summary as follows, for the record. If we
have
f (a ? b) = f a ? f b
for all functions f but allow
f failure /= failure
for some functions f, like (const x), then (?) is idempotent. One way
out is to drop the first law (for example by using run/eval-time choice)
or to not allow the second inequalities (for example by using call-by
value). Another way out would be to find an alternative characterization
of call-time choice.
> > 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?
The laws imply that the sharing monad is idempotent if we include the
(Ignore) law:
a = share (mzero `mplus` mzero) >>= \_ -> a (Ignore)
= (share mzero >>= \_ -> a)
`mplus` (share mzero >>= \_ -> a) (Choice)
= (return mzero >>= \_ -> a)
`mplus` (return mzero >>= \_ -> a) (Fail)
= a `mplus` a (Lret)
If we don't include (Ignore), we still require idempotence in the
observation monad as discussed in Section 4.4 under "Idempotence of
mplus".
Our implementation does not eliminate duplicate results. But the laws
predict some duplication that does not occur in our implementation which
is why we require idempotence in the observation monad.
> Even if f (a ? b) =
> f a ? f b does not hold generally? This would contradict a statement I
> have made below.
As encapsulation violates this law, I'd like to postpone thinking about
encapsulation until I understand the laws for a language without
encapsulation but with anti. Or do you think encapsulation could clarify
the meaning of anti?
> >> 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.
I think even with a set-based notion of nondterminism one could
distinguish [0?1] and [0]?[1] if one allows sets to be nested inside
constructors.
> Do others think that encapsulation should behave
> differently in this example?
Can set functions distinguish [0?1] and [0]?[1] ?
> 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).
I think the distinction between sets and multisets is different from the
distinction between flat and nested nondeterminism. The former is about
allowing duplicates, the latter about nesting.
For example, using the sharing monad approach you can use a set- or a
multiset-monad but either way nondeterminism can be nested inside
constructors. (If you use a multi-set monad, the number of results may
differ from the number predicted by the laws as mentioned above.)
> 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.
Would nested set-based nondeterminism suffice?
Sebastian
_______________________________________________
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