projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
962395b
)
edits
author
Chris
<chris.barker@nyu.edu>
Tue, 12 May 2015 14:03:24 +0000
(10:03 -0400)
committer
Chris
<chris.barker@nyu.edu>
Tue, 12 May 2015 14:03:24 +0000
(10:03 -0400)
topics/_week15_continuation_applications.mdwn
patch
|
blob
|
history
diff --git
a/topics/_week15_continuation_applications.mdwn
b/topics/_week15_continuation_applications.mdwn
index
d13efa7
..
001f8b1
100644
(file)
--- 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.]
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
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
@@
-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).
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:
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:
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:
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:β).
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:
To demonstrate that this is indeed the continuation monad's ¢
operator:
@@
-410,7
+416,9
@@
operator:
== ------
fx
== ------
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
Neverthless, obeys the monad laws.
Oh, one more thing: because natural language allows the functor to be