From 4e90575923350315ab60968f7ca746af5f6a101d Mon Sep 17 00:00:00 2001
From: Chris Barker <barker@kappa.linguistics.fas.nyu.edu>
Date: Mon, 27 Sep 2010 13:55:17 -0400
Subject: [PATCH] edits

---
 evaluation_order.mdwn | 125 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 125 insertions(+)
 create mode 100644 evaluation_order.mdwn

diff --git a/evaluation_order.mdwn b/evaluation_order.mdwn
new file mode 100644
index 00000000..3cd25fb5
--- /dev/null
+++ b/evaluation_order.mdwn
@@ -0,0 +1,125 @@
+This discussion elaborates on the discussion of evaluation order in the
+class notes from week 2.  It makes use of the reduction diagrams drawn
+in class, which makes choice of evaluation strategy a choice of which
+direction to move through a network of reduction links.
+
+
+Some lambda terms can be reduced in different ways:
+
+<pre>
+                     ((\x.x)((\y.y) z))
+                       /      \
+                      /        \  
+                     /          \
+                    /            \
+                    ((\y.y) z)   ((\x.x) z)
+                      \             /
+                       \           /
+                        \         /
+                         \       /
+                          \     /
+                           \   /
+                             z
+</pre>
+
+But because the lambda calculus is confluent (has the diamond
+property, named after the shape of the diagram above), no matter which
+lambda you choose to target for reduction first, you end up at the
+same place.  It's like travelling in Manhattan: if you walk uptown
+first and then head east, you end up in the same place as if you walk
+east and then head uptown.
+
+But which lambda you target has implications for efficiency and for 
+termination.  (Later in the course, it will have implications for
+the order in which side effects occur.)
+
+First, efficiency:
+
+<pre>
+                      ((\x.w)((\y.y) z))
+                        \      \
+                         \      ((\x.w) z)
+                          \       /
+                           \     /
+                            \   /
+                             \ /
+                              w    
+</pre>                    
+
+If a function discards its argument (as `\x.w` does), it makes sense
+to target that function for reduction, rather than wasting effort
+reducing the argument only to have the result of all that work thrown
+away.  So in this situation, the strategy of "always reduce the
+leftmost reducible lambda" wins.
+
+But:
+
+<pre>
+                        ((\x.xx)((\y.y) z))
+                          /       \
+     (((\y.y) z)((\y.y) z)         ((\x.xx) z)
+        /         |                  /
+       /          (((\y.y)z)z)      /
+      /              |             / 
+     /               |            /
+    /                |           /
+    (z ((\y.y)z))    |          / 
+         \           |         /
+          -----------.---------
+                     |
+                     zz
+</pre>
+
+This time, the leftmost function `\x.xx` copies its argument.
+If we reduce the rightmost lambda first (rightmost branch of the
+diagram), the argument is already simplified before we do the
+copying.  We arrive at the normal form (i.e., the form that cannot be
+further reduced) in two steps.  
+
+But if we reduce the rightmost lambda first (the two leftmost branches
+of the diagram), we copy the argument before it has been evaluated.
+In effect, when we copy the unreduced argument, we double the amount
+of work we need to do to deal with that argument.
+
+So when the function copies its argument, the "always reduce the
+rightmost reducible lambda" wins.
+
+So evaluation strategies have a strong effect on how many reduction
+steps it takes to arrive at a stopping point (e.g., normal form).
+
+Now for termination:
+
+<pre>
+(\x.w)((\x.xxx)(\x.xxx))
+ |      \
+ |       (\x.w)((\x.xxx)(\x.xxx)(\x.xxx))
+ |        /      \
+ |       /        (\x.w)((\x.xxx)(\x.xxx)(\x.xxx)(\x.xxx))
+ |      /          /       \
+ .-----------------         etc.
+ |
+ w
+</pre>
+
+Here we have a function that discards its argument on the left, and a
+non-terminating term on the right.  It's even more evil than Omega,
+because it not only never reduces, it generates more and more work
+with each so-called reduction.  If we unluckily adopt the "always
+reduce the rightmost reducible lambda" strategy, we'll spend our days
+relentlessly copying out new copies of \x.xxx.  But if we even once
+reduce the leftmost reducible lambda, we'll immediately jump to the
+normal form, `w`.
+
+We can roughly associate the "leftmost always" strategy with call by
+name (normal order), and the "rightmost always" strategy with call by
+value (applicative order).  There are fine-grained distinctions among
+these terms of art that we will not pause to untangle here.
+
+If a term has a normal form (a reduction such that no further
+reduction is possible), then a leftmost-always reduction will find it.
+(That's why it's called "normal order": it's the evaluation order that
+guarantees finding a normal form if one exists.)
+
+Preview: if the evaluation of a function has side effects, then the
+choice of an evaluation strategy will make a big difference in which
+side effect occur and in which order.
-- 
2.11.0