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

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

Right? Moreover, double is a well-behaved, deterministic function,
thus for every t, one should compute

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 : Fr Okt 07 2022 - 07:15:15 CEST