The goal of this lecture note is to explore the two patterns of structural recursion for lists: one, recursive, and the other, tail recursive and with an accumulator.
Let us revisit the template for any structurally recursive function over lists. It follows the inductive structure of lists – base case and induction step:
let ... vs_given =
let rec traverse vs =
match vs with
| [] ->
...
| v :: vs' ->
let ih = traverse vs'
in ...
in traverse vs_given;;
Let us functionally abstract what to do in the base case and what to do in the induction step. The result is what is called the fold-right function for lists (traditionally called just fold_right in practice):
let list_fold_right nil_case cons_case vs_given =
(* list_fold_right : 'a -> ('b -> 'a -> 'a) -> 'b list -> 'a *)
let rec traverse vs =
(* traverse : 'b list -> 'a *)
match vs with
| [] ->
nil_case
| v :: vs' ->
let ih = traverse vs'
in cons_case v ih
in traverse vs_given;;
Given a nil case nil_specific, a cons case cons_specific, and, e.g., a list [v0; v1; v2; v3], i.e., the result of evaluating:
List.cons v0 (List.cons v1 (List.cons v2 (List.cons v3 [])))
list_fold_right essentially yields the result of evaluating:
cons_specific v0 (cons_specific v1 (cons_specific v2 (cons_specific v3 nil_specific)))
In words, given a list vs of length n and represented as vs, evaluating list_fold_right nil_specific cons_specific vs recursively gives rise to n nested applications of cons_specific that mimic the n nested occurrences of List.cons that constructed vs.
Here is how we had defined the length function:
let length vs_given =
let rec measure vs =
match vs with
| [] ->
0
| v :: vs' ->
let ih = measure vs'
in succ ih
in measure vs_given;;
(As usual, the induction hypothesis is implemented by the recursive call.)
By instantiating nil_case to be 0 and cons_case to be (fun v ih -> succ ih), we make list_fold_right emulate the computation of the length function:
let length_gen vs =
list_fold_right
0
(fun v ih ->
succ ih)
vs;;
This generic implementation passes the corresponding unit tests.
Here is how we had defined an unparsing function for polymorphic lists in long hand:
let show_list_in_long_hand show_v vs_given =
(* show_list_in_long_hand : ('a -> string) -> 'a list -> string *)
let rec visit vs =
match vs with
| [] ->
"[]"
| v :: vs' ->
let ih = visit vs'
in (show_v v) ^ " :: " ^ ih
in visit vs_given;;
By instantiating nil_case to be "[]" and cons_case to be (fun v ih -> (show_v v) ^ " :: " ^ ih), we make list_fold_right emulate the computation of the unparsing function for lists in long hand:
let show_list_in_long_hand_gen show_v vs_given =
(* show_list_in_long_hand_gen : ('a -> string) -> 'a list -> string *)
list_fold_right
"[]"
(fun v ih ->
(show_v v) ^ " :: " ^ ih)
vs_given;;
This generic implementation passes the corresponding unit tests.
Here is how we had defined an unparsing function for polymorphic lists in short hand:
let show_list_in_short_hand show_v vs =
(* show_list_in_short_hand : ('a -> string) -> 'a list -> string *)
"[" ^ match vs with
| [] ->
"]"
| v :: vs' ->
(show_v v) ^ (let rec show_list_aux vs =
(* show_list_aux : 'a list -> string *)
match vs with
| [] ->
"]"
| v :: vs' ->
let ih = show_list_aux vs'
in "; " ^ (show_v v) ^ ih
in show_list_aux vs');;
By instantiating nil_case to be "]" and cons_case to be (fun v ih -> "; " ^ (show_v v) ^ ih), we make list_fold_right emulate the computation of the unparsing function for lists in short hand:
let show_list_in_long_hand_gen show_v vs =
(* show_list_in_short_hand : ('a -> string) -> 'a list -> string *)
"[" ^ match vs with
| [] ->
"]"
| v :: vs' ->
(show_v v) ^ (list_fold_right "]"
(fun v ih ->
"; " ^ (show_v v) ^ ih)
vs');;
This generic implementation passes the corresponding unit tests.
Here is how we had defined a function that duplicates the elements of any given list:
let stutter2 vs_given =
(* stutter2 : 'a list -> 'a list *)
let rec visit vs =
(* visit : 'a list -> 'a list *)
match vs with
| [] ->
[]
| v :: vs' ->
let ih = visit vs'
in v :: v :: ih
in visit vs_given;;
By instantiating nil_case to be [] and cons_case to be (fun v ih -> v :: v :: ih), we make list_fold_right emulate the computation of the stutter2 function:
let stutter2_gen vs_given =
list_fold_right
[]
(fun v ih ->
v :: v :: ih)
vs_given;;
This generic implementation passes the corresponding unit tests.
Here is how we had defined a function to concatenate lists:
let append xs_given ys_given =
let rec visit xs =
match xs with
| [] ->
ys_given
| x :: xs' ->
let ih = visit xs'
in x :: ih
in visit xs_given;;
Given two lists xs_given and ys_given, by instantiating nil_case to be ys_given and cons_case to be (fun x ih -> x :: ih), we make list_fold_right emulate the computation of the append function:
let append_gen xs_given ys_given =
list_fold_right
ys_given
(fun x ih ->
x :: ih)
xs_given;;
This generic implementation passes the corresponding unit tests.
Here is how we had defined a function to test whether an element occurs in a list:
let member e es_given =
let rec visit es =
match es with
| [] ->
false
| e' :: es' ->
let ih = visit es'
in if e = e'
then true
else ih
in visit es_given;;
Given an element e and a list es_given, by instantiating nil_case to be false and cons_case to be (fun e' ih -> if e = e' then true else ih), we make list_fold_right emulate the computation of the member function:
let member_gen e es_given =
list_fold_right
false
(fun e' ih ->
if e = e'
then true
else ih)
es_given;;
This generic implementation passes the corresponding unit tests.
Which function does list_fold_right emulate when nil_case is [] and cons_case is (fun x ih -> x :: ih), i.e., List.cons?
In other words, you are asked to characterize the following OCaml function:
let the_following_OCaml_function xs =
list_fold_right [] (fun x ih -> x :: ih) xs;;
Subsidiary question – in reference to Exercise 01, characterize the following alternative OCaml function:
let the_following_alternative_OCaml_function xs =
list_fold_right [] (fun x ih -> List.append ih [x]) xs;;
As an unashamed excuse for writing structurally recursive functions over lists using list_fold_right, let us revisit the representation of sets as the list of their elements (without repetition).
Revisit Exercise 12 in the lecture note about representing sets as lists, and express your set_union function using list_fold_right. Verify that it passes the unit tests.
Willy nilly, one defines set union by induction on its first argument:
let set_union e1s e2s =
let rec visit e1s =
match e1s with
| [] ->
e2s
| e1 :: e1s' ->
let ih = visit e1s'
in if belongs_to e1 e2s
then ih
else e1 :: ih
in visit e1s;;
By instantiating nil_case to be e2s and cons_case to be (fun e1 ih -> if belongs_to e1 e2s then ih else e1 :: ih), we make list_fold_right emulate the computation of the set_union function:
let set_union_gen e1s e2s =
list_fold_right
e2s
(fun e ih ->
if belongs_to e e2s
then ih
else e :: ih)
e1s;;
This generic implementation passes the corresponding unit tests.
Revisit Exercise 14 in the lecture note about representing sets as lists, and express your set_intersection function using list_fold_right. Verify that it passes the unit tests.
Revisit Exercise 17 in the lecture note about representing sets as lists, and express your set_minus function using list_fold_right. Verify that it passes the unit tests.
Revisit Exercise 20 in the lecture note about representing sets as lists, and express your set_minus_symmetric function using list_fold_right. Verify that it passes the unit tests.
Here is how we had defined a function that computes the Cartesian product of two sets represented as the list of their elements:
let cartesian_product_2 vs_given ws_given =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in let rec traverse_2 ws =
match ws with
| [] ->
ih_outer
| w :: ws' ->
let ih_inner = traverse_2 ws'
in (v, w) :: ih_inner
in traverse_2 ws_given
in traverse_1 vs_given;;
We can express traverse_2 using list_fold_right by instantiating nil_case to be ih_outer and cons_case to be (fun w ih_inner -> (v, w) :: ih_inner):
let cartesian_product_2_gen' vs_given ws_given =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in list_fold_right
ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_given
in traverse_1 vs_given;;
This alternative implementation passes the corresponding unit tests.
We can express traverse_1 using list_fold_right by instantiating nil_case to be [] and cons_case to be (fun v ih_outer -> list_fold_right ih_outer (fun w ih_inner -> (v, w) :: ih_inner) ws_given):
let cartesian_product_2_gen vs_given ws_given =
list_fold_right
[]
(fun v ih_outer ->
list_fold_right
ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_given)
vs_given;;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined a function that computes the Cartesian product of three sets represented as the list of their elements:
let cartesian_product_3 vs_given ws_given xs_given =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in let rec traverse_2 ws =
match ws with
| [] ->
ih_outer
| w :: ws' ->
let ih_median = traverse_2 ws'
in let rec traverse_3 xs =
match xs with
| [] ->
ih_median
| x :: xs' ->
let ih_inner = traverse_3 xs'
in (v, w, x) :: ih_inner
in traverse_3 xs_given
in traverse_2 ws_given
in traverse_1 vs_given;;
We can express traverse_3 using list_fold_right by instantiating nil_case to be ih_median and cons_case to be (fun x ih_inner -> (v, w, x) :: ih_inner):
let cartesian_product_3_gen'' vs_given ws_given xs_given =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in let rec traverse_2 ws =
match ws with
| [] ->
ih_outer
| w :: ws' ->
let ih_median = traverse_2 ws'
in list_fold_right
ih_median
(fun x ih_inner ->
(v, w, x) :: ih_inner)
xs_given
in traverse_2 ws_given
in traverse_1 vs_given;;
This generic implementation passes the corresponding unit tests.
We can express traverse_2 using list_fold_right by instantiating nil_case to be ih_outer and cons_case to be (fun w ih_inner -> list_fold_right ih_median (fun x ih_inner -> (v, w, x) :: ih_inner) xs_given):
let cartesian_product_3_gen' vs_given ws_given xs_given =
let rec traverse_1 vs =
match vs with
| [] ->
[]
| v :: vs' ->
let ih_outer = traverse_1 vs'
in list_fold_right
ih_outer
(fun w ih_median ->
list_fold_right
ih_median
(fun x ih_inner ->
(v, w, x) :: ih_inner)
xs_given)
ws_given
in traverse_1 vs_given;;
This generic implementation passes the corresponding unit tests.
We can express traverse_1 using list_fold_right by instantiating nil_case to be [] and cons_case to be (fun v ih_outer -> list_fold_right ih_outer (fun w ih_inner -> list_fold_right ih_median (fun x ih_inner -> (v, w, x) :: ih_inner) xs_given) ws_given):
let cartesian_product_3_gen vs_given ws_given xs_given =
list_fold_right
[]
(fun v ih_outer ->
list_fold_right
ih_outer
(fun w ih_median ->
list_fold_right
ih_median
(fun x ih_inner ->
(v, w, x) :: ih_inner)
xs_given)
ws_given)
vs_given;;
This generic implementation passes the corresponding unit tests.
Revisit Exercise 23 in the lecture notes about the Cartesian product and express your cartesian_product_4 function using list_fold_right. Verify that it passes the unit tests.
Let us revisit the template for any structurally recursive function over lists that uses an accumulator. It follows the inductive structure of lists – base case and induction step:
let ... vs_given =
let rec traverse vs a =
match vs with
| [] ->
a
| v :: vs' ->
traverse vs' ...
in traverse vs_given ...;;
Let us functionally abstract what to do in the base case and what to do in the induction step. The result is what is called the fold-left function for lists (traditionally called just fold_left in practice):
let list_fold_left nil_case cons_case vs_given =
(* list_fold_left : 'a -> ('b -> 'a -> 'a) -> 'b list -> 'a *)
let rec traverse vs a =
(* traverse : 'b list -> 'a -> 'a *)
match vs with
| [] ->
a
| v :: vs' ->
traverse vs' (cons_case v a)
in traverse vs_given nil_case;;
Given a nil case nil_specific, a cons case cons_specific, and, e.g., a list [v0; v1; v2; v3], i.e., the result of evaluating:
List.cons v0 (List.cons v1 (List.cons v2 (List.cons v3 [])))
list_fold_left essentially yields the result of evaluating:
cons_specific v3 (cons_specific v2 (cons_specific v1 (cons_specific v0 nil_specific)))
In words, given a list vs of length n and represented as vs, evaluating list_fold_left nil_specific cons_specific vs tail-recursively gives rise to n nested applications of cons_specific that mirror the n nested occurrences of List.cons that constructed vs.
Halcyon: Is this where we are supposed to heed the reverse order of accumulation?The practical OCaml programmer: Yes. Check out Exercise 18.
Here is how we had defined the length function using an accumulator:
let length_acc vs_given =
let rec measure vs a =
match vs with
| [] ->
a
| v :: vs' ->
measure vs' (1 + a)
in measure vs_given 0;;
By instantiating nil_case to be 0 and cons_case to be (fun v a -> succ a), we make list_fold_left emulate the computation of the length_acc function:
let length_acc_gen vs =
list_fold_left
0
(fun v a ->
succ a)
vs;;
This generic implementation passes the corresponding unit tests.
Given a list xs, what happens if we instantiate nil_case to be [] and cons_case to be (fun x a -> x :: a), i.e., List.cons? Which function does list_fold_left emulate then?
In other words, you are asked to characterize the following other OCaml function:
let the_following_other_OCaml_function xs =
list_fold_left [] (fun x a -> x :: a) xs;;
Subsidiary question – characterize the following other alternative OCaml function:
let the_following_other_alternative_OCaml_function xs =
list_fold_left [] (fun x a -> List.append a [x]) xs;;
As an unashamed excuse for writing structurally recursive functions over lists that use an accumulator using list_fold_left, let us re3visit the representation of sets as the list of their elements (without repetition).
Revisit Exercise 07 in the lecture note about programming with lists using accumulators and express your set_union_acc function using list_fold_left.
Verify that it passes the unit tests.
We had defined set union by induction on its first argument:
let set_union_acc e1s_given e2s_given =
let rec visit e1s a =
match e1s with
| [] ->
a
| e1 :: e1s' ->
visit e1s' (if belongs_to e1 e2s_given
then a
else e1 :: a)
in visit e1s_given e2s_given;;
By instantiating nil_case to be e2s_given and cons_case to be (fun e1 a -> if belongs_to e1 e2s_given then a else e1 :: a), we make list_fold_left emulate the computation of the set_union_acc function:
let set_union_acc_gen e1s_given e2s_given =
list_fold_left
e2s_given
(fun e1 a ->
if belongs_to e1 e2s_given
then a
else e1 :: a)
e1s_given;;
This generic implementation passes the corresponding unit tests.
Revisit Exercise 08 in the lecture note about programming with lists using accumulators and express your set_intersection_acc function using list_fold_left.
Verify that it passes the unit tests.
Revisit Exercise 09 in the lecture note about programming with lists using accumulators and express your set_minus_acc function using list_fold_left.
Verify that it passes the unit tests.
Revisit Exercise 09 in the lecture note about programming with lists using accumulators and express your symmetric_set_minus_acc function using list_fold_left.
Verify that it passes the unit tests.
Since list_map is structurally recursive, it can be defined using list_fold_right:
let list_map_gen f ns =
list_fold_right [] (fun n ih -> f n :: ih) ns;;
To wit:
# list_map_gen succ [1; 2; 3];;
- : int list = [2; 3; 4]
#
Not so, though, for list_andmap and list_ormap, since they critically rely on OCaml’s short-circuit evaluation for Boolean operations:
# let list_andmap_not p vs = list_fold_right true (fun v ih -> p v && ih) vs;;
val list_andmap_not : ('a -> bool) -> 'a list -> bool = <fun>
# list_andmap_not (fun n -> if n = 0 then false else 1/0 = 0) [0; 1; 2; 3];;
Exception: Division_by_zero.
#
Anton: I feel exhausted.
Alfrothul: Still.
Anton: Still, what.
Alfrothul: Doesn’t it look like list_fold_right and list_fold_left are just one list reversal away from another?
Anton: You mean that for any n, c, and vs of the right types, evaluating list_fold_right n c vs and list_fold_left n c (List.rev vs) yield the same result?
Alfrothul: What I actually was thinking of was that evaluating list_fold_right n c vs and List.rev (list_fold_left n c vs) yield the same result, but otherwise yes.
Dana (perspicacious): Assuming the result to be a list.
Pablito: Actually, list_fold_right n c (List.rev vs) and list_fold_left n c vs would fit the bill too.
Dana: Or List.rev (list_fold_right n c vs) and list_fold_left n c vs for that matter, if the result is a list, but how about we call it a day.
Halcyon: You are all welcome to have a seat.
Anton (hastily): And that means you too, Mimer.
Dana (amused): Too late.
In the light of this aftermath, it doesn’t really matter whether to use list_fold_left or list_fold_right to compute, e.g., set union with an accumulator (as in Exercise 19) or without (as in Exercise 13), since the order of elements doesn’t matter in a list that represents a set.
However, it does matter when expressing the functions computing the Cartesian products, because using list_fold_left instead of list_fold_right makes the unit tests fail:
# let cartesian_product_2_gen' vs_given ws_given =
list_fold_left
[]
(fun v ih_outer ->
list_fold_left
ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_given)
vs_given;;
val cartesian_product_2_gen' : 'a list -> 'b list -> ('a * 'b) list = <fun>
# let () = assert (test_cartesian_product_2 cartesian_product_2_gen');;
Exception: Assert_failure ("//toplevel//", 638, 9).
#
Why is that? What needs to be fixed?
This exercise is due to Christopher Strachey.
Implement an OCaml function that generalizes cartesian_product_2 and cartesian_product_3 in that when applied to a list of sets, it returns their Cartesian product (as a list of lists instead of as a list of tuples). Here is a sketch for this generalization that reuses cartesian_product_2 and cartesian_product_3 (and that posits plausible implementations of the Cartesian product of one set and of the Cartesian product of zero sets):
let cartesian_product_star xss =
(* cartesian_product_star : 'a list list -> 'a list list *)
match xss with
| [] ->
[[]]
| x1s :: [] ->
List.map (fun x1 -> [x1]) x1s
| x1s :: x2s :: [] ->
List.map (fun (x1, x2) -> [x1; x2]) (cartesian_product_2 x1s x2s)
| x1s :: x2s :: x3s :: [] ->
List.map (fun (x1, x2, x3) -> [x1; x2; x3]) (cartesian_product_3 x1s x2s x3s)
| _ ->
let () = assert false
in [];;
In more words:
So by extension,
The sketch above is defined for lists of up to 3 lists.
You are asked to write a function that will recursively traverse the given list of n lists and construct their Cartesian product, resulting in a list of lists of length n.
As usual, it is a good idea to start by writing a unit-test function for cartesian_product_star. As suggested by the sketch, this unit-test function could reuse the existing unit-test functions. For example, whereas the unit-test function for cartesian_product_3 read:
let test_cartesian_product_3 candidate =
let b0 = (candidate [] [] [] =
[])
and b1 = (candidate [1] [] [] =
[])
and b2 = (candidate [] [10] [] =
[])
and b3 = (candidate [] [10] [100] =
[])
and b4 = (candidate [1] [10] [100] =
[(1, 10, 100)])
and b5 = (candidate [1; 2] [10] [100] =
[(1, 10, 100); (2, 10, 100)])
and b6 = (candidate [1; 2] [10; 20] [100] =
[(1, 10, 100); (1, 20, 100);
(2, 10, 100); (2, 20, 100)])
and b7 = (candidate [1; 2; 3] [10; 20] [100] =
[(1, 10, 100); (1, 20, 100);
(2, 10, 100); (2, 20, 100);
(3, 10, 100); (3, 20, 100)])
and b8 = (candidate [1; 2; 3] [10; 20] [100; 200] =
[(1, 10, 100); (1, 10, 200);
(1, 20, 100); (1, 20, 200);
(2, 10, 100); (2, 10, 200);
(2, 20, 100); (2, 20, 200);
(3, 10, 100); (3, 10, 200);
(3, 20, 100); (3, 20, 200)])
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8 (* etc. *);;
a unit-test function for cartesian_product_star could read:
let test_cartesian_product_star_3 candidate =
let b0 = (candidate [[]; []; []] =
[])
and b1 = (candidate [[1]; []; []] =
[])
and b2 = (candidate [[]; [10]; []] =
[])
and b3 = (candidate [[]; [10]; [100]] =
[])
and b4 = (candidate [[1]; [10]; [100]] =
[[1; 10; 100]])
and b5 = (candidate [[1; 2]; [10]; [100]] =
[[1; 10; 100]; [2; 10; 100]])
and b6 = (candidate [[1; 2]; [10; 20]; [100]] =
[[1; 10; 100]; [1; 20; 100];
[2; 10; 100]; [2; 20; 100]])
and b7 = (candidate [[1; 2; 3]; [10; 20]; [100]] =
[[1; 10; 100]; [1; 20; 100];
[2; 10; 100]; [2; 20; 100];
[3; 10; 100]; [3; 20; 100]])
and b8 = (candidate [[1; 2; 3]; [10; 20]; [100; 200]] =
[[1; 10; 100]; [1; 10; 200];
[1; 20; 100]; [1; 20; 200];
[2; 10; 100]; [2; 10; 200];
[2; 20; 100]; [2; 20; 200];
[3; 10; 100]; [3; 10; 200];
[3; 20; 100]; [3; 20; 200]])
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7 && b8 (* etc. *);;
where the expected result is not a list of triples but a list of lists of length 3. The sketch passes these unit tests:
# test_cartesian_product_star_3 cartesian_product_star;;
- : bool = true
#
Pablito: Remember the implementation of powerset_v1?
Anton: The listless one? Yes:
let append_map f vs rest =
let rec visit vs =
match vs with
| [] ->
rest
| v :: vs' ->
f v :: visit vs'
in visit vs;;
let powerset_v1 vs_given =
let rec visit vs =
match vs with
| [] ->
[[]]
| v :: vs' ->
let ih = visit vs'
in append_map (fun ws -> v :: ws) ih ih
in visit vs_given;;
Alfrothul: You tested it:
# test_powerset_int powerset_v1;;
- : bool = true
#
Pablito: I did. But this implementation, is it structurally recursive?
Anton: Well, yes – its recursive calls follow the structure of its input data. Why do you ask?
Pablito: The induction hypothesis is used twice.
Alfrothul: And so it is. But we could still express it using list_fold_right.
Dana: Yay, more generic programming.
Pablito: May I give it a shot?
Alfrothul: By all means.
Pablito: Lemmesee:
let powerset_v2 vs_given =
list_fold_right
[[]]
(fun v ih ->
append_map (fun ws -> v :: ws) ih ih)
vs_given;;
Anton (courteously): Testing, testing:
# test_powerset_int powerset_v2;;
- : bool = true
#
Alfrothul: Wait a minute. The definition of append_map' is structurally recursive too.
Anton: True. Look:
let append_map' f vs rest =
list_fold_right
rest
(fun v ih ->
f v :: ih)
vs;;
Pablito: Just a sec:
# test_append_map_int append_map';;
- : bool = true
#
Alfrothul: How about we unfold the call to append_map' in the definition of powerset_v2?
Anton (reflexively): Unfold the call to append_map' in the definition of powerset_v2.
Alfrothul: Yes, look:
let powerset_v7 vs_given =
list_fold_right
[[]]
(fun v vss ->
list_fold_right
vss
(fun vs vss' ->
(v :: vs) :: vss')
vss)
vs_given;;
Anton: Harrumph. You, my friend, have been skipping a few derivation steps.
Alfrothul (virtuously): But they are spelled out in the accompanying resource file.
Pablito (with uncertainty): Testing, testing:
# test_powerset_int powerset_v7;;
- : bool = true
#
Pablito (to himself): Wow.
Mimer: According to Mike Gordon, this definition was discovered by Dave du Feu, back in the days.
Dana (wondering): When a list represents a set, the order of its elements does not matter, right?
Anton: Right.
Dana: So we could use list_fold_left instead of list_fold_right, couldn’t we?
Alfrothul: That is going to change the order of elements in the resulting lists and sublists, but the result should be indeed correct.
Anton: For example, all the sublists will be in reverse order.
Dana: So we need a new unit-test function:
let test_powerset_int' candidate =
let test vs =
set_equal (candidate vs) (List.map List.rev (powerset_v7 vs))
in let b0 = test []
and b1 = test [1]
and b2 = test [2; 1]
and b3 = test [3; 2; 1]
and b4 = test [4; 3; 2; 1]
and b5 = test [5; 4; 3; 2; 1]
and b6 = test [6; 5; 4; 3; 2; 1]
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6;;
Alfrothul: I see – the sublists are reversed and the order of the lists is left to set_equal. Let’s do this:
let powerset_v7' vs_given =
list_fold_left
[[]]
(fun v vss ->
list_fold_left
vss
(fun vs vss' ->
(v :: vs) :: vss')
vss)
vs_given;;
Pablito (hanging on): Testing again:
# test_powerset_int' powerset_v7';;
- : bool = true
#
Anton: I wonder how this function works.
Alfrothul: To discover that, we can unfold the two calls to list_fold_left and simplify. Skipping a few steps...
Anton: You don’t say.
Dana (unrattled): They are spelled out in the accompanying resource file.
Alfrothul: ...we obtain the following tail-recursive definition:
let powerset_v0' vs_given =
let rec outer_loop vs outer_a =
match vs with
| [] ->
outer_a
| v :: vs' ->
let rec inner_loop vss inner_a =
match vss with
| [] ->
outer_loop vs' inner_a
| vs :: vss' ->
inner_loop vss' ((v :: vs) :: inner_a)
in inner_loop outer_a outer_a
in outer_loop vs_given [[]];;
Dana: And a listless one too.
Anton: Renaming the outer instance of traverse as outer_loop and the inner instance as inner_loop makes sense.
Dana: Ditto for the outer accumulator and the inner accumulator.
Pablito (bravely): Testing, testing:
# test_powerset_int' powerset_v0';;
- : bool = true
#
Alfrothul (candidly): Man, I would be hard pressed to define powerset_v0' by hand in the first place.
Mimer: That’s another aspect of unfolding function calls.
Anton: What do you mean?
Mimer: In the chapter about Inlining functions, we have unfolded calls to a fold function to verify that we fall back on our feet when inlining its definition.
Alfrothul: But here we didn’t start from a structurally recursive function so we are not in position to fall back on our feet.
Mimer: True. But we are in position to discover the underlying iterative program that does the job. In doing so, we can indeed realize that inlining doesn’t merely make us fall back on our feet, as in Chapter about Inlining functions, it can make us discover a new program that we did not know yet, one that we can then wonder whether we could have written by hand in the first place (as you just did when seeing powerset_v0'), or that can suggest other programs.
Dana: So Platonism is also at work in computer science, in that programs are not only invented, they can also be discovered?
Mimer: Indeed. Programs are not just things that we write independently of each other: they are things that we can relate to each other, that we can reason about using observational equivalence, and that we can derive or calculate from other programs, from specifications, or from properties.
Dana: Care to give another example?
Mimer: Thanks for asking. Remember fibfib in Week 06?
Alfrothul (modestly): We do. It was in the Interlude in the chapter about The case of the Fibonacci numbers:
let fibfib n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then (0, 1)
else let i' = i - 1
in let (fib_i', fib_succ_i') = visit i'
in (fib_succ_i', fib_i' + fib_succ_i')
in visit n;;
Mimer: The point of Exercise 31 that week was to express fibfib using nat_fold_right.
Anton: Right:
let fibfib_gen n =
nat_fold_right
(0, 1)
(fun (fib_i', fib_succ_i') -> (fib_succ_i', fib_i' + fib_succ_i'))
n;;
Dana: OK, so inlining nat_fold_right in the definition of fibfib_gen makes us fall back on our feet in that it gives us back the definition of fibfib. That’s not a new example.
Mimer: Indeed it isn’t, unless we first replace nat_fold_right with nat_fold_left.
Dana: nat_fold_left?
Mimer: The generic counterpart of a structurally tail-recursive definition over a natural number with an accumulator:
let nat_fold_left zero_case succ_case n =
let () = assert (n >= 0) in
let rec loop i a =
if i = 0
then a
else loop (pred i) (succ_case a)
in loop n zero_case;;
Dana: OK...
Mimer: Given a zero case zero_specific, a successor case succ_specific, and, e.g., the non-negative integer 3, i.e., the result of evaluating:
succ (succ (succ 0))
nat_fold_left essentially yields the result of evaluating:
succ_specific (succ_specific (succ_specific zero_specific))
In words, given a non-negative integer n represented as n, evaluating nat_fold_left zero_specific succ_specific n tail-recursively gives rise to n nested applications of succ_specific that mirror the n nested occurrences of succ that constructed n.
Dana: That’s pretty similar to the essence of nat-fold-right.
Mimer: Indeed, Dana. Fun fact – nat_fold_left and nat_fold_right are equivalent, since applying either to z, s, and n yields s (s (s (... (s z)...))) where s is applied n times, assuming that n denotes n. These applications are nested recursively if we use nat_fold_right and they are nested tail-recursively, i.e., accumulated, if we use nat_fold_left.
Dana: Wow. This means that replacing nat_fold_right with nat_fold_left in any of our implementations makes this implementation tail-recursive instead of recursive, just like that.
Mimer: Yup. And now aren’t you curious what these tail-recursive implementations look like?
Dana: OK, OK, we should inline the definition of nat_fold_left to know what they look like. Let me try, starting with:
let tr_fibfib_v0 n =
nat_fold_left
(0, 1)
(fun (fib_k, fib_succ_k) -> (fib_succ_k, fib_k + fib_succ_k))
n;;
Pablito: You are going to do as in the chapter about Inlining functions in Week 07, right?
Dana: Right.
Pablito: Just a sec:
let test_fibfib candidate =
let b0 = (candidate 0 = (0, 1))
and b1 = (candidate 1 = (1, 1))
and b2 = (candidate 2 = (1, 2))
and b3 = (candidate 3 = (2, 3))
and b4 = (candidate 4 = (3, 5))
and b5 = (candidate 5 = (5, 8))
in b0 && b1 && b2 && b3 && b4 && b5;;
Dana: Thanks, Pablito. First, unfolding the call and applying the function denoted by nat_fold_left:
let tr_fibfib_v1 n =
let n = n
and succ_case = (fun (fib_k, fib_succ_k) -> (fib_succ_k, fib_k + fib_succ_k))
and zero_case = (0, 1)
in let () = assert (n >= 0) in
let rec loop i a =
if i = 0
then a
else loop (pred i) (succ_case a)
in loop n zero_case;;
Pablito: Check!
Dana: The three definienses are values, so let us unfold the let-expression:
let tr_fibfib_v2 n =
let () = assert (n >= 0) in
let rec loop i a =
if i = 0
then a
else loop (pred i) ((fun (fib_k, fib_succ_k) -> (fib_succ_k, fib_k + fib_succ_k)) a)
in loop n (0, 1);;
Pablito: Check!
Dana: The accumulator is a pair, so let me replace a with a pair:
let tr_fibfib_v3 n =
let () = assert (n >= 0) in
let rec loop i (fib_k, fib_succ_k) =
if i = 0
then (fib_k, fib_succ_k)
else loop (pred i) ((fun (fib_k, fib_succ_k) -> (fib_succ_k, fib_k + fib_succ_k)) (fib_k, fib_succ_k))
in loop n (0, 1);;
Mimer: Good choice of names, Dana.
Pablito: And it checks too.
Dana: Thanks. In the induction step, the application is trivial, so let us unfold it:
let tr_fibfib_v4 n =
let () = assert (n >= 0) in
let rec loop i (fib_k, fib_succ_k) =
if i = 0
then (fib_k, fib_succ_k)
else loop (pred i) (fib_succ_k, fib_k + fib_succ_k)
in loop n (0, 1);;
Pablito: Check!
Anton: What do you know? That’s a tail-recursive definition of fibfib with an accumulator.
Alfrothul: With a pair of accumulators, actually. How about we curry loop?
Dana: Good idea, Alfrothul:
let tr_fibfib_v5 n =
let () = assert (n >= 0) in
let rec loop i fib_k fib_succ_k =
if i = 0
then (fib_k, fib_succ_k)
else loop (pred i) fib_succ_k (fib_k + fib_succ_k)
in loop n 0 1;;
Pablito: Check!
Mimer: See? Discovered, not invented.
Dana: Thanks.
Alfrothul: Wait. What if fibfib only returned the first component of the pair, instead of returning the pair?
Anton: Aha, that would make it compute the Fibonacci function tail-recursively and with two accumulators:
let tr_fib n =
let () = assert (n >= 0) in
let rec loop i fib_k fib_succ_k =
if i = 0
then fib_k
else loop (pred i) fib_succ_k (fib_k + fib_succ_k)
in loop n 0 1;;
Alfrothul: In linear time.
Halcyon: Words fail me.
Loki: How about “discovered, not invented”?
Mimer: In any case, and at the risk of not leaving well enough alone, do you guys remember your clever implementation of the factorial function using nat_fold_right in Week 06?
Dana: Yes, that was Exercise 25.
Mimer: Aren’t you curious of what you actually implemented?
Dana: OK Mimer. Oops, I didn’t mean the way that sounded, please forgive me.
Mimer: There is nothing to forgive, it’s just my name, and it is OK.
Dana: Still, I am curious, and I will get back to it and inline the definition of nat_fold_right to see what I actually implemented.
Mimer: While you are at it, you could also replace nat_fold_right with nat_fold_left in your implementation.
Dana: OMG. That will give me a tail-recursive implementation. OK, now I am really curious to see what that implementation looks like. Bye for now.
Mimer: And she’s gone. Platonism rules.
Alfrothul: Hmmm.
Mimer: Yes, Alfrothul?
Alfrothul <clickety clickety clickety click>: Let me visualize the computation with a trace:
# traced_tr_fib 6;;
tr_fib 6 ->
loop 6 0 1 ->
loop 5 1 1 ->
loop 4 1 2 ->
loop 3 2 3 ->
loop 2 3 5 ->
loop 1 5 8 ->
loop 0 8 13 ->
- : int = 8
#
Anton: Right – pairs of successive Fibonacci numbers are enumerated, starting from the first one.
Alfrothul: Wait. Let me compare this tail-recursive trace with a trace of the recursive definition of the Fibonacci function in our “Calculemus interlude”:
# traced_fib_v5 6;;
fib_v5 6 ->
visit 6 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- (0, 1)
visit 1 <- (1, 1)
visit 2 <- (1, 2)
visit 3 <- (2, 3)
visit 4 <- (3, 5)
visit 5 <- (5, 8)
visit 6 <- (8, 13)
fib_v5 6 <- 8
- : int = 8
#
Anton: The pairs of the successive Fibonacci numbers are enumerated too, but at return time instead of at tail-call time. I think this is the point of using a tail-recursive function with an accumulator.
Mimer: Tis.
Alfrothul: Yes, I see that.
Anton: The tail-recursive function is more efficient: given a non-negative integer n, it performs n+1 tail calls to loop, whereas the recursive function performs n+1 calls to visit and n+1 returns from visit.
Alfrothul: Right. But still.
Bong-sun: The recursive version is easier to reason about, since applying visit to i returns (fib_i, fib_succ i), but the relation between the three arguments of loop, in loop i fib_k fib_succ_k is less immediate. How are i and k related exactly?
Alfrothul: Thanks, Bong-sun. Well put.
Bong-sun (practical): Well, let’s see:
loop 6 fib_0 fib_1 ->
loop 5 fib_1 fib_2 ->
loop 4 fib_2 fib_3 ->
loop 3 fib_3 fib_4 ->
loop 2 fib_4 fib_5 ->
loop 1 fib_5 fib_6 ->
loop 0 fib_6 fib_7 ->
Alfrothul: Eureka: i + k = n.
Bong-sun: Let’s check that with an assertion:
let tr_fib_with_an_assertion n =
let () = assert (n >= 0) in
let rec loop i fib_k fib_succ_k =
let () = assert (fib_k = tr_fib (n - i)) in
if i = 0
then fib_k
else loop (pred i) fib_succ_k (fib_k + fib_succ_k)
in loop n 0 1;;
Pablito: Checking:
# tr_fib_with_an_assertion 6;;
- : int = 8
#
Bong-sun: And checked. Thanks, Pablito.
Alfrothul: So a structurally recursive function is simpler to reason about, and a structurally tail-recursive function with an accumulator is more efficient to run.
Mimer: That about sums it up.
Anton: A post-postlude now.
Alfrothul: Yes. A practical one.
Anton: Go ahead.
Alfrothul: The tail-recursive implementation of the powerset function is critical in OCaml.
Anton: You mean compared to the original recursive implementation?
Alfrothul: Yes. You know how if the cardinality of a set is n, the cardinality of its powerset is 2^n:
let exp2 n =
let () = assert (n >= 0) in
let rec visit n a =
if n = 0
then a
else visit (n - 1) (2 * a)
in visit n 1;;
Anton (prudently): I have heard about that.
Alfrothul: But OCaml’s control stack is limited, which makes the original recursive implementation impractical:
# List.length (powerset_v1 (List.init 20 (fun n -> n))) = exp2 20;;
Stack overflow during evaluation (looping recursion?).
#
Anton: The tail-recursive implementation, however:
# List.length (powerset_v0' (List.init 25 (fun n -> n))) = exp2 25;;
Anton: Wait for it:
- : bool = true
#
The goal of this exercise is to explore nat_parafold_left, which is to nat_parafold_right what nat_fold_left is to nat_fold_right.
Bong-sun: Fourth Wall?
The fourth wall: Yes, yes.
Bong-sun: Thank you. Let’s see. Back in Week 06, the point was that given a zero case zero_specific, a successor case succ_specific, and, e.g., the non-negative integer 3, i.e., the result of evaluating:
succ (succ (succ 0))
nat_parafold_right essentially yields the result of evaluating:
succ_specific 2 (succ_specific 1 (succ_specific 0 zero_specific))
The fourth wall: So in words, given a non-negative integer n represented as n, evaluating nat_parafold_right zero_specific succ_specific n recursively gives rise to n nested applications of succ_specific that mimic the n nested occurrences of succ that constructed n, and each of the calls to succ_specific is also passed a decreasing index.
Bong-sun: Right. Something similar should hold for nat_parafold_left. Given a zero case zero_specific, a successor case succ_specific, and, e.g., the non-negative integer 3, i.e., the result of evaluating:
succ (succ (succ 0))
nat_parafold_left essentially yields the result of evaluating:
succ_specific 0 (succ_specific 1 (succ_specific 2 zero_specific))
The fourth wall: So in words, given a non-negative integer n represented as n, evaluating nat_parafold_left zero_specific succ_specific n tail-recursively gives rise to n nested applications of succ_specific that mimic the n nested occurrences of succ that constructed n, accumulating each of the calls to succ_specific with a decreasing index. Shooting from the hip:
let nat_parafold_left zero_case succ_case n =
(* nat_parafold_left : 'a -> (int -> 'a -> 'a) -> int -> 'a *)
let () = assert (n >= 0) in
let rec visit i a =
if i = 0
then a
else let i' = pred i
in visit i' (succ_case i' a) (* <-- succ_case takes two arguments *)
in visit n zero_case;;
Bong-sun: The type of nat_parafold_left is 'a -> (int -> 'a -> 'a) -> int -> 'a:
Alfrothul (standing by): So like for list_fold_left and list_fold_right, nat_parafold_left and nat_parafold_right are equivalent if their induction-step parameter is associative and commutative.
Anton: Like the multiplication function.
Bong-sun: Right. Factorial function, here we come again:
let fac_right n =
let () = assert (n >= 0) in
nat_parafold_right
1
(fun i' ih ->
succ i' * ih)
n;;
let fac_left n =
let () = assert (n >= 0) in
nat_parafold_left
1
(fun i' ih ->
succ i' * ih)
n;;
Dana: And if we inline the call to nat_parafold_right in the definition of fac_right, we get the usual recursive implementation of the factorial function.
Alfrothul: And if we inline the call to nat_parafold_left in the definition of fac_left, we get the usual recursive tail-implementation of the factorial function with an accumulator.
The fourth wall: Yay!
Everybody looks at it.
The fourth wall: Look, there is a couple of exercises right below.
Which function does nat_parafold_right emulate when zero_case is [] and succ_case is (fun x ih -> x :: ih), i.e., List.cons?
In other words, you are asked to characterize this OCaml function:
let this_OCaml_function n =
nat_parafold_right [] (fun i' ih -> i' :: ih) n;;
Subsidiary question – in reference to Exercise 01, characterize this alternative OCaml function:
let this_alternative_OCaml_function n =
nat_parafold_right [] (fun i' ih -> List.append ih [i']) n;;
Joe Dassin: À toi...Halcyon (chorusing): À la façon que tu as d’être belle...
Which function does nat_parafold_left emulate when zero_case is [] and succ_case is (fun x ih -> x :: ih), i.e., List.cons?
In other words, you are asked to characterize this other OCaml function:
let this_other_OCaml_function n =
nat_parafold_left [] (fun i' ih -> i' :: ih) n;;
Subsidiary question – in reference to Exercise 01, characterize this alternative OCaml function:
let this_alternative_other_OCaml_function n =
nat_parafold_left [] (fun i' ih -> List.append ih [i']) n;;
Added Exercise 25 and its solution, Exercise 26, and Exercise 27 and aligned Exercise 12 and Exercise 18 [16 Apr 2023]
Expanded the postlude with traces [04 Mar 2023]
Created [10 Jan 2023]