author Chris Mon, 30 Mar 2015 01:56:16 +0000 (21:56 -0400) committer Chris Mon, 30 Mar 2015 01:56:16 +0000 (21:56 -0400)

index 56c4eb4..557bd2f 100644 (file)
@@ -169,148 +169,6 @@ map2 +  ⇧1    _____|_____  ⇧4

With these adjustments, the faulty computation now completes smoothly:

With these adjustments, the faulty computation now completes smoothly:

-    1. Reduce head ((map2 +)  -->
-
-%%%
-<pre>
-\tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
-
- ___________
- |         |
-_|__    ___|___
-|  |    |     |
-+  1  __|___  4
-      |    |
-      *  __|___
-         |    |
-        _|__  2
-        |  |
-        /  6
-</pre>
-
-This computation should reduce to 13.  But given a specific reduction
-strategy, we can watch the order in which the computation proceeds.
-Following on the lambda evaluator developed during the previous
-homework, let's adopt the following reduction strategy:
-
-    In order to reduce (head arg), do the following in order:
-    1. Reduce head to h'
-    2. Reduce arg to a'.
-    3. If (h' a') is a redex, reduce it.
-
-There are many details left unspecified here, but this will be enough
-for today.  The order in which the computation unfolds will be
-
-    1. Reduce head (+ 1) to itself
-    2. Reduce arg ((* (/ 6 2)) 3)
-         1. Reduce head (* ((/ 6) 2))
-              1. Reduce head *
-              2. Reduce arg ((/ 6) 2)
-                   1. Reduce head (/ 6) to itself
-                   2. Reduce arg 2 to itself
-                   3. Reduce ((/ 6) 2) to 3
-              3. Reduce (* 3) to itself
-         2. Reduce arg 4 to itself
-         3. Reduce ((* 3) 4) to 12
-     3. Reduce ((+ 1) 12) to 13
-
-This reduction pattern follows the structure of the original
-expression exactly, at each node moving first to the left branch,
-processing the left branch, then moving to the right branch, and
-finally processing the results of the two subcomputation.  (This is
-called depth-first postorder traversal of the tree.)
-
-It will be helpful to see how the types change as we make adjustments.
-
-    type num = int
-    type contents = Num of num   | Op of (num -> num -> num)
-    type tree = Leaf of contents | Branch of tree * tree
-
-Never mind that these types will allow us to construct silly
-arithmetric trees such as `+ *` or `2 3`.  Note that during the
-reduction sequence, the result of reduction was in every case a
-well-formed subtree.  So the process of reduction could be animated by
-replacing subtrees with the result of reduction on that subtree, till
-the entire tree is replaced by a single integer (namely, 13).
-
-Now we replace the number 2 with 0:
-
-<pre>
-\tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
-
- ___________
- |         |
-_|__    ___|___
-|  |    |     |
-+  1  __|___  4
-      |    |
-      *  __|___
-         |    |
-        _|__  0
-        |  |
-        /  6
-</pre>
-
-When we reduce, we get quite a ways into the computation before things
-go south:
-
-    1. Reduce head (+ 1) to itself
-    2. Reduce arg ((* (/ 6 0)) 3)
-         1. Reduce head (* ((/ 6) 0))
-              1. Reduce head *
-              2. Reduce arg ((/ 6) 0)
-                   1. Reduce head (/ 6) to itself
-                   2. Reduce arg 0 to itself
-                   3. Reduce ((/ 6) 0) to ACKKKK
-
-This is where we replace `/` with `safe-div`.  This means changing the
-type of the arithmetic operators from `int -> int -> int` to
-`int -> int -> int option`; and since we now have to anticipate the
-possibility that any argument might involve division by zero inside of
-it, here is the net result for our types:
-
-    type num = int option
-    type contents = Num of num   | Op of (num -> num -> num)
-    type tree = Leaf of contents | Branch of tree * tree
-
-The only difference is that instead of defining our numbers to be
-simple integers, they are now int options; and so Op is an operator
-over int options.
-
-At this point, we bring in the monadic machinery.  In particular, here
-is the ⇧ and the map2 function from the notes on safe division:
-
-    ⇧ (a: 'a) = Just a;;
-
-    map2 (g : 'a -> 'b -> 'c) (u : 'a option) (v : 'b option) =
-      match u with
-      | None -> None
-      | Some x ->
-          (match v with
-          | None -> None
-          | Some y -> Some (g x y));;
-
-Then we lift the entire computation into the monad by applying ⇧ to
-the integers, and by applying `map1` to the operators:
-
-<pre>
-\tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
-
-     ___________________
-     |                 |
-  ___|____         ____|_____
-  |      |         |        |
-map2 +  ⇧1    _____|_____  ⇧4
-              |         |
-            map2 *  ____|____
-                    |       |
-                 ___|____  ⇧0
-                 |      |
-               map2 /  ⇧6
-</pre>
-
-With these adjustments, the faulty computation now completes smoothly:
-
1. Reduce head ((map2 +) ⇧1)
2. Reduce arg (((map2 *) (((map2 /) ⇧6) ⇧2)) ⇧3)
1. Reduce head ((map2 *) (((map2 /) ⇧6) ⇧2))
1. Reduce head ((map2 +) ⇧1)
2. Reduce arg (((map2 *) (((map2 /) ⇧6) ⇧2)) ⇧3)
1. Reduce head ((map2 *) (((map2 /) ⇧6) ⇧2))