Re: Invertible nondeterminism?

From: Sebastian Fischer <>
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.


curry mailing list
Received on Fr Dez 17 2010 - 14:22:59 CET

This archive was generated by hypermail 2.3.0 : Di Sep 29 2020 - 07:15:03 CEST