[Prev][Next][Index][Thread]
Re: Why Prolog and CBV?
-
Subject: Re: Why Prolog and CBV?
-
From: John C. Mitchell <jcm@cs.stanford.edu>
-
Date: Fri, 15 Nov 91 17:36:44 EST
-
Cc: types
-
In-Reply-To: Harper's message of Fri, 15 Nov 91 10:41:07 -0500. <199111151541.AA12537@stork.lcs.mit.edu>
-
Sender: meyer@theory.lcs.mit.edu
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