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

From: Jan Christiansen <jac_at_informatik.uni-kiel.de>

Date: Fri, 17 Dec 2010 13:15:33 +0100

On 17.12.2010, at 01:25, Sebastian Fischer wrote:

*> 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?
*

It was supposed to be a mathematical construct in the semantics.

By the way I would expect that something like

f (a ? b) ]= f a ? f b

always holds where ]= is the "superset" relation on multisets.

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

Wouldn't another alternative be to demand f (a ? b) = f a ? f b for

strict functions f only? The inequational law above as well as the

restriction of the law to strict functions strongly reminds me of free

theorems in functional programming. There you have to assure that

certain functions are strict to get an equational law as well.

*> 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?
*

No.

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

You are correct. I have mixed these up because I suspect that you need

nesting if you want multisets. But it is not the other way round. On

the other hand if you have the "pain" of using nesting in a formal

model you can as well use multisets and get the benefits. For example,

you can reason about duplicate results. You most certainly want to

minimize the number of results and prevent duplicates. There might be

simple transformation laws which translate programs which yield

duplicate results into program which yield every result once. But this

is another topic.

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 - 13:51:44 CET

Date: Fri, 17 Dec 2010 13:15:33 +0100

On 17.12.2010, at 01:25, Sebastian Fischer wrote:

It was supposed to be a mathematical construct in the semantics.

By the way I would expect that something like

f (a ? b) ]= f a ? f b

always holds where ]= is the "superset" relation on multisets.

Wouldn't another alternative be to demand f (a ? b) = f a ? f b for

strict functions f only? The inequational law above as well as the

restriction of the law to strict functions strongly reminds me of free

theorems in functional programming. There you have to assure that

certain functions are strict to get an equational law as well.

No.

You are correct. I have mixed these up because I suspect that you need

nesting if you want multisets. But it is not the other way round. On

the other hand if you have the "pain" of using nesting in a formal

model you can as well use multisets and get the benefits. For example,

you can reason about duplicate results. You most certainly want to

minimize the number of results and prevent duplicates. There might be

simple transformation laws which translate programs which yield

duplicate results into program which yield every result once. But this

is another topic.

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 - 13:51:44 CET

*
This archive was generated by hypermail 2.3.0
: Mo Jan 27 2020 - 07:15:11 CET
*