# Re: Why Prolog and CBV?

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?
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

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

`