-\tree ((((+) (1)) (((*) (((/) (6)) (2))) (4)))) - - ___________ - | | -_|__ ___|___ -| | | | -+ 1 __|___ 4 - | | - * __|___ - | | - _|__ 2 - | | - / 6 -- -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: - -

-\tree ((((+) (1)) (((*) (((/) (6)) (0))) (4)))) - - ___________ - | | -_|__ ___|___ -| | | | -+ 1 __|___ 4 - | | - * __|___ - | | - _|__ 0 - | | - / 6 -- -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: - -

-\tree ((((map2 +) (â§1)) (((map2 *) (((map2 /) (â§6)) (â§0))) (â§4)))) - - ___________________ - | | - ___|____ ____|_____ - | | | | -map2 + â§1 _____|_____ â§4 - | | - map2 * ____|____ - | | - ___|____ â§0 - | | - map2 / â§6 -- -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)) -- 2.11.0