+(\x.y)(ww) + * +y ++ +Done! 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! + -- 2.11.0