Re: Comments from Madrid

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