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_init =
let rec traverse vs =
match vs with
| [] ->
...
| v :: vs' ->
let ih = traverse vs'
in ...
in traverse vs_init;;
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_init =
(* 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_init;;
Given a nil case nil_specific, a cons case cons_specific, and a list v0 :: v1 :: v2 :: v3 :: [], which was constructed by 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, the result of list_fold_right is a series of nested applications of cons_specific that mimics the nested occurrences of the original constructor List.cons in the given list.
Here is how we had defined the length function:
let length vs_init =
let rec measure vs =
match vs with
| [] ->
0
| v :: vs' ->
let ih = measure vs'
in succ ih
in measure vs_init;;
(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_alt vs =
list_fold_right 0
(fun v ih ->
1 + ih)
vs;;
This alternative 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_yourself vs_init =
(* 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_yourself v) ^ " :: " ^ ih
in visit vs_init;;
By instantiating nil_case to be "[]" and cons_case to be (fun v ih -> (show_yourself 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_alt show_yourself vs_init =
(* show_list_in_long_hand_alt : ('a -> string) -> 'a list -> string *)
list_fold_right "[]"
(fun v ih ->
(show_yourself v) ^ " :: " ^ ih)
vs_init;;
This alternative 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_yourself vs =
(* show_list_in_short_hand : ('a -> string) -> 'a list -> string *)
"[" ^ match vs with
| [] ->
"]"
| v :: vs' ->
(show_yourself 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_yourself v) ^ ih
in show_list_aux vs');;
By instantiating nil_case to be "]" and cons_case to be (fun v ih -> "; " ^ (show_yourself 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_alt show_yourself vs =
(* show_list_in_short_hand : ('a -> string) -> 'a list -> string *)
"[" ^ match vs with
| [] ->
"]"
| v :: vs' ->
(show_yourself v) ^ (list_fold_right "]"
(fun v ih ->
"; " ^ (show_yourself v) ^ ih)
vs');;
This alternative 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_init =
(* 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_init;;
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_alt vs_init =
list_fold_right []
(fun v ih ->
v :: v :: ih)
vs_init;;
This alternative implementation passes the corresponding unit tests.
Here is how we had defined a function to concatenate lists:
let append xs_init ys_init =
let rec visit xs =
match xs with
| [] ->
ys_init
| x :: xs' ->
let ih = visit xs'
in x :: ih
in visit xs_init;;
Given two lists xs_init and ys_init, by instantiating nil_case to be ys_init and cons_case to be (fun x ih -> x :: ih), we make list_fold_right emulate the computation of the append function:
let append_alt xs_init ys_init =
list_fold_right ys_init
(fun x ih ->
x :: ih)
xs_init;;
This alternative 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_init =
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_init;;
Given an element e and a list es_init, 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_alt e es_init =
list_fold_right false
(fun e' ih ->
if e = e'
then true
else ih)
es_init;;
This alternative implementation passes the corresponding unit tests.
Given a list, what happens if we instantiate nil_case to be [] and cons_case to be (fun x ih -> x :: ih), i.e., List.cons? Which function does list_fold_right emulate then?
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;;
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 9 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_alt e1s e2s =
list_fold_right e2s
(fun e ih ->
if belongs_to e e2s
then ih
else e :: ih)
e1s;;
This alternative implementation passes the corresponding unit tests.
Revisit Exercise 11 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 14 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 17 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_init ws_init =
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_init
in traverse_1 vs_init;;
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_alt' vs_init ws_init =
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_init
in traverse_1 vs_init;;
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_init):
let cartesian_product_2_alt vs_init ws_init =
list_fold_right []
(fun v ih_outer ->
list_fold_right ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_init)
vs_init;;
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_init ws_init xs_init =
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_init
in traverse_2 ws_init
in traverse_1 vs_init;;
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_alt'' vs_init ws_init xs_init =
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_init
in traverse_2 ws_init
in traverse_1 vs_init;;
This alternative 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_init):
let cartesian_product_3_alt' vs_init ws_init xs_init =
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_init)
ws_init
in traverse_1 vs_init;;
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 -> list_fold_right ih_median (fun x ih_inner -> (v, w, x) :: ih_inner) xs_init) ws_init):
let cartesian_product_3_alt vs_init ws_init xs_init =
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_init)
ws_init)
vs_init;;
This alternative implementation passes the corresponding unit tests.
Revisit Exercise 20 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_init =
let rec traverse vs a =
match vs with
| [] ->
a
| v :: vs' ->
traverse vs' ...
in traverse vs_init ...;;
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_init =
(* 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_init nil_case;;
Given a nil case nil_specific, a cons case cons_specific, and a list v0 :: v1 :: v2 :: v3 :: [], which was constructed by 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, the result of list_fold_left is a series of nested applications of cons_specific that mirrors the nested occurrences of the original constructor List.cons in the given list.
Here is how we had defined the length function using an accumulator:
let length_acc vs_init =
let rec measure vs a =
match vs with
| [] ->
a
| v :: vs' ->
measure vs' (1 + a)
in measure vs_init 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_alt vs =
list_fold_left 0
(fun v a ->
succ a)
vs;;
This alternative 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;;
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 4 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_init e2s_init =
let rec visit e1s a =
match e1s with
| [] ->
a
| e1 :: e1s' ->
visit e1s' (if belongs_to e1 e2s_init
then a
else e1 :: a)
in visit e1s_init e2s_init;;
By instantiating nil_case to be e2s_init and cons_case to be (fun e1 a -> if belongs_to e1 e2s_init then a else e1 :: a), we make list_fold_left emulate the computation of the set_union_acc function:
let set_union_acc_alt e1s_init e2s_init =
list_fold_left e2s_init
(fun e1 a ->
if belongs_to e1 e2s_init
then a
else e1 :: a)
e1s_init;;
This alternative implementation passes the corresponding unit tests.
Revisit Exercise 5 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 6 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 6 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_v2 f ns =
list_fold_right [] (fun n ih -> f n :: ih) ns;;
To wit:
# list_map_v2 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.
#
Harald: I feel exhausted.
Alfrothul: Still.
Harald: Still, what.
Alfrothul: Doesn’t it look like list_fold_right and list_fold_left are just one list reversal away from another?
Harald: 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.
Brynja (perspicacious): Assuming the result to be a list.
Vigfus: Actually, list_fold_right n c (List.rev vs) and list_fold_left n c vs would fit the bill too.
Brynja: 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.
Harald (hastily): And that means you too, Mimer.
Brynja (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 15) or without (as in Exercise 9), 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_alt' vs_init ws_init =
list_fold_left []
(fun v ih_outer ->
list_fold_left ih_outer
(fun w ih_inner ->
(v, w) :: ih_inner)
ws_init)
vs_init;;
val cartesian_product_2_alt' : 'a list -> 'b list -> ('a * 'b) list = <fun>
# let () = assert (test_cartesian_product_2 cartesian_product_2_alt');;
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):
let cartesian_product_star nss =
(* cartesian_product_star : 'a list list -> 'a list list *)
match nss with
| [] ->
[[]]
| n1s :: [] ->
List.map (fun x1 -> [x1]) n1s
| n1s :: n2s :: [] ->
List.map (fun (x1, x2) -> [x1; x2]) (cartesian_product_2 n1s n2s)
| n1s :: n2s :: n3s :: [] ->
List.map (fun (x1, x2, x3) -> [x1; x2; x3]) (cartesian_product_3 n1s n2s n3s)
| _ ->
let () = assert false
in [];;
Vigfus: Remember the implementation of powerset_v1?
Harald: 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_init =
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_init;;
Alfrothul: You tested it:
# test_powerset_int powerset_v1;;
- : bool = true
#
Vigfus: I did. But this implementation, is it structurally recursive?
Harald: Well, yes – its recursive calls follow the structure of its input data. Why do you ask?
Vigfus: The induction hypothesis is used twice.
Alfrothul: And so it is. But we could still express it using list_fold_right.
Brynja: Yay, more generic programming.
Vigfus: May I give it a shot?
Alfrothul: By all means.
Vigfus: Lemmesee:
let powerset_v2 vs_init =
list_fold_right
[[]]
(fun v ih ->
append_map (fun ws -> v :: ws) ih ih)
vs_init;;
Harald (courteously): Testing, testing:
# test_powerset_int powerset_v2;;
- : bool = true
#
Alfrothul: Wait a minute. The definition of append_map' is structurally recursive too.
Harald: True. Look:
let append_map' f vs rest =
list_fold_right
rest
(fun v ih ->
f v :: ih)
vs;;
Vigfus: 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?
Harald (reflexively): Unfold the call to append_map' in the definition of powerset_v2.
Alfrothul: Yes, look:
let powerset_v7 vs_init =
list_fold_right
[[]]
(fun v vss ->
list_fold_right
vss
(fun vs vss' ->
(v :: vs) :: vss')
vss)
vs_init;;
Harald: Harrumph. You, my friend, have been skipping a few derivation steps.
Alfrothul (virtuously): But they are spelled out in the accompanying resource file.
Vigfus (with uncertainty): Testing, testing:
# test_powerset_int powerset_v7;;
- : bool = true
#
Vigfus (to himself): Wow.
Mimer: According to Mike Gordon, this definition was discovered by Dave du Feu, back in the days.
Brynja (wondering): When a list represents a set, the order of its elements does not matter, right?
Harald: Right.
Brynja: 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.
Harald: For example, all the sublists will be in reverse order.
Brynja: 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_init =
list_fold_left
[[]]
(fun v vss ->
list_fold_left
vss
(fun vs vss' ->
(v :: vs) :: vss')
vss)
vs_init;;
Vigfus (hanging on): Testing again:
# test_powerset_int' powerset_v7';;
- : bool = true
#
Harald: 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...
Harald: You don’t say.
Brynja (unrattled): They are spelled out in the accompanying resource file.
Alfrothul: ...we obtain the following tail-recursive definition:
let powerset_v0' vs_init =
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_init [[]];;
Brynja: And a listless one too.
Harald: Renaming the outer instance of traverse as outer_loop and the inner instance as inner_loop makes sense.
Brynja: Ditto for the outer accumulator and the inner accumulator.
Vigfus (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.
Harald: 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.
Brynja: 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.
Brynja: 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 rec visit n =
if n = 0
then (0, 1)
else let n' = n - 1
in let (fib_n', fib_n) = visit n'
in (fib_n, fib_n' + fib_n)
in visit n;;
Mimer: The point of Exercise 11 was to express fibfib using nat_fold_right.
Harald: Right:
let fibfib_alt n =
nat_fold_right
(0, 1)
(fun (fib_k', fib_k) -> (fib_k, fib_k' + fib_k))
n;;
Brynja: OK, so inlining nat_fold_right in the definition of fibfib_alt 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 by nat_fold_left.
Brynja: 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 rec loop n a =
if n = 0
then a
else loop (pred n) (succ_case a)
in loop n zero_case;;
Brynja: OK...
Mimer: 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.
Brynja: Wow. This means that replacing nat_fold_right by 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?
Brynja: 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_k) -> (fib_k, fib_k' + fib_k))
n;;
Vigfus: You are going to do as in the chapter about Inlining functions in Week 07, right?
Brynja: Right.
Vigfus: 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;;
Brynja: Thanks, Vigfus. 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_k) -> (fib_k, fib_k' + fib_k))
and zero_case = (0, 1)
in let rec loop n a =
if n = 0
then a
else loop (pred n) (succ_case a)
in loop n zero_case;;
Vigfus: Check!
Brynja: The three definienses are values, so let us unfold the let-expression:
let tr_fibfib_v2 n =
let rec loop n a =
if n = 0
then a
else loop (pred n) ((fun (fib_k', fib_k) -> (fib_k, fib_k' + fib_k)) a)
in loop n (0, 1);;
Vigfus: Check!
Brynja: The accumulator is a pair, so let me replace a with a pair:
let tr_fibfib_v3 n =
let rec loop n (fib_k', fib_k) =
if n = 0
then (fib_k', fib_k)
else loop (pred n) ((fun (fib_k', fib_k) -> (fib_k, fib_k' + fib_k)) (fib_k', fib_k))
in loop n (0, 1);;
Mimer: Good choice of names, Brynja.
Vigfus: And it checks too.
Brynja: Thanks. In the induction step, the application is trivial, so let us unfold it:
let tr_fibfib_v4 n =
let rec loop n (fib_k', fib_k) =
if n = 0
then (fib_k', fib_k)
else loop (pred n) (fib_k, fib_k' + fib_k)
in loop n (0, 1);;
Vigfus: Check!
Harald: 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?
Brynja: Good idea, Alfrothul:
let tr_fibfib_v5 n =
let rec loop n fib_k' fib_k =
if n = 0
then (fib_k', fib_k)
else loop (pred n) fib_k (fib_k' + fib_k)
in loop n 0 1;;
Vigfus: Check!
Mimer: See? Discovered, not invented.
Brynja: Thanks.
Alfrothul: Wait. What if fibfib only returned the first component of the pair, instead of returning the pair?
Harald: Aha, that would make it compute the Fibonacci function tail-recursively and with two accumulators:
let tr_fib n =
let rec loop n fib_k' fib_k =
if n = 0
then fib_k'
else loop (pred n) fib_k (fib_k' + fib_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 the midterm project?
Brynja: Yes, that was Exercise 3 (hard) in Week 06.
Mimer: Aren’t you curious of what you actually implemented?
Brynja: 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.
Brynja: 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 by nat_fold_left in your implementation.
Brynja: 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.
Harald: A post-postlude now.
Alfrothul: Yes. A practical one.
Harald: Go ahead.
Alfrothul: The tail-recursive implementation of the powerset function is critical in OCaml.
Harald: 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;;
Harald (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?).
#
Harald: The tail-recursive implementation, however:
# List.length (powerset_v0' (List.init 25 (fun n -> n))) = exp2 25;;
Harald: Wait for it:
- : bool = true
#
Extended the postlude about Platonism with fibfib and with nat_fold_left [16 Apr 2021]
Fixed the type of traverse in the definition of list_fold_left, thanks to Aditya Singhania’s eagle eye [12 Apr 2021]
Added the post-postlude [01 Apr 2021]
Created [20 Mar 2021]