(\x.y)(ww) * yDone! We have a normal form. But if we reduce using a different strategy, things go wrong:

(\x.y)(ww) = (\x.y)((\x.xx)w) = * (\x.y)(ww) = (\x.y)((\x.xx)w) = * (\x.y)(ww)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:

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)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:

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))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!