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.
Finally, is Hussmann's work online? I did a Web search, but I
could not find it.
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
--------------------------------
Received on Mi Feb 05 1997 - 08:25:54 CET