⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ ⇧c) I = \k.⇧+(\f.⇧a(\x.k(fx))) ¢ (⇧+ ¢ shift' ¢ ⇧c) I = \k.(\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.k(fx))) I ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.I(fx))) ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(f)) ~~> ⇧+(\f.⇧a(\x.(\f.(⇧+ ¢ shift' ¢ ⇧c)(f))(fx)))) ~~> ⇧+(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx))) = (\k.k+)(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx))) ~~> ⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x)) = (\k.ka)(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x)) ~~> (⇧+ ¢ shift' ¢ ⇧c)(+a) = (\k.⇧+(\f.shift(\x.k(fx)))) ¢ ⇧c (+a) = (\k.(\k.⇧+(\f.shift(\x.k(fx))))(\f.⇧c(\x.k(fx))))(+a) ~~> (\k.⇧+(\f.shift(\x.k(fx))))(\f'.⇧c(\x'.(+a)(f'x'))) ~~> ⇧+(\f.shift(\x.(\f'.⇧c(\x'.(+a)(f'x')))(fx))) ~~> ⇧+(\f.shift(\x.⇧c(\x'.(+a)((fx)x')))) = (\k.k+)(\f.shift(\x.⇧c(\x'.(+a)((fx)x')))) ~~> shift(\x.⇧c(\x'.(+a)((+x)x')))) = shift(\x.(\k.kc)(\x'.(+a)((+x)x')))) ~~> shift(\x.(+a)((+x)c))So now we see what the argument of shift will be: a function k from strings x to the string asc. So shift k will be k(k "") = aacc. Ok, this is ridiculous. We need a way to get ahead of this deluge of lambda conversion. We'll see how to understand what is going on when we talk about quantifier raising in the next lecture. ## Viewing Montague's PTQ as CPS Montague's conception of determiner phrases as generalized quantifiers is a limited form of continuation-passing. (See, e.g., chapter 4 of Barker and Shan 2014.) Start by assuming that ordinary DPs such as proper names denote objects of type `e`. Then verb phrases denote functions from individuals to truth values, i.e., functions of type `e -> t`. The meaning of extraordinary DPs such as *every woman* or *no dog* can't be expressed as a simple individual. As Montague argued, it works much better to view them as predicates on verb phrase meanings, i.e., as having type `(e->t)->t`. Then *no woman left* is true just in case the property of leaving is true of no woman: no woman: \k.not \exists x . (woman x) & kx left: \x.left x (no woman) (left) = not \exists x . woman x & left x Montague also proposed that all determiner phrases should have the same type. After all, we can coordinate proper names with quantificational DPs, as in *John and no dog left*. Then generalized quantifier corresponding to the proper name *John* is the quantifier `\k.kj`. ## How continuations can simulate other monads Because the continuation monad allows the result type ρ to be any type, we can choose ρ in clever ways that allow us to simulate other monads. Reader: ρ = env -> α State: ρ = s -> (α, s) Maybe: ρ = Just α | Nothing You see how this is going to go. Let's see an example by adding an abort operator to our task language, which represents what we want to have happen if we divide by zero, where what we want to do is return Nothing. abort k = Nothing mid a k = k a map2 f u v k = u(\u' -> v (\v' -> k(f u' v'))) t13 = map2 (++) (mid "a") (map2 (++) (mid "b") (map2 (++) (mid "c") (mid "d"))) t13 (\k->Just k) == Just "abcd" t14 = map2 (++) (mid "a") (map2 (++) abort (map2 (++) (mid "c") (mid "d"))) t14 (\k->Just k) == Nothing Super cool. ## Continuation Passing Style Transforms 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 lucid discussion of evaluation order in the context of the lambda calculus can be found here: [Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf). Sestoft also provides a lovely on-line lambda evaluator: [Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html), which allows you to select multiple evaluation strategies, and to see reductions happen step by step. 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:

(\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. Using a Continuation Passing Style transform to control order of evaluation --------------------------------------------------------------------------- We'll present a technique for controlling evaluation order by transforming a lambda term using a Continuation Passing Style transform (CPS), then we'll explore what the CPS is doing, and how. In order for the CPS to work, we have to adopt a new restriction on beta reduction: beta reduction does not occur underneath a lambda. That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to `\u.z`, because the `\u` protects the redex in the body from reduction. (In this context, a "redex" is a part of a term that matches the pattern `...((\xM)N)...`, i.e., something that can potentially be the target of beta reduction.) Start with a simple form that has two different reduction paths: reducing the leftmost lambda first: `(\x.y)((\x.z)u) ~~> y` reducing the rightmost lambda first: `(\x.y)((\x.z)u) ~~> (\x.y)z ~~> y` After using the following call-by-name CPS transform---and assuming that we never evaluate redexes protected by a lambda---only the first reduction path will be available: we will have gained control over the order in which beta reductions are allowed to be performed. Here's the CPS transform defined: [x] = x [\xM] = \k.k(\x[M]) [MN] = \k.[M](\m.m[N]k) Here's the result of applying the transform to our simple example: [(\x.y)((\x.z)u)] = \k.[\x.y](\m.m[(\x.z)u]k) = \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) = \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k) Because the initial `\k` protects (i.e., takes scope over) the entire transformed term, we can't perform any reductions. In order to watch the computation unfold, we have to apply the transformed term to a trivial continuation, usually the identity function `I = \x.x`. [(\x.y)((\x.z)u)] I = (\k.[\x.y](\m.m[(\x.z)u]k)) I * [\x.y](\m.m[(\x.z)u] I) = (\k.k(\x.y))(\m.m[(\x.z)u] I) * * (\x.y)[(\x.z)u] I --A-- * y I The application to `I` unlocks the leftmost functor. Because that functor (`\x.y`) throws away its argument (consider the reduction in the line marked (A)), we never need to expand the CPS transform of the argument. This means that we never bother to reduce redexes inside the argument. Compare with a call-by-value xform: {x} = \k.kx {\aM} = \k.k(\a{M}) {MN} = \k.{M}(\m.{N}(\n.mnk)) This time the reduction unfolds in a different manner: {(\x.y)((\x.z)u)} I = (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I * {\x.y}(\m.{(\x.z)u}(\n.mnI)) = (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI)) * * {(\x.z)u}(\n.(\x.{y})nI) = (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI) * {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) = (\k.k(\x.{z}))(\m.{u}(\n.mn(\n.(\x.{y})nI))) * * {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) = (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI)) * * (\x.{z})u(\n.(\x.{y})nI) --A-- * {z}(\n.(\x.{y})nI) = (\k.kz)(\n.(\x.{y})nI) * * (\x.{y})zI * {y}I = (\k.ky)I * I y In this case, the argument does get evaluated: consider the reduction in the line marked (A). Both xforms make the following guarantee: as long as redexes underneath a lambda are never evaluated, there will be at most one reduction available at any step in the evaluation. That is, all choice is removed from the evaluation process. Now let's verify that the CBN CPS avoids the infinite reduction path discussed above (remember that `w = \x.xx`): [(\x.y)(ww)] I = (\k.[\x.y](\m.m[ww]k)) I * [\x.y](\m.m[ww]I) = (\k.k(\x.y))(\m.m[ww]I) * * (\x.y)[ww]I * y I Questions and exercises: 1. Prove that {(\x.y)(ww)} does not terminate. 2. Why is the CBN xform for variables `[x] = x` instead of something involving kappas (i.e., `k`'s)? 3. Write an Ocaml function that takes a lambda term and returns a CPS-xformed lambda term. You can use the following data declaration: type form = Var of char | Abs of char * form | App of form * form;; 4. The discussion above talks about the "leftmost" redex, or the "rightmost". But these words apply accurately only in a special set of terms. Characterize the order of evaluation for CBN (likewise, for CBV) more completely and carefully. 5. What happens (in terms of evaluation order) when the application rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.mnk))`? 6. A term and its CPS xform are different lambda terms. Yet in some sense they "do" the same thing computationally. Make this sense precise. Thinking through the types -------------------------- This discussion is based on [Meyer and Wand 1985](http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.44.7943&rep=rep1&type=pdf). Let's say we're working in the simply-typed lambda calculus. Then if the original term is well-typed, the CPS xform will also be well-typed. But what will the type of the transformed term be? The transformed terms all have the form `\k.blah`. The rule for the CBN xform of a variable appears to be an exception, but instead of writing `[x] = x`, we can write `[x] = \k.xk`, which is eta-equivalent. The `k`'s are continuations: functions from something to a result. Let's use σ as the result type. The each `k` in the transform will be a function of type ρ --> σ for some choice of ρ. We'll need an ancilliary function ': for any ground type a, a' = a; for functional types a->b, (a->b)' = ((a' -> σ) -> σ) -> (b' -> σ) -> σ. Call by name transform Terms Types [x] = \k.xk [a] = (a'->o)->o [\xM] = \k.k(\x[M]) [a->b] = ((a->b)'->o)->o [MN] = \k.[M](\m.m[N]k) [b] = (b'->o)->o Remember that types associate to the right. Let's work through the application xform and make sure the types are consistent. We'll have the following types: M:a->b N:a MN:b k:b'->o [N]:(a'->o)->o m:((a'->o)->o)->(b'->o)->o m[N]:(b'->o)->o m[N]k:o [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o [M](\m.m[N]k):o [MN]:(b'->o)->o Be aware that even though the transform uses the same symbol for the translation of a variable (i.e., `[x] = x`), in general the variable in the transformed term will have a different type than in the source term. Excercise: what should the function ' be for the CBV xform? Hint: see the Meyer and Wand abstract linked above for the answer. Other CPS transforms -------------------- It is easy to think that CBN and CBV are the only two CPS transforms. (We've already seen a variant on call-by-value one of the excercises above.) In fact, the number of distinct transforms is unbounded. For instance, here is a variant of CBV that uses the same types as CBN: