edits

[lambda.git] / topics / _week15_continuation_applications.mdwn

diff --git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
index b56fcc0..6eeaf8f 100644 (file)
--- a/topics/_week15_continuation_applications.mdwn
+++ b/topics/_week15_continuation_applications.mdwn
@@ -126,7 +126,8 @@ a  __|___
          S  e
 </pre>
 
          S  e
 </pre>
 

-First we QR the lower shift operator
+First we QR the lower shift operator, replacing it with a variable and
+abstracting over that variable.

 
 <!--
 \tree (. (S) ((\\x) ((a)((S)((d)((x)(e)))))))
 
 <!--
 \tree (. (S) ((\\x) ((a)((S)((d)((x)(e)))))))


@@ -178,7 +179,7 @@ S  ___|____
 
 We then evaluate, using the same value for the shift operator proposed before:
 
 
 We then evaluate, using the same value for the shift operator proposed before:
 

-    shift = \k.k(k "")
+    S = shift = \k.k(k "")

 
 It will be easiest to begin evaluating this tree with the lower shift
 operator (we get the same result if we start with the upper one).
 
 It will be easiest to begin evaluating this tree with the lower shift
 operator (we get the same result if we start with the upper one).


@@ -261,8 +262,8 @@ a  ___|____           |      |
 The yield of this tree (the sequence of leaf nodes) is
 aadadeedaadadeedee, which is the expected output of the double-shifted tree.
 
 The yield of this tree (the sequence of leaf nodes) is
 aadadeedaadadeedee, which is the expected output of the double-shifted tree.
 

-Exercise: the result is different, by the way, if the QR occurs in a
-different order.
+Exercise: the result is different, by the way, if the QR occurs in the
+opposite order.

 
 Three lessons:
 
 
 Three lessons:
 


@@ -271,7 +272,9 @@ Three lessons:
   dramatic increase in power and complexity.
 
 * Operators that
   dramatic increase in power and complexity.
 
 * Operators that

-  compose multiple copies of a context can be hard to understand.
+  compose multiple copies of a context can be hard to understand
+  (though keep this in mind when we see the continuations-based
+  analysis of coordination, which involves context doubling).

 
 * When considering two-sided, tree-based continuation operators,
   quantifier raising is a good tool for visualizing (defunctionalizing)
 
 * When considering two-sided, tree-based continuation operators,
   quantifier raising is a good tool for visualizing (defunctionalizing)


@@ -310,8 +313,8 @@ space:
 
 <pre>
     _______________               _______________           _______________ 
 
 <pre>
     _______________               _______________           _______________ 

-    | [x->2, y->3] |             | [x->2, y->3] |          | [x->2, y->3] |
-  -------------------          ------------------         ------------------
+    | [x->2, y->3] |             | [x->2, y->3] |          | [x->2, y->3] |
+  -------------------           ------------------        ------------------

     |              |     ¢        |              |    =     |              |
     |    +2        |             |     y        |          |     5        |
     |______________|             |______________|          |______________|
     |              |     ¢        |              |    =     |              |
     |    +2        |             |     y        |          |     5        |
     |______________|             |______________|          |______________|


@@ -331,14 +334,18 @@ We won't keep the outer box, but we will keep the horizontal line
 dividing main effects from side-effects.
 
 Tower convention for types:
 dividing main effects from side-effects.
 
 Tower convention for types:

+<pre>

                                               γ | β
     (α -> β) -> γ can be equivalently written ----- 
                                                 α
                                               γ | β
     (α -> β) -> γ can be equivalently written ----- 
                                                 α

+</pre>

 
 Tower convention for values:
 
 Tower convention for values:

+<pre>

                                            g[] 
     \k.g[k(x)] can be equivalently written ---
                                             x
                                            g[] 
     \k.g[k(x)] can be equivalently written ---
                                             x

+</pre>

 
 If \k.g[k(x)] has type (α -> β) -> γ, then k has type (α -> β).
 
 
 If \k.g[k(x)] has type (α -> β) -> γ, then k has type (α -> β).
 


@@ -351,12 +358,15 @@ individuals) and S (the type of truth values).
 Then in the spirit of monadic thinking, we'll have a way of lifting an
 arbitrary value into the tower system:
 
 Then in the spirit of monadic thinking, we'll have a way of lifting an
 arbitrary value into the tower system:
 

-                                           []    γ|β
-    LIFT (x:α) = \k.kx : (α -> β) -> γ ==  --- : ---
-                                           x      α
+                                           []   β|β
+    LIFT (x:α) = \k.kx : (α -> β) -> β ==  -- : ---
+                                           x     α

 
 Obviously, LIFT is exactly the midentity (the unit) for the continuation monad.
 
 Obviously, LIFT is exactly the midentity (the unit) for the continuation monad.

-The name comes from Partee's 1987 theory of type-shifters for
+Notice that LIFT requires the result type of the continuation argument
+and the result type of the overall expression to match (here, both are β).
+
+The name LIFT comes from Partee's 1987 theory of type-shifters for

 determiner phrases.  Importantly, LIFT applied to an
 individual-denoting expression yields the generalized quantifier
 proposed by Montague as the denotation for proper names:
 determiner phrases.  Importantly, LIFT applied to an
 individual-denoting expression yields the generalized quantifier
 proposed by Montague as the denotation for proper names:


@@ -369,6 +379,14 @@ So if the proper name *John* denotes the individual j, LIFT(j) is the
 generalized quantifier that maps each property k of type DP -> S to true
 just in case kj is true.
 
 generalized quantifier that maps each property k of type DP -> S to true
 just in case kj is true.
 

+Crucially for the discussion here, LIFT does not apply only to DPs, as
+in Montague and Partee, but to any expression whatsoever.  For
+instance, here is LIFT applied to a lexical verb phrase:
+
+                                                   []     S|S 
+    LIFT (left:DP\S) = \k.kx : (DP\S -> S) -> S == ---- : ---
+                                                   left   DP
+

 Once we have expressions of type (α -> β) -> γ, we'll need to combine
 them.  We'll use the ¢ operator from the continuation monad:
 
 Once we have expressions of type (α -> β) -> γ, we'll need to combine
 them.  We'll use the ¢ operator from the continuation monad: