X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week15_continuation_applications.mdwn;h=001f8b19d9b0a6e23fb6bcb38a64823e3cba9e27;hp=cc5c9e2918ea22fa4153e612b0130f1a85aa6b7c;hb=0f8ff4c3540567e649fcabd628c6e4aa208df052;hpb=88b8a69e01f705bf5000ce75cd3f70caea1a929d
diff --git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
index cc5c9e29..001f8b19 100644
--- a/topics/_week15_continuation_applications.mdwn
+++ b/topics/_week15_continuation_applications.mdwn
@@ -109,7 +109,9 @@ Here, QDP is a scope-taking quantificational DP.
Just to emphasize the similarity between QR and shift, we can use QR
to provide insight into the tree task that mystified us earlier.
+
.
@@ -124,9 +126,12 @@ a __|___
S e
-First we QR the lower shift operator
+First we QR the lower shift operator, replacing it with a variable and
+abstracting over that variable.
+
.
@@ -147,7 +152,9 @@ S ___|___
Next, we QR the upper shift operator
+
.
@@ -172,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).
@@ -180,7 +187,9 @@ The relevant value for k is (\x.a(y(d(x e)))). Then k "" is
a(y(d(""(e)))), and k(k "") is a(y(d((a(y(d(""(e)))))(e)))). In tree
form:
+
.
@@ -211,7 +220,9 @@ S ___|____
Repeating the process for the upper shift operator replaces each
occurrence of y with a copy of the whole tree.
+
.
@@ -251,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.
-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:
@@ -261,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)
@@ -287,6 +300,8 @@ reproduce the analyses giving in Barker and Shan in purely QR terms.
Simple quantificational binding using parasitic scope should be easy,
but how reconstruction would work is not so clear.]
+## Introducting the tower notation
+
We'll present tower notation, then comment and motivate several of its
features as we consider various applications. For now, we'll motivate
the tower notation by thinking about box types. In the discussion of
@@ -299,12 +314,12 @@ separating a box into two regions, the payload and the hidden scratch
space:
- _______________ _______________ _______________
- | [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 |
+ |______________| |______________| |______________|
For people who are familiar with Discourse Representation Theory (Kamp
@@ -321,14 +336,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:
+
γ | β
(α -> β) -> γ can be equivalently written -----
α
+
Tower convention for values:
+
g[]
\k.g[k(x)] can be equivalently written ---
x
+
If \k.g[k(x)] has type (α -> β) -> γ, then k has type (α -> β).
@@ -338,15 +357,20 @@ hole in it. For instance, we might have g[x] = \forall x.P[x].
We'll use a simply-typed system with two atomic types, DP (the type of
individuals) and S (the type of truth values).
+## LIFT
+
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:
@@ -359,6 +383,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:
@@ -369,6 +401,8 @@ them. We'll use the ¢ operator from the continuation monad:
Note that the types below the horizontal line combine just like
functional application (i.e, f:(α->β) (x:α) = fx:β).
+## Not quite a monad
+
To demonstrate that this is indeed the continuation monad's ¢
operator:
@@ -382,9 +416,21 @@ operator:
== ------
fx
-Not a monad (Wadler); would be if the types were
+However, these continuations do not form an official monad. The
+reason is that (see Wadler's paper `Composable continuations' for details).
+
Neverthless, obeys the monad laws.
+Oh, one more thing: because natural language allows the functor to be
+on the left or on the right, we replace the type arrow -> with a
+left-leaning version \ and a right-leaning version, as follows:
+
+ α/β β = α
+ β β\α = α
+
+This means we need two versions of ¢ too (see Barker and Shan 2014
+chapter 1 for full details).
+
This is (almost) all we need to get some significant linguistic work
done.