Re: Comments from Madrid

From: Michael Hanus <hanus_at_medoc.informatik.rwth-aachen.de>
Date: Fri, 31 Jan 1997 13:58:00 +0100

Sergio Antoy wrote:
> 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.

I hoped that the original designers of the calculus with
non-deterministic functions sent you the answer. Since you are
waiting, I'll try to give a partial answer.

> 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?
>

My formulation was a little bit sloppy. In their ESOP'96 paper,
Paco et al. presented a basic proof calculus where a so-called
"call-time-choice" for non-determinism is required. This means
that the values of arguments must be chosen before the call.
Unfortunately, a deeper explanation for this restriction is not
presented (maybe Paco can comment this), but, as a consequence,
outermost rewriting is not sound w.r.t. this proof calculus.
For instance, consider the following program:

data nat = o ; s(nat).

coin = o.
coin = s(o).

add(o,N) = N.
add(s(M),N) = s(add(M,N)).

double(X) = add(X,X).

(like Curry, but with Prolog-like notation)

Now, the following results should be computed in their logic:

double(coin) --> o
double(coin) --> s(s(0))

but not:

double(coin) --> s(o)

In particular, double(coin) -> add(coin,coin)
is not a valid rewriting step in their logic.
Thus, our Curry implementation, which does not implement
sharing but only term rewriting, computes the following results:


|: double(coin).
 
s(s(o)) | s(o) | s(o) | o

This has the consequence that you have to base your proof calculus
on sharing common expressions.

Best regards,

Michael
Received on Fr Jan 31 1997 - 15:32:51 CET