ω &ome
A computational system is said to be **confluent**, or to have the **ChurchRosser** or **diamond** property, if, whenever there are multiple possible evaluation paths, those that terminate always terminate in the same value. In such a system, the choice of which subexpressions to evaluate first will only matter if some of them but not others might lead down a nonterminating path.
+The diamond property is named after the shape of diagrams like the following:
+
++ ((\x.x)((\y.y) z))
+ / \
+ / \
+ / \
+ / \
+ ((\y.y) z) ((\x.x) z)
+ \ /
+ \ /
+ \ /
+ \ /
+ \ /
+ \ /
+ z
+
+
+Because the starting term contains more than one redex, we can imagine
+reducing the leftmost redex first (the left branch of the diagram) or
+else the rightmost redex (the right branch of the diagram). But
+because the lambda calculus is confluent, 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.
+
The untyped lambda calculus is confluent. So long as a computation terminates, it always terminates in the same way. It doesn't matter which order the subexpressions are evaluated in.
A computational system is said to be **strongly normalizing** if every permitted evaluation path is guaranteed to terminate. The untyped lambda calculus is not strongly normalizing: ω ω
doesn't terminate by any evaluation path; and (\x. y) (ω ω)
terminates only by some evaluation paths but not by others.
@@ 174,60 +225,12 @@ But is there any method for doing this in generalfor telling, of any given co
Interestingly, Church also set up an association between the lambda calculus and firstorder predicate logic, such that, for arbitrary lambda formulas `M` and `N`, some formula would be provable in predicate logic iff `M` and `N` were convertible. So since the righthand side is not decidable, questions of provability in firstorder predicate logic must not be decidable either. This was the first proof of the undecidability of firstorder predicate logic.
+## Efficiency
##More on evaluation strategies##

Here are notes on [[evaluation order]] that make the choice of which
lambda to reduce next the selection of a route through a network of
links.


##More on evaluation strategies##

Here (below) are notes on [[evaluation order]] that make the choice of which
lambda to reduce next the selection of a route through a network of
links.


More on Evaluation Order
========================

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:

 ((\x.x)((\y.y) z))
 / \
 / \
 / \
 / \
 ((\y.y) z) ((\x.x) z)
 \ /
 \ /
 \ /
 \ /
 \ /
 \ /
 z


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:
+Which evaluation strategy you adopt has implications not only for
+decidability and termination, but for efficiency. (Later in the
+course, it will have implications for the order in which side effects
+occur.)
((\x.w)((\y.y) z))
@@ 237,14 +240,14 @@ First, efficiency:
\ /
\ /
\ /
 w

+ w
+
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.
+If a function discards its argument, as `\x.w` does, it makes sense to
+prioritize redexes in which that function serves as the head, 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" is more efficient.
But:
@@ 254,10 +257,10 @@ But:
(((\y.y) z)((\y.y) z) ((\x.xx) z)
/  /
/ (((\y.y)z)z) /
 /  /
+ /  /
/  /
/  /
 (z ((\y.y)z))  /
+ (z ((\y.y)z))  /
\  /
.

@@ 268,7 +271,7 @@ 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.
+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.
@@ 276,44 +279,7 @@ 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.
+rightmost reducible lambda" is more efficient.
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:

(\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


Here we have a function that discards its argument on the left, and a
nonterminating 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 socalled 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 finegrained 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 leftmostalways 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.