Re: Comments from Madrid

From: Mario Rodriguez Artalejo <mario_at_eucmos.sim.ucm.es>
Date: Tue, 04 Feb 1997 11:18:45 +0100 (MET)

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 Tue Feb 04 1997 - 11:26:11 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 23 2019 - 07:15:04 CEST