+Just to be explicit, here are the two versions:
+
+ g[] γ | δ h[] δ | ρ g[h[]] γ | ρ
+ --- : ------- ¢ --- : ----- == ------ : -----
+ f α/β x α fx β
+
+ h[] δ | ρ g[] γ | δ g[h[]] γ | ρ
+ --- : ----- ¢ --- : ------- == ------ : -----
+ x α f β\α fx β
+
+With respect to types, they differ only in replacing α -> β with α/β
+(top version) and with β\α (bottom version). With respect to
+syntactic order, they differ in a parallel way with respect to whether
+the function f is on the left of its argument x (top version) or on
+the right (bottom version).
+
+Logically, separating -> into \\ and / corresponds to rejecting the
+structural rule of exchange.
+
+Note that the \\ and / only govern types at the bottom of the tower.
+That is, we currently still have arrow at the higher-order levels of
+the types, if we undo the tower notation:
+
+ γ|δ
+ --- == ((α/β) -> δ) -> γ
+ α/β
+
+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 (\\, /, \\\\,
+//) will have a syntactic interpretation:
+
+ \ argument is adjacent on the left of the functor
+ / argument is adjacent on the right of the functor
+ \\ 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: