Why Prolog and CBV?

Subject: Why Prolog and CBV?
From: mitchell wand <wand@cheech.lcs.mit.edu>
Date: Sun, 17 Nov 91 20:22:31 EST
Cc: types@theory.lcs.mit.edu
In-Reply-To: John C. Mitchell's message of Fri, 15 Nov 91 17:36:44 EST <199111152236.AA12993@stork.lcs.mit.edu>
Sender: meyer@theory.lcs.mit.edu

Date: Sun, 17 Nov 91 13:57:17 -0500
To: jcm@cs.stanford.edu
cc: gunter@cis.upenn.edu

   Date: Fri, 15 Nov 91 17:36:44 EST
   Cc: types@theory.lcs.mit.edu
   From: John C. Mitchell <jcm@cs.stanford.edu>
   Sender: meyer@theory.lcs.mit.edu
   Subject: Re: Why Prolog and CBV? 

   Date: Fri, 15 Nov 91 10:39:25 PST
   To: Robert_Harper@GOTTLOB.TIP.CS.CMU.EDU

      What does seem to be the case is that if one integrates
      effects into the language in roughly the style of ML (eg,
      with ref types), then cbv is essentially forced on you for
      reasons of determinacy.

   I realize that this is accepted by many, but what is the mathematical
   reason for it, if any? Leftmost evaluation is certainly deterministic.
   If asked, I would make up some story about a call f(e), where e contains
   an assignment, and say that with cbn it is hard to predict where in
   the evaluation of the body of f this assignment would be done.
   If the body of f assigns to or reads the same variable, it gets
   confusing. Does anyone have a ready-made explanation that is more
   precise, say involving proof rules?

   John

It gets more than confusing:  it gets non-CR.  Consider

((begin
   (set! x 3)
   (lambda (u) x))
 (begin
   (set! x 4)
   5))

which gives different results depending on the order of evaluation of the
operator and operand.  As we speak, this very debate is raging on
comp.lang.scheme, over the issue of the order of evaluation of arguments in
Scheme.  I wish I could report that anything new or interesting was being said
there, however.

--Mitch