author Jim Pryor Wed, 1 Dec 2010 05:37:04 +0000 (00:37 -0500) committer Jim Pryor Wed, 1 Dec 2010 05:37:04 +0000 (00:37 -0500)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>

index 170ae5d..ff7e392 100644 (file)
@@ -30,9 +30,9 @@ This deceptively simple task gives rise to some mind-bending complexity.
Note that it matters which 'S' you target first (the position of the *
indicates the targeted 'S'):

-           t "aSbS"
+           t "aSbS"
*
-       ~~> t "aabS"
+       ~~> t "aabS"
*
~~> "aabaab"

@@ -40,7 +40,7 @@ versus

t "aSbS"
*
-       ~~> t "aSbaSb"
+       ~~> t "aSbaSb"
*
~~> t "aabaSb"
*
@@ -74,10 +74,10 @@ entire list has been unzipped (and so the zipped half of the zipper is empty).

type 'a list_zipper = ('a list) * ('a list);;

-       let rec tz (z : char list_zipper) =
+       let rec tz (z : char list_zipper) =
match z with
| (unzipped, []) -> List.rev(unzipped) (* Done! *)
-           | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
+           | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
| (unzipped, target::zipped) -> tz (target::unzipped, zipped);; (* Pull zipper *)

# tz ([], ['a'; 'b'; 'S'; 'd']);;
@@ -96,44 +96,40 @@ arguments to `tz` each time it is (recurcively) called.  Note that the
lines with left-facing arrows (`<--`) show (recursive) calls to `tz`,
giving the value of its argument (a zipper), and the lines with
right-facing arrows (`-->`) show the output of each recursive call, a
-simple list.
-
-<pre>
-# #trace tz;;
-t1 is now traced.
-# tz ([], ['a'; 'b'; 'S'; 'd']);;
-tz <-- ([], ['a'; 'b'; 'S'; 'd'])
-tz <-- (['a'], ['b'; 'S'; 'd'])         (* Pull zipper *)
-tz <-- (['b'; 'a'], ['S'; 'd'])         (* Pull zipper *)
-tz <-- (['b'; 'a'; 'b'; 'a'], ['d'])    (* Special step *)
-tz <-- (['d'; 'b'; 'a'; 'b'; 'a'], [])  (* Pull zipper *)
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']        (* Output reversed *)
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-- : char list = ['a'; 'b'; 'a'; 'b'; 'd']
-</pre>
+simple list.
+
+       # #trace tz;;
+       t1 is now traced.
+       # tz ([], ['a'; 'b'; 'S'; 'd']);;
+       tz <-- ([], ['a'; 'b'; 'S'; 'd'])
+       tz <-- (['a'], ['b'; 'S'; 'd'])         (* Pull zipper *)
+       tz <-- (['b'; 'a'], ['S'; 'd'])         (* Pull zipper *)
+       tz <-- (['b'; 'a'; 'b'; 'a'], ['d'])    (* Special step *)
+       tz <-- (['d'; 'b'; 'a'; 'b'; 'a'], [])  (* Pull zipper *)
+       tz --> ['a'; 'b'; 'a'; 'b'; 'd']        (* Output reversed *)
+       tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+       tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+       tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+       tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+       - : char list = ['a'; 'b'; 'a'; 'b'; 'd']

The nice thing about computations involving lists is that it's so easy
to visualize them as a data structure.  Eventually, we want to get to
a place where we can talk about more abstract computations.  In order
to get there, we'll first do the exact same thing we just did with
-concrete zipper using procedures.
-
-Think of a list as a procedural recipe: `['a'; 'b'; 'S'; 'd']`
-is the result of the computation `'a'::('b'::('S'::('d'::[])))` (or, in our old
-style, `make_list 'a' (make_list 'b' (make_list 'S' (make_list 'd' empty)))`).
-The recipe for constructing the list goes like this:
-
-<pre>
-(0)  Start with the empty list []
-(1)  make a new list whose first element is 'd' and whose tail is the list constructed in step (0)
-(2)  make a new list whose first element is 'S' and whose tail is the list constructed in step (1)
------------------------------------------
-(3)  make a new list whose first element is 'b' and whose tail is the list constructed in step (2)
-(4)  make a new list whose first element is 'a' and whose tail is the list constructed in step (3)
-</pre>
+concrete zipper using procedures.
+
+Think of a list as a procedural recipe: `['a'; 'b'; 'S'; 'd']` is the result of
+the computation `'a'::('b'::('S'::('d'::[])))` (or, in our old style,
+`make_list 'a' (make_list 'b' (make_list 'S' (make_list 'd' empty)))`). The
+recipe for constructing the list goes like this:
+
+>      (0)  Start with the empty list []
+>      (1)  make a new list whose first element is 'd' and whose tail is the list constructed in step (0)
+>      (2)  make a new list whose first element is 'S' and whose tail is the list constructed in step (1)
+>      -----------------------------------------
+>      (3)  make a new list whose first element is 'b' and whose tail is the list constructed in step (2)
+>      (4)  make a new list whose first element is 'a' and whose tail is the list constructed in step (3)

What is the type of each of these steps?  Well, it will be a function
from the result of the previous step (a list) to a new list: it will
@@ -153,10 +149,10 @@ The structure and the behavior will follow that of `tz` above, with
some small but interesting differences.  We've included the orginal
`tz` to facilitate detailed comparison:

-       let rec tz (z : char list_zipper) =
+       let rec tz (z : char list_zipper) =
match z with
| (unzipped, []) -> List.rev(unzipped) (* Done! *)
-           | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
+           | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
| (unzipped, target::zipped) -> tz (target::unzipped, zipped);; (* Pull zipper *)

let rec tc (l: char list) (c: (char list) -> (char list)) =
@@ -187,7 +183,7 @@ point of the excercise, and it should be emphasized.  For instance,
you can see this difference in the fact that in `tz`, we have to glue
together the two instances of `unzipped` with an explicit (and
relatively inefficient) `List.append`.
-In the `tc` version of the task, we simply compose `c` with itself:
+In the `tc` version of the task, we simply compose `c` with itself:
`c o c = fun x -> c (c x)`.

Why use the identity function as the initial continuation?  Well, if
@@ -225,4 +221,3 @@ The following section explores this connection.  We'll return to the
list task after talking about generalized quantifiers below.

-