X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week15_continuation_applications.mdwn;h=328b506ee9b7fc429e634f491b748b0a3455baa8;hp=3bdbd2a14c25a56f3fb1d99f5c90f39db6e35332;hb=8e42213815ea8a2e0013aa4039a5d9bc44697425;hpb=36e5cafb9453eb4c59283903a951b30f69915038

diff --git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
index 3bdbd2a1..328b506e 100644
--- a/topics/_week15_continuation_applications.mdwn
+++ b/topics/_week15_continuation_applications.mdwn
@@ -377,7 +377,7 @@ 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
+## LIFT (mid)
 
 Then in the spirit of monadic thinking, we'll have a way of lifting an
 arbitrary value into the tower system:
@@ -569,7 +569,7 @@ We'll change these arrows into left-leaning and right-leaning versions
 too, according to the following scheme:
 
     γ|δ
-    --- == γ//((α/β) \\\\ δ)
+    --- == γ//((α/β) \\ δ)
     α/β
 
 As we'll see in a minute, each of these for implications (\\, /, \\\\,
@@ -580,3 +580,26 @@ As we'll see in a minute, each of these for implications (\\, /, \\\\,
     \\   argument is surrounded by the functor
     //  argument surrounds the functor
 
+## LOWER (reset)
+
+One more ingredient: one thing that shifty continuation operators
+require is an upper bound, a reset to show the extent of the remainder
+of the computation that the shift operator captures.  In the list
+version of the doubling task, we have
+
+    "a#bdeSfg" ~~> "abdebdefg"   continuation captured: bde
+    "ab#deSfg" ~~> "abdedefg"    continuation captured:  de
+
+In programming languages, resets are encoded in the computation
+explicitly.  In natural language, resets are always invisible.
+We'll deal with this in the natural language setting by allowing
+spontaneous resets, as long as the types match the following recipe:
+
+           g[] α|S
+    LOWER (---:---) == g[p]:α
+            p   S
+
+This will be easiest to explain by presenting our first complete
+example from natural language:
+
+