Two questions: lazy evaluation and Church-Rosser

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Two questions: lazy evaluation and Church-Rosser

Gregory Woodhouse
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
[hidden email]

"Nothing is as powerful than an idea
whose time has come."
-- Victor Hugo



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Two questions: lazy evaluation and Church-Rosser

Ben Rudiak-Gould
In reply to this post by Gregory Woodhouse
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe