author Chris Tue, 12 May 2015 13:32:10 +0000 (09:32 -0400) committer Chris Tue, 12 May 2015 13:32:10 +0000 (09:32 -0400)

index b56fcc0..6eeaf8f 100644 (file)
@@ -126,7 +126,8 @@ a  __|___
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)))))))
@@ -178,7 +179,7 @@ S  ___|____

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).
@@ -261,8 +262,8 @@ a  ___|____           |      |
The yield of this tree (the sequence of leaf nodes) is

-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:

@@ -271,7 +272,9 @@ Three lessons:
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)
@@ -310,8 +313,8 @@ space:

<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        |
|______________|             |______________|          |______________|
@@ -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:
+<pre>
γ | β
(α -> β) -> γ can be equivalently written -----
α
+</pre>

Tower convention for values:
+<pre>
g[]
\k.g[k(x)] can be equivalently written ---
x
+</pre>

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:

-                                           []    γ
-    LIFT (x:Î±) = \k.kx : (Î± -> Î²) -> Î³ ==  --- : ---
-                                           x      α
+                                           []   β
+    LIFT (x:Î±) = \k.kx : (Î± -> Î²) -> Î² ==  -- : ---
+                                           x     α

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:
@@ -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.

+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: