Gaining control over order of evaluation
----------------------------------------

We know that evaluation order matters.  We're beginning to learn how
to gain some control over order of evaluation (think of Jim's abort handler).
We continue to reason about order of evaluation.

A superbly clear and lucid discussion can be found here:
[Sestoft: Demonstrating Lambda Calculus Reduction](http://tinyurl.com/27nd3ub).
Sestoft also provides a really lovely lambda evaluator, 
which allows you to select multiple evaluation strategies, 
and to see reductions happen step by step:
[Sestoft's lambda reduction webpage](http://ellemose.dina.kvl.dk/~sestoft/lamreduce/lamframes.html).


Evaluation order matters
------------------------

We've seen this many times.  For instance, consider the following
reductions.  It will be convenient to use the abbreviation `w =
\x.xx`.  I'll indicate which lambda is about to be reduced with a *
underneath:

<pre>
(\x.y)(ww)
 *
y
</pre>

Done!  We have a normal form.  But if we reduce using a different
strategy, things go wrong:

<pre>
(\x.y)(ww) =
(\x.y)((\x.xx)w) =
        *
(\x.y)(ww) =
(\x.y)((\x.xx)w) =
        *
(\x.y)(ww) 
</pre>

Etc.  

As a second reminder of when evaluation order matters, consider using
`Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function:

<pre>
Y (\f n. blah) =
(\f.(\h.f(hh))(\h.f(hh))) (\f n. blah) 
     *
(\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah) 
       *
(\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah) 
         *
(\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah) 
</pre>

And we never get the recursion off the ground.


Restricting evaluation: call by name, call by value
---------------------------------------------------

One way to begin to gain some control is by adjusting our notion of
beta reduction.  This strategy has some of the flavor of adding types,
but is actually a part of the untyped calculus.

In order to have a precise discussion, we'll need some vocabulary.
We've been talking about normal form (lambda terms that can't be
further reduced), and leftmost evaluation (the reduction strategy of
always choosing the left most reducible lambda); we'll need to refine
both of those concepts.

Kinds of normal form:
---------------------

Recall that there are three kinds of lambda term.  Let `a` be an
arbitrary variable, and let `M` and `N` be arbitrary terms:

<pre>
The pure untyped lambda calculus (again):

             Form     Examples  
Variable     a        x, y, z
Abstract     \aM      \x.x, \x.y, \x.\y.y
Application  MN       (x x), ((\x.x) y), ((\x.x)(\y.y))
</pre>

It will be helpful to define a *redex*, which is a lambda term of
the form `((\aM) N)`.  That is, a redex is a form for which beta
reduction is defined (ignoring, as usual, the manouvering required in
order to avoid variable collision).

It will also be helpful to have names for the two components of an
application `(M N)`: we'll call `M` the *functor*, and `N` the
*argument*.  Note that functor position can be occupied by a variable,
since `x` is in the functor position of the term `(x y)`.

Ok, with that vocabulary, we can distinguish four different types of 
normal form:







Take Plotkin's CBN CPS:

[x] ~~> x
[\xM] ~~> \k.k(\x[M])
[MN] ~~> \k.[M](\m.m[N]k)

let w = \x.xx in

[(\xy)(ww)] ~~>
\k.[\xy](\m.m[ww]k) ~~>
\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) ~~>
\k.[\xy](\m.m(\k.(\k.k(\x[xx]))(\m.m[w]k))k) ~~> beta*
\k.[\xy](\m.m(\k.(\x[xx])[w]k)k) ~~>
\k.[\xy](\m.m(\k.(\x(\k.[x](\m.m[x]k)))[w]k)k) ~~>
\k.[\xy](\m.m(\k.(\x(\k.x(\m.mxk)))[w]k)k) ~~> beta
\k.[\xy](\m.m(\k.[w](\m.m[w]k))k) --- same as second line!