[Haskell-cafe] Two questions: lazy evaluation and Church-Rosser

[Ezra Cooper]

Gregory,

Church-Rosser is proved in any good text on lambda calculus, such as 
Barendregt [1]. Some rather detailed notes on that book are at [2].

Lazy evaluation is often formalized as "call-by-need." Try [3].

Ezra

[1] Barendregt. The Lambda Calculus 
<http://www.amazon.com/exec/obidos/ASIN/0444875085>
[2] <http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html>
[3] Maraist, Odersky, and Wadler, "A call-by-need lambda-calculus." 
Journal of Functional Programming 8(3):275-317 (May 1998). 
<http://homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html>

On Nov 15, 2005, at 5:30 AM, Gregory Woodhouse wrote:

> This is surely a dumb question, but where can I find a proof of the 
> Church-Rosser theorem?
>
> Now, a totally(?) separate question: I've been trying to do some 
> background reading on lambda calculus, and have found discussions of 
> strict evaluation strategies (call-by-value and  call-by-name) but 
> have yet to find an appropriate framework for modeling lazy evaluation 
> (much less infinite lists and comprehensions). Can anyone point me in 
> the right direction?