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

From: Sergio Antoy <antoy_at_cs.pdx.edu>

Date: Mon, 3 Feb 1997 08:58:40 -0800

Dear Paco,

Thanks for following up on my enquiry. Unfortunately, I think

that the most important of my questions has not been discussed.

You say:

*> Michael has done the work for me, with respect
*

*> to Sergio's questions.
*

*> ...
*

*> Michael explanation is right, and the 'coin' example
*

*> is quite illustrative.
*

But Michael says:

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

So may question is: Given the program (in Michael's notation)

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).

What's wrong with computing

double(coin) --> s(o)

My first feeling is that if a calculus does NOT compute it, then

it is incomplete. I am troubled by the fact that one should

compute

add(coin,coin) -> s(o)

Right? Moreover, double is a well-behaved, deterministic function,

thus for every t, one should compute

double(t) -> add(t,t)

I wonder if there is a very basic problem with ``equational

reasoning''. Rewriting has been used for equational (algebraic)

specifications to impose a direction for the replacement of equals

with equals. The rationale is that oriented equations make

computing (deductions) more efficient.

However, I do not regard a rule of a non-deterministic function,

such as permute for example, as an equation. Clearly,

permute [1,2,3] -> [2,1,3]

permute [1,2,3] -> [2,3,1]

...

but I do not think that [2,1,3] = [2,3,1] (or even that permute

[1,2,3] = [2,1,3]). My reason to use a non-deterministic function

such as permute is that if I have to solve, say, the n_queens

problem, then I am able to code a simpler program if I can use a

non-deterministic permute, than if I can't.

To be the devil's advocate, suppose that I want to know whether

there is more than one solution to my problem. I define a

(polymorphic) function

many_solutions x -> not (x = x)

and I solve

many_solution n_queens = true

What's wrong with that? To conclude, what is the rationale that

requires sharing, or bans outermost narrowing, when

non-deterministic functions are used?

Thanks,

Sergio

Received on Mo Feb 03 1997 - 18:10:46 CET

Date: Mon, 3 Feb 1997 08:58:40 -0800

Dear Paco,

Thanks for following up on my enquiry. Unfortunately, I think

that the most important of my questions has not been discussed.

You say:

But Michael says:

So may question is: Given the program (in Michael's notation)

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).

What's wrong with computing

double(coin) --> s(o)

My first feeling is that if a calculus does NOT compute it, then

it is incomplete. I am troubled by the fact that one should

compute

add(coin,coin) -> s(o)

Right? Moreover, double is a well-behaved, deterministic function,

thus for every t, one should compute

double(t) -> add(t,t)

I wonder if there is a very basic problem with ``equational

reasoning''. Rewriting has been used for equational (algebraic)

specifications to impose a direction for the replacement of equals

with equals. The rationale is that oriented equations make

computing (deductions) more efficient.

However, I do not regard a rule of a non-deterministic function,

such as permute for example, as an equation. Clearly,

permute [1,2,3] -> [2,1,3]

permute [1,2,3] -> [2,3,1]

...

but I do not think that [2,1,3] = [2,3,1] (or even that permute

[1,2,3] = [2,1,3]). My reason to use a non-deterministic function

such as permute is that if I have to solve, say, the n_queens

problem, then I am able to code a simpler program if I can use a

non-deterministic permute, than if I can't.

To be the devil's advocate, suppose that I want to know whether

there is more than one solution to my problem. I define a

(polymorphic) function

many_solutions x -> not (x = x)

and I solve

many_solution n_queens = true

What's wrong with that? To conclude, what is the rationale that

requires sharing, or bans outermost narrowing, when

non-deterministic functions are used?

Thanks,

Sergio

Received on Mo Feb 03 1997 - 18:10:46 CET

*
This archive was generated by hypermail 2.3.0
: Di Jan 18 2022 - 07:15:03 CET
*