- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

Date: Fri, 17 Dec 2010 09:25:36 +0900

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

Date: Fri, 17 Dec 2010 09:25:36 +0900

Hi Jan,

On Thu, 2010-12-16 at 23:08 +0100, Jan Christiansen wrote:

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 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.

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?

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.

Can set functions distinguish [0?1] and [0]?[1] ?

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.)

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

*
This archive was generated by hypermail 2.3.0
: Mo Okt 26 2020 - 07:15:05 CET
*