[Prev][Next][Index][Thread]

Re: Why Prolog and CBV?

Date: Sun, 17 Nov 91 20:36:26 PST
To: mitchell wand <wand@cheech.lcs.mit.edu>

   It gets more than confusing:  it gets non-CR.  Consider
 
   ((begin
      (set! x 3)
      (lambda (u) x))
    (begin
      (set! x 4)
      5))

Yes. But suppose we fix leftmost evaluation. Then who
cares about confluence? More specifically, we could begin with
a set of rules, identify the normal forms (and optionally,
observable types) and notice that leftmost evaluation 
always finds a normal form if there is one. Confluence
is nice, and gives us some useful properties, but I am not
sure why it should be the most important criterion.
CBV isn't ``confluent'' either, for any interpretation I
can give to an evaluation order being confluent. 

The usual argument for CBV, in my experience, has been the overhead
of building closures. We should be able to find something more
mathematical, in this day and age. I guess partial functions
are a reasonable justification, but still do not give a general 
view of why or when an approximation to a "complete" strategy
is computationally preferable.

An interesting example, by the way, is the generalized Takeuchi
function considered in Knuth's contribution to the recently
published McCarthy volume (in honor of his 64th birthday; Academic
Press). The ordinary 3-argument version is

 fun tak(x,y,z) = if x<=y then y
      else tak(tak(x-1,y,z),tak(y-1,z,x),tak(z-1,x,y));

which is much easier to prove total under lazy evaluation 
than CBV. In fact, termination for the general function 
(of k arguments) under CBV is open. (The running time of 
this function may be very long, without using a large 
amount of stack space. It is sometimes used for Lisp, etc.
benchmarks.)

John Mitchell