Re: [Haskell-cafe] Two questions: lazy evaluation and Church-Rosser
Gregory Woodhouse wrote: 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 Just wanted to point out that call-by-name is non-strict. Lazy evaluation is basically just call-by-name with extra sharing; if you only care about semantics and not time/space behavior, it's the same as call-by-name. (much less infinite lists and comprehensions). In a lazy or call-by-name operational semantics, you never get infinite lists, just lists with unevaluated tails which get unwrapped as needed. List comprehensions in Haskell are syntactic sugar. The Haskell 98 report explains how to transform them away. -- Ben ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Two questions: lazy evaluation and Church-Rosser
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? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Two questions: lazy evaluation and Church-Rosser
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? === Gregory Woodhouse [EMAIL PROTECTED] Nothing is as powerful than an idea whose time has come. -- Victor Hugo ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
