- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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 Fri Jan 31 1997 - 15:32:51 CET

Date: Fri, 31 Jan 1997 13:58:00 +0100

Sergio Antoy wrote:

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.

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 Fri Jan 31 1997 - 15:32:51 CET

*
This archive was generated by hypermail 2.3.0
: Mon Sep 16 2019 - 07:15:04 CEST
*