Re: Invertible nondeterminism?

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Fri, 17 Dec 2010 22:02:47 +0900

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 Fri Dec 17 2010 - 14:22:59 CET

This archive was generated by hypermail 2.3.0 : Thu Sep 19 2019 - 07:15:08 CEST