Hi Jan,
> 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.
Yes, even with run/eval-time choice semantics.
> Wouldn't another alternative be to demand f (a ? b) = f a ? f b for
> strict functions f only?
Yes, this law holds in a lazy language with call-time choice and does
not imply idempotence (I think):
f (a ? b) = f a ? f b if f failure = failure
(Depending on whether failure is the same as nontermination the
condition may be something else than strictness.)
It's a bit sad that this seems like a very strong restriction: The good
thing about call-time choice is that it allows to reason about *lazy*
nondeterministic computations as if they were *eager* computations. The
above law only allows to reason about *eager* computations as if they
were *eager* computations ;o) So one probably needs additional
"call-time choice laws" if one wants a complete calculus.
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Dez 17 2010 - 14:22:59 CET