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=ffe10ba68d3cd2c39c65f0d8ec7147103dc7c68a;hb=0f8ff4c3540567e649fcabd628c6e4aa208df052;hpb=f33813998bb13f6d227c6ba635bb29a5b46d065b

diff --git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
index ffe10ba6..001f8b19 100644
--- a/topics/_week15_continuation_applications.mdwn
+++ b/topics/_week15_continuation_applications.mdwn
@@ -300,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
@@ -312,12 +314,12 @@ separating a box into two regions, the payload and the hidden scratch
 space:
 
 <pre>
-    _______________               _______________           _______________ 
+    _______________               _______________            _______________ 
     | [x->2, y->3] |	          | [x->2, y->3] |          | [x->2, y->3] |
   ------------------- 	         ------------------        ------------------
     |              |     ¢        |              |    =     |              |
-    |    +2        |	          |     y        |	    |     5        |
-    |______________|	          |______________|	    |______________|
+    |    +2        |	          |     y        |          |     5        |
+    |______________|	          |______________|          |______________|
 </pre>
 
 For people who are familiar with Discourse Representation Theory (Kamp
@@ -355,6 +357,8 @@ 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:
 
@@ -383,9 +387,9 @@ 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
+                                                        []    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:
@@ -397,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:
 
@@ -410,7 +416,9 @@ 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