- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

Date: Tue, 04 Feb 1997 11:18:45 +0100 (MET)

On Mon, 3 Feb 1997, Sergio Antoy wrote:

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
: Fr Mai 29 2020 - 07:15:03 CEST
*