+We saw in the copy-string example ("abSd") and in the same-fringe example that
+local properties of a structure (whether a character is `'S'` or not, which
+integer occurs at some leaf position) can control global properties of
+the computation (whether the preceeding string is copied or not,
+whether the computation halts or proceeds). Local control of
+surrounding context is a reasonable description of in-situ
+quantification.
+
+ (1) John saw everyone yesterday.
+
+This sentence means (roughly)
+
+ forall x . yesterday(saw x) john
+
+That is, the quantifier *everyone* contributes a variable in the
+direct object position, and a universal quantifier that takes scope
+over the whole sentence. If we have a lexical meaning function like
+the following:
+
+ let lex (s:string) k = match s with
+ | "everyone" -> Node (Leaf "forall x", k "x")
+ | "someone" -> Node (Leaf "exists y", k "y")
+ | _ -> k s;;
+
+Then we can crudely approximate quantification as follows:
+
+ # let sentence1 = Node (Leaf "John",
+ Node (Node (Leaf "saw",
+ Leaf "everyone"),
+ Leaf "yesterday"));;
+
+ # tree_monadize lex sentence1 (fun x -> x);;
+ - : string tree =
+ Node
+ (Leaf "forall x",
+ Node (Leaf "John", Node (Node (Leaf "saw", Leaf "x"), Leaf "yesterday")))
+
+In order to see the effects of evaluation order,
+observe what happens when we combine two quantifiers in the same
+sentence:
+
+ # let sentence2 = Node (Leaf "everyone", Node (Leaf "saw", Leaf "someone"));;
+ # tree_monadize lex sentence2 (fun x -> x);;
+ - : string tree =
+ Node
+ (Leaf "forall x",
+ Node (Leaf "exists y", Node (Leaf "x", Node (Leaf "saw", Leaf "y"))))
+
+The universal takes scope over the existential. If, however, we
+replace the usual `tree_monadizer` with `tree_monadizer_rev`, we get
+inverse scope:
+
+ # tree_monadize_rev lex sentence2 (fun x -> x);;
+ - : string tree =
+ Node
+ (Leaf "exists y",
+ Node (Leaf "forall x", Node (Leaf "x", Node (Leaf "saw", Leaf "y"))))
+
+There are many crucially important details about quantification that
+are being simplified here, and the continuation treatment used here is not
+scalable for a number of reasons. Nevertheless, it will serve to give
+an idea of how continuations can provide insight into the behavior of
+quantifiers.
+
+
+The Tree monad
+==============
+
+Of course, by now you may have realized that we are working with a new
+monad, the binary, leaf-labeled Tree monad. Just as mere lists are in fact a monad,
+so are trees. Here is the type constructor, unit, and bind: