Re: Why Prolog and CBV?

Subject: Re: Why Prolog and CBV?
From: matthias@cs.rice.edu (Matthias Felleisen)
Date: Tue, 19 Nov 91 13:38:15 EST
Cc: types
Sender: meyer@theory.lcs.mit.edu
From: Andrew.Pitts@cl.cam.ac.uk
To: matthias@cs.rice.edu (Matthias Felleisen)
Cc: types@theory.lcs.mit.edu
Subject: Re: Why Prolog and CBV?
In-Reply-To: Your message of Mon, 18 Nov 91 11:15:10 -0500. <199111181615.AA13787@stork.lcs.mit.edu>
Date: Tue, 19 Nov 91 09:57:02 +0000

Matthias says in passing:

>I would again agree w/ Wadler here that
>call-by-need is most difficult to reason about: the rules for cbn are
>some of the most complex I have seen. (This result is only in Crank's
>thesis not the paper.)

Nevertheless I'd like to see them. (Well, maybe `like' is the wrong word!) More
generally does anyone have other references for treatments of call-by-need using
structured operational semantics?

Andy Pitts

-------------------------------------------------------------------------------

Date: Tue, 19 Nov 91 12:26:59 CST
To: Andrew.Pitts@cl.cam.ac.uk

Here are two answers: 

1.Here is the one change that you have to make to the c-b-name rules
  to get c-b-need:  

    (\lambda x.M)M' --> (letrec ([x (set! x M')]) M) 	(beta-by-need)

  When I said "complex rules" I really meant "complex uses of rules",
  i.e., when you trace programs in this rule set you get strange
  results. 

  An aside: if the starting point is a program in the set! free subset,
  you can use beta. By comparing the reduction sequences you can also
  see that call-by-need evaluates each argument to a value at most once,
  which is the intended characteristic. 

2. The references are: 

   [1] {Crank, E. and M. Felleisen}.  Parameter-passing and the
   lambda-calculus.  In {\it Proc. 18th ACM Symposium on Principles of
   Programming Languages\/}, 1990, 233--245.

   [2] {Crank, E}.  Parameter-passing and the lambda-calculus.  Master's
   Thesis, Rice University, August 1990.

   [3] {Cartwright, R.S. and M. Felleisen}.  Observable sequentiality and
   full abstraction.  In {\it Proc. 19th ACM Symposium on Principles of
   Programming Languages}, 1992, to appear. (We are also in the process
   of writing up an extended tech rpt version of this paper.)

I hope that one of the above answers is what you were asking for. Let
me know if not and I'll try to provide the information. 

-- Matthias


END