```      ⇧+ ¢ ⇧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)
*
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)
```