Michael writes:
> 2. More importantly, the computation with non-deterministic
> functions complicates from the beginning the operational
> meaning of programs. The current semantics consists of
> replacing equals by equals plus a (possibly) non-deterministic
> instantiation of free variables. However, the computation with
> non-deterministic functions requires the computation with
> sharing which is also considered in your calculus. Without
> sharing, the calculus is unsound. This is also the reason
> why our prototype implementation (which is not based on
> sharing) does not compute the correct results of your example,
> although it can deal with non-deterministic functions.
I find very intriguing the use of non-deterministic functions and
I think that it deserves serious consideration. I wonder if
someone could help me to clarify the soundness issue.
1. What does it mean that a calculus is sound (in the presence of
non-deterministic functions?)
2. What is the rationale for this definition?
3. What is a simple example of unsound computation?
Thanks,
Sergio
Received on Di Jan 28 1997 - 19:49:12 CET
This archive was generated by hypermail 2.3.0
: Do Feb 01 2024 - 07:15:04 CET