Re: Comments from Madrid

From: Sergio Antoy <antoy_at_cs.pdx.edu>
Date: Tue, 28 Jan 1997 09:38:03 -0800

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