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
This archive was generated by hypermail 2.3.0
: Do Feb 01 2024 - 07:15:04 CET