Talk:Haskell/Graph reduction

From Wikibooks, the open-content textbooks collection

[edit] Explain Confluence?

Should we note that reduction is confluent, or rather that it might be imaginable that it's not? Arguably, this is assumed intuitively and an explanataion only eats space but doesn't add additional insights. Unless there's either an informal proof or a good non-confluent example, I wouldn't mention confluence at all. --apfeλmus 10:34, 20 June 2007 (UTC)

So far, we implicitely assumed that every sequence of reductions would yield the same normal form. After all, we're replacing equals by equals and the result should be the same. But "equal" only means that we can convert from one to the other by expanding function definitions (square 3 ⇒ 3*3) or abstracting a given expression into a function application (3*3 ⇒ square 3), there is no guarantee that always applying only one direction of the equivalence will lead to a unique normal form. Of course, intuition tells us that for expanding function applications, this should nevertheless be the case and we can in fact rely on the following

Theorem

Every Haskell expression has at most one normal form, i.e. the order of reduction doesn't change the result.

This follows more or less from the w:Church-Rosser theorem stating that the untyped lambda-calculus is confluent. We will not proof this here, but to appreciate the result, we'll show an example of a term rewriting system that does not enjoy unique normal forms.

Show the example!

The confluence theorem is of interest when studying deeply lambda-calculus and reduction strategies of lambda-terms; however, it has a nontrivial part, mentioning that every 'terminating' sequence of reduction leads to the same normal form. But (λxy.x)1Ω terminates only with a call-by-name strategy (like Haskell's one), not with a call-by-value one.

Reduction order is also important for infinite data structures.

So, what you say is correct as long as the reduction strategy is lazy.

--Blaisorblade (talk) 15:52, 6 January 2008 (UTC)

[edit] Solutions to Graph reduction exercises

There ought to be a tool that automatically generates solutions to these exercises, so that we don't have to do it ourselves. -- apfeλmus 13:58, 21 June 2007 (UTC)

[edit] Supercombinators means Combinatory logic?

The page mentions supercombinators about GHC implementation. Are you talking about the ones in: http://en.wikipedia.org/wiki/Combinatory_logic ?

Yes, pretty much. Apparently, this wikibook section is not written yet, the todo notes just track what I have in mind for it. The notes are based on SPJ's book [1] chapter 13, in particular 13.2.1.

The question arises since I've read in http://www.cl.cam.ac.uk/teaching/Lectures/founds-fp/Founds-FP.ps.gz (lecture notes of a Cambridge course) about the work of David Turner (also mentioned in the above wikipedia article), who used them to implement graph reduction. The naive approach exposed in the article does not work well because the graph representing a function may be shared, so you must either copy the graph before starting reductions, or use combinators (I've not yet fully understood the solution).

It's actually fairly simple. For evaluating something like (λx.(x+1)+2)5, there are several options:

• Copy the body ((x+1)+2) and replace every occurrence of x with 5.
• Evaluate the body ((x+1)+2) while keeping in mind that x=5 (environment).
• Defer the "keep in mind" part to the lambda expression, i.e. use (super-)combinators which looks like (λx.(λx.x+1)x+2)5. In other words, instead of storing expressions as expr where I kept in mind that x=5, store them as (λx.expr)5. This is pretty neat and thus that's how ghc and others do it.

Btw, thanks for your lecture notes, I think they make a very good reference concerning lambda calculus for the wikibook.

-- apfeλmus 10:17, 6 January 2008 (UTC)