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:
too, according to the following scheme:
γ|δ
- --- == γ//((α/β) \\\\ δ)
+ --- == γ//((α/β) \\ δ)
α/β
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:
+
+