On Mon, 3 Feb 1997, Sergio Antoy wrote:
> 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
>
>
Dear Sergio,
I have just read your e-mail as well as Paco's answers, where he already
gives most of the reasons I can think of. However, I can add some remarks:
1. Our notion of model for nondeterministic coonstructor based
rewriting programs is inspired by Hussmann's thesis (published
in Birkhauser Verlag). The terminology "call-time-choice" is
also Hussmann's. Chapter 1 in the thesis gives a very nice
overview, including good motivation.
2. This terminology corresponds to the rule adopted in Hussmann's
approach (and also in our approach) to compute the denotation
of an expression f(e1, ... ,en) in a given algebra: each ei
will denote a set Vi of values from the algebra's carrier, and
f(e1, ... , en) will denote the union of all sets f(v1 ,..., vn)
for vi running over Vi. (What is different in our approach w.r.t.
Hussmann's is the fact that we assume a partially ordered carrier
with bottom element and we require that expressions' denotations
are cones rather than arbitrary sets; this is needed to model
lazy partial functions, but not essential for the present discussion).
3. In particular, 2. applies to term algebras, whose carrier is the
set of all partial constructor terms.
4. In any given algebra, an approximation statement e -> t is defined
to hold iff t's denotation is a subset of e's denotation. Since
t's denotation is always a principal ideal (because t is a possibly
partial constructor term, and constructor are always interpreted
as deterministic functions), it is equivalent to say: e -> t holds
iff the maximal element in t's denotation belongs to e's denotation.
5. Now, soundness requires that, whenever e -> t is derived, e -> t
must hold in all models of the program; in particular, in the free
term model. This soundness requirement wouldn't be met by using
ordinary term rewriting and narrowing, as shown by the coin example
(also from Hussmann; see Section 1.2.3 in his Thesis, entitled
"Soundness: a negative result"). That's why we use the special
rewriting calculi in the ESOP'96 paper, and we formulate the
narrowing calculus in such a way that sharing is built in.
6. To summarize: in our approach, sharing is not merely an implementation
technique, adopted for the sake of efficiency, but a real need for
soundness w.r.t. the model-theoretic semantics we have adopted,
which we find a natural one.
7. A final remark regarding equations vs joinability statements: An
equation a = b should mean, w.r.t. our semantics, that a and b denote
the same set of values. Clearly, this doesn't yield a computable
notion. That's why we use joinabilty statements a >< b in conditions
and goals. A statement a >< b holds iff the denotations of a, b
include some common total value. This can be implemented (by search
of course). Moreover, the resulting language has initial semantics.
I hope to be helpfuk with these remarks.
Best Regards,
Mario.
Received on Di Feb 04 1997 - 11:26:11 CET
This archive was generated by hypermail 2.3.0
: Do Jun 20 2024 - 07:15:05 CEST