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