- 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:
-