From 8e42213815ea8a2e0013aa4039a5d9bc44697425 Mon Sep 17 00:00:00 2001 From: Chris Date: Wed, 13 May 2015 09:28:57 -0400 Subject: [PATCH 1/1] edits --- topics/_week15_continuation_applications.mdwn | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) 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: + + -- 2.11.0