author Chris Wed, 13 May 2015 17:04:45 +0000 (13:04 -0400) committer Chris Wed, 13 May 2015 17:04:45 +0000 (13:04 -0400)

index 0b99065..42f2c11 100644 (file)
@@ -65,7 +65,7 @@ We have to lift each functor (+) and each object (e.g., "b") into the
application, where

-    ¢ mf mx = \k -> mf (\f -> mx (\a -> k(f x)))
+    ¢ M N = \k -> M (\f -> N (\a -> k(f x)))

@@ -73,17 +73,16 @@ The way in which we extract a value from a continuation box is by
applying it to a continuation; often, it is convenient to supply the
trivial continuation, the identity function \k.k = I.  So in fact,

-   t1 = mt1 I
+    t1 = mt1 I

That is, the original computation is the monadic version applied to
the trivial continuation.

-We can now imagine replacing the third element ("c") with a shifty
-operator.  We would like to replace just the one element, and we will
-do just that in a moment; but in order to simulate the original task,
-we'll have to take a different strategy initially.  We'll start by
-imagining a shift operator that combined direction with the tail of
-the list, like this:
+We can now add a shifty operator.  We would like to replace just the
+one element, and we will do just that in a moment; but in order to
+simulate the original task, we'll have to take a different strategy
+initially.  We'll start by imagining a shift operator that combined
+direction with the tail of the list, like this:

mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))

@@ -96,7 +95,7 @@ and a string continuation k of type [Char] -> [Char].  Since u is the
the argument to shift, it represents the tail of the list after the
shift operator.  Then k is the continuation of the expression headed
by `shift`.  So in order to execute the task, shift needs to invoke k
-twice.
+twice.  The expression `\s.k(ks)` is just the composition of k with itself.

mt2 I == "ababd"

@@ -118,19 +117,26 @@ For a reset operator #, we can have

# u k = k(u(\k.k))   -- ex.: ab#deSf ~~> abdedef

+The reset operator executes the remainder of the list separately, by
+giving it the trivial continuation (\k.k), then feeds the result to
+the continuation corresponding to the position of the reset.
+
a way that conforms to our by-now familiar strategy of lifting a
computation into a monad, and then writing a few key functions (shift,
reset) that exploit the power of the monad.

+## Generalizing to the tree doubling task
+
Now we should consider what happens when we write a shift operator
that takes the place of a single letter.

mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
mt4 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ shift' ¢ ⇧d))

-Instead of mt2, we have mt4.  So now the type of "c" (a boxed string,
-type M[Char]) is the same as the type of the new shift operator, shift'.
+Instead of mt2 (copied from above), we have mt4.  So now the type of a
+leaf (a boxed string, type M[Char]) is the same as the type of the new
+shift operator, shift'.

shift' = \k.k(k"")

@@ -179,6 +185,7 @@ Let's go back to a simple one-shift example, "aSc".  Let's trace what
the shift' operator sees as its argument k by replacing ⇧ and ¢ with
their definitions:

+<pre>
⇧+ ¢ ⇧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
@@ -199,106 +206,14 @@ their definitions:
~~> shift(\x.⇧c(\x'.(+a)((+x)x'))))
= shift(\x.(\k.kc)(\x'.(+a)((+x)x'))))
~~> shift(\x.(+a)((+x)c))
+</pre>

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 adapt the notational strategy developed in
-Barker and Shan 2014:
-
-
-    \k.g(kf): (α -> ρ) -> ρ
-
-we'll write
-
-    g[]    ρ
-    --- : ---
-     f     α
-
-Then
-             []
-    mid(x) = --
-             x
-
-and
-
-    g[]    ρ      h[]    ρ    g[h[]]    ρ
-    --- : ----  ¢ --- : --- = ------ : ---
-     f    α->β     x     α     fx       β
-
-Here's the justification:
-
-        (\FXk.F(\f.X(\x.k(fx)))) (\k.g(kf)) (\k.h(kx))
-    ~~> (\Xk.(\k.g(kf))(\f.X(\x.k(fx)))) (\k.h(kx))
-    ~~> \k.(\k.g(kf))(\f.(\k.h(kx))(\x.k(fx)))
-    ~~> \k.g((\f.(\k.h(kx))(\x.k(fx)))f)
-    ~~> \k.g((\k.h(kx))(\x.k(fx)))
-    ~~> \k.g(h(\x.k(fx))x)
-    ~~> \k.g(h(k(fx)))
-
-Then
-                          (\ks.k(ks))[]
-    shift = \k.k(k("")) = -------------
-                               ""
-
-Let 2 == \ks.k(ks).
-
-so aSc lifted into the monad is
-
-    []     2[]   []
-    -- ¢ ( --- ¢ --- ) =
-    a      ""    c
-
-First, we need map2 instead of map1.  Second, the type of the shift
-operator will be a string continuation, rather than a function from
-string continuations to string continuations.
-
-(\k.k(k1))(\s.(\k.k(k2))(\r.sr))
-(\k.k(k1))(\s.(\r.sr)((\r.sr)2))
-(\k.k(k1))(\s.(\r.sr)(s2))
-(\k.k(k1))(\s.s(s2))
-(\s.s(s2))((\s.s(s2))1)
-(\s.s(s2))(1(12))
-(1(12))((1(12)2))
-
-
-
-
-
-But here's the interesting part: from the point of view of the shift
-operator, the continuation that it will be fed will be the entire rest
-of the computation.  This includes not only what has come before, but
-what will come after it as well.  That means when the continuation is
-doubled (self-composed), the result duplicates not only the prefix
-`(ab ~~> abab)`, but also the suffix `(d ~~> dd)`.  In some sense, then,
-continuations allow functions to see into the future!
-
-What do you expect will be the result of executing "aScSe" under the
-second perspective?  The answer to this question is not determined by
-the informal specification of the task that we've been using, since
-under the new perspective, we're copying complete (bi-directional)
-contexts rather than just left contexts.
-
-It might be natural to assume that what execution does is choose an S,
-and double its context, temporarily treating all other shift operators
-as dumb letters, then choosing a remaining S to execute.  If that was
-our interpreation of the task, then no string with more than one S
-would ever terminate, since the number S's after each reduction step
-would always be 2(n-1), where n is the number before reduction.
-
-But there is another equally natural way to answer the question.
-Assume the leftmost S is executed first.  What will the value of its
-continuation k be?  It will be a function that maps a string s to the
-result of computing `ascSe`, which will be `ascascee`.  So `k(k "")`
-will be `k(acacee)`, which will result in `a(acacee)ca(acacee)cee`
-(the parentheses are added to show stages in the construction of the
-final result).
-
-So the continuation monad behaves in a way that we expect a
-continuation to behave.  But where did the continuation monad come
-from?  Let's consider some ways of deriving the continuation monad.
+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

@@ -325,80 +240,6 @@ quantificational DPs, as in *John and no dog left*.  Then generalized
quantifier corresponding to the proper name *John* is the quantifier
`\k.kj`.

-At this point, we have a type for our Kliesli arrow and a value for
-our mid.  Given some result type (such as `t` in the Montague application),
-
-    α ==> (α -> ρ) -> ρ
-    ⇧a = \k.ka
-
-It remains only to find a suitable value for bind.  Montague didn't
-provide one, but it's easy to find:
-
-    bind ::    Mα -> (α -> Mβ) -> Mβ
-
-given variables of the following types
-
-    u :: Mα == (α -> ρ) -> ρ
-    f :: α -> Mβ
-    k :: β -> ρ
-    x :: α
-
-We have
-
-    bind u f = \k.u(\x.fxk)
-
-Let's carefully make sure that this types out:
-
-    bind u f = \k.       u      (\x .   f       x     k)
-                                      --------  --
-                                      α -> Mβ   α
-                                     ------------  ------
-                                         Mβ        β -> ρ
-                                  --  --------------------
-                                  α            ρ
-                  -------------  ------------------------
-                  (α -> ρ) -> ρ             α -> ρ
-                  ---------------------------------
-                                ρ
-                -----------------------
-                    (β -> ρ) -> ρ
-
-Yep!
-
-Is there any other way of building a bind operator?  Well, the
-challenge is getting hold of the "a" that is buried inside of `u`.
-In the Reader monad, we could get at the a inside of the box by
-applying the box to an environment.  In the State monad, we could get
-at the a by applying to box to a state and deconstructing the
-resulting pair.  In the continuation case, the only way to do it is to
-apply the boxed a (i.e., u) to a function that takes an a as an
-argument.  That means that f must be invoked inside the scope of the
-functional argument to u.  So we've deduced the structure
-
-    ... u (\x. ... f x ...) ...
-
-At this point, in order to provide u with an argument of the
-appropriate type, the argument must not only take objects of type
-α as an argument, it must return a result of type ρ.  That means that
-we must apply fx to an object of type β -> ρ.  We can hypothesize such
-an object, as long as we eliminate that hypothesis later (by binding
-it), and we have the complete bind operation.
-
-The way in which the value of type α that is needed in order to unlock
-the function f is hidden inside of u is directly analogous to the
-concept of "data hiding" in object-oriented programming.  See Pierce's
-discussion of how to extend system F with existential type
-quantification by encoding the existential using continuations.
-
-So the Kliesli type pretty much determines the bind operation.
-
-## What continuations are doing
-
-Ok, we have a continuation monad.  We derived it from first
-principles, and we have seen that it behaves at least in some respects
-as we expect a continuation monad to behave (in that it allows us to
-give a good implementation of the task).
-
## How continuations can simulate other monads

Because the continuation monad allows the result type ρ to be any
@@ -434,16 +275,3 @@ is return Nothing.

Super cool.

-
-
-
-## Delimited versus undelimited continuations
-
-## Natural language requries delimited continuations
-
-
-
-
-
-