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