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 gregory.woodhouse@sbcglobal.net "Nothing is as powerful than an idea whose time has come." -- Victor Hugo
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
participants (2)
-
Ben Rudiak-Gould -
Gregory Woodhouse