On Tue, 4 Feb 1997, Sergio Antoy wrote:
> Dear Curritos,
>
> Thanks for all the answers that I got from my enquiry regarding
> the soundness of the Madrid calculus for non-deterministic
> functions. Your messages were helpfull and I understand the
> calculus much better now.
>
> At the cost of being a bit crude, I would summarize the discussion
> as following. Given a TRS R, a value of f(t1,...tn) is a normal
> form (w.r.t. R) of f(v1,...vn) for all the values v1,...vn of
> t1,...tn respectively. This must be refined, since the calculus
> computes the value of f(t1,...tn) even when some ti has no value,
> if the value of ti is not needed, but with more accuracy, both
> simplicity and intuition go.
>
> This definition is reasonable and, of course, not all narrowing
> strategies are sound for this definition, as the double(coin)
> example shows. The existence of a sound and complete strategy for
> this definition in non-confluent, non-terminating systems is not
> at all obvious, and the Madrid group did a great job.
>
> Has anyone investigated an alternative notion of value? E.g.,
> values and data terms (constructor normal forms) coincide. This
> definition is simpler and would allow more computations, such as
> the ``many_solutions'' example of a previous posting. The
> difference between the two alternatives seems to boil down to the
> difference between call-by-value and call-by-name. Does anyone
> see major advantages or disadvantages of the latter? A simpler
> semantics is an advantage. The existence of a sound, complete,
> and efficient strategy for it is not obvious.
In case of adopting call-by-name, the use of sharing in the
implementation would mean incompleteness (again, this is
shown by the coin example). I think it is more sensible to
adopt call-time-choice, that permits sharing while respecting
soundness and completeness.
By the way: another reason why call-time-choice doesn't contradict
the spirit of lazy evaluation is the following: call-time-choice
is something like call-by-value, true, but values are partial
values (constructor terms with possible occurrences of the bottom
symbol).
>
> Finally, is Hussmann's work online? I did a Web search, but I
> could not find it.
>
I don't know about Hussmann's work online, but I can point to
his paper "Nondeterministic Algebraic Specifications and
Nonconfluent Term Rewriting", Journal of Logic Programming,
1992:12:237-255.
> Thanks again,
> Sergio
>
> --------------------------------
> Sergio Antoy
> Dept. of Computer Science
> Portland State University
> P.O.Box 751
> Portland, OR 97207
> voice +1 (503) 725-3009
> fax +1 (503) 725-3211
> internet antoy_at_cs.pdx.edu
> WWW http://www.cs.pdx.edu/~antoy
> --------------------------------
>
>
Best,
Mario.
---------------------------------------------------------------------------
Prof. Mario Rodriguez-Artalejo e-mail: mario_at_dia.ucm.es
Dpto. de Informatica y Automatica
http://mozart.mat.ucm.es/
Universidad Complutense de Madrid Fax: +34 1 3 94 46 07
Facultad de Matematicas Phone: +34 1 3 94 45 12
Av. Complutense s/n
E-28040 Madrid, Spain
---------------------------------------------------------------------------
Received on Mi Feb 05 1997 - 16:46:26 CET