X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week7.mdwn;h=bc8dc8eff4a28cd9cd62865c7becf04ec6ca9e23;hp=a4538ee3e3e5572c504adf9495bc9e594224c8e7;hb=7b960aed1552ab5ee4b17428ae4e293decaee2b7;hpb=63b3d068ec7da4f7ad620d2e8ff674495b642024

diff --git a/week7.mdwn b/week7.mdwn
index a4538ee3..bc8dc8ef 100644
--- a/week7.mdwn
+++ b/week7.mdwn
@@ -164,7 +164,7 @@ arguments of a monoid operation) the two arguments of the bind are of
 different types.  But if we generalize bind so that both arguments are
 of type `'a -> M 'a`, then we get plain identity laws and
 associativity laws, and the monad laws are exactly like the monoid
-laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>).
+laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>, near the bottom).
 
 
 Monad outlook
@@ -191,12 +191,15 @@ intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
 though without explicitly using monads.
 
 All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
-To run it, download the file, start Ocaml, and say `# #use
-"intensionality-monad.ml";;`. 
+To run it, download the file, start Ocaml, and say 
+
+    # #use "intensionality-monad.ml";;
+
+Note the extra `#` attached to the directive `use`.
 
 Here's the idea: since people can have different attitudes towards
 different propositions that happen to have the same truth value, we
-can't have sentences denoting simple truth values.  Then if John
+can't have sentences denoting simple truth values.  If we did, then if John
 believed that the earth was round, it would force him to believe
 Fermat's last theorem holds, since both propositions are equally true.
 The traditional solution is to allow sentences to denote a function
@@ -217,16 +220,16 @@ Vs        s->t->e->t              s->(s->t)->(s->e)->t    thought
 </pre>
 
 This system is modeled on the way Montague arranged his grammar.
-(There are significant simplifications: for instance, determiner
+There are significant simplifications: for instance, determiner
 phrases are thought of as corresponding to individuals rather than to
-generalized quantifiers.)  If you're curious about the initial `s`'s
+generalized quantifiers.  If you're curious about the initial `s`'s
 in the extensional types, they're there because the behavior of these
 expressions depends on which world they're evaluated at.  If you are
 in a situation in which you can hold the evaluation world constant,
-you can further simplify the extensional types.  (Usually, the
+you can further simplify the extensional types.  Usually, the
 dependence of the extension of an expression on the evaluation world
 is hidden in a superscript, or built into the lexical interpretation
-function.)
+function.
 
 The main difference between the intensional types and the extensional
 types is that in the intensional types, the arguments are functions
@@ -240,8 +243,9 @@ types.  Wouldn't it be nice to keep the complicated types to just
 those attitude verbs that need to worry about intensions, and keep the
 rest of the grammar as extensional as possible?  This desire is
 parallel to our earlier desire to limit the concern about division by
-zero to the division function, and let the other functions ignore
-division-by-zero problems as much as possible.
+zero to the division function, and let the other functions, like
+addition or multiplication, ignore division-by-zero problems as much
+as possible.
 
 So here's what we do: