Programming using accumulators

The goal of this lecture note is to illustrate the many uses of accumulators in functional programming.

Resources

Adding natural numbers: the unit tests

Let us define the addition of two natural numbers:

let test_add a =
      (* an instance of the base case: *)
  let b0 = (let y = Random.int 2000
            in a 0 y = y)
      (* a random instance of the induction step: *)
  and b1 = (let y = Random.int 2000
            and x' = Random.int 1000
            in a (succ x') y = succ (a x' y))
      (* a few handpicked numbers: *)
  and b2 = (a 0 100 = 100)
  and b3 = (a 1 100 = 101)
  and b4 = (a 2 100 = 102)
      (* using a witness implementation of the addition function *)
  and b5 = (let x = Random.int 1000
            and y = Random.int 2000
            in a x y = x + y)
  (* etc. *)
  in b0 && b1 && b2 && b3 && b4 && b5;;

Adding natural numbers: Version 1, lambda-dropped

The addition function is applied to two arguments, x and y. Given y, it is specified by induction over x, in a lambda-dropped fashion (“lambda-dropped” means that the definition of visit below is scope-sensitive, in that it uses y_given which is declared outside the definition):

  • base case (x = 0):

    we define the addition of 0 and y to be y

    In words: adding 0 to y yields y.

  • induction step (x = succ x’):

    induction hypothesis: adding x’ and y yields a natural number ih

    we define the addition of (succ x’) and y to be succ ih

    In words, if adding x’ to y yields the natural number ih, then adding the successor of x’ to y yields the successor of ih.

The following recursive function embodies this inductive specification:

let add_v1 x_given y_given =
  let () = assert (x_given >= 0) in
  let rec visit x =
    if x = 0
    then y_given
    else let x' = pred x
         in let ih = visit x'
            in succ ih
  in visit x_given;;

Or again, unfolding the let-expressions since they are cosmetic:

let add_v1' x_given y_given =
  let () = assert (x_given >= 0) in
  let rec visit x =
    if x = 0
    then y_given
    else succ (visit (pred x))
  in visit x_given;;

Both functions pass the unit test:

# test_add add_v1;;
- : bool = true
# test_add add_v1';;
- : bool = true
#

Adding natural numbers: Version 2, lambda-lifted

Alternatively, we can move the quantification over y from the top level to after the quantification of x. We still specify the addition function by induction over its first argument, x, in a lambda-lifted fashion (“lambda-lifted” means that the definition of visit below is scope-insensitive, in that it only uses names that are declared as part of the definition):

  • base case (x = 0):

    given a natural number y, we define the addition of 0 and y to be y

    In words: adding 0 to any natural number yields that natural number.

  • induction step (x = succ x’):

    induction hypothesis: for all natural numbers y, adding x’ and y yields a natural number ih

    given a natural number y, we define the addition of (succ x’) and y to be succ ih

    In words, if adding two natural numbers x’ and y yields the natural number ih, then adding the successor of x’ to y yields the successor of ih.

The following recursive function embodies this inductive specification:

let add_v2 x_given y_given =
  let () = assert (x_given >= 0) in
  let rec visit x y =
    if x = 0
    then y
    else let x' = pred x
         in let ih = visit x'
            in succ (ih y)
  in visit x_given y_given;;

Or again, unfolding the let-expressions:

let add_v2' x_given y_given =
  let () = assert (x_given >= 0) in
  let rec visit x y =
    if x = 0
    then y
    else succ (visit (pred x) y)
  in visit x_given y_given;;

And lo and behold, both functions pass the unit test:

# test_add add_v2;;
- : bool = true
# test_add add_v2';;
- : bool = true
#

Exercise 05

Express add_v2 using nat_fold_right.

Adding natural numbers: Version 3, using an accumulator

As another alternative, we can use the second argument of the addition function as an accumulator:

  • base case (x = 0):

    given a natural number y, we define the addition of 0 and y to be y

    In words: adding 0 to any natural number yields that natural number.

  • induction step (x = succ x’):

    induction hypothesis: for all natural numbers y, adding x’ and y yields a natural number r

    given a natural number y, if adding x’ and (succ y) gives r, then adding (succ x’) and y also gives r

    In words, adding (succ x’) and y gives the same result as adding x’ and (succ y).

Computationally, instead of waiting that the recursive call completes to increment the result with 1, we directly increment the second argument in the call.

The following recursive function embodies this inductive specification:

let add_v3 x_given y_given =
  let () = assert (x_given >= 0) in
  let rec visit x y =
    if x = 0
    then y
    else let x' = pred x
         in let ih = visit x'
            in ih (succ y)
  in visit x_given y_given;;

Or again, unfolding the let-expressions:

let add_v3' x_given y_given =
  let () = assert (x_given >= 0) in
  let rec visit x y =
    if x = 0
    then y
    else visit (pred x) (succ y)
  in visit x_given y_given;;

Both functions pass the unit test:

# test_add add_v3;;
- : bool = true
# test_add add_v3';;
- : bool = true
#

Accumulators in a nutshell

Bottom line: accumulators make it possible to start constructing the result as we go, instead of having to wait until the current recursive call has completed. In general, a function that uses an accumulator differs from a function that does not, witness reverse_v4 and its accumulatorless counterpart:

let reverse_v4 vs_given =
  let rec visit vs a =
    match vs with
    | [] ->
       a
    | v :: vs' ->
       visit vs' (v :: a)
  in visit vs_given [];;

let look_Ma_no_accumulator vs_given =
  let rec visit vs =
    match vs with
    | [] ->
       []
    | v :: vs' ->
       v :: visit vs'
  in visit vs_given;;

Traced versions of these functions (defined in the resource file for the present lecture note) illustrate this difference:

# traced_reverse_v4 [1; 2; 3; 4; 5];;
visit [1; 2; 3; 4; 5] [] ->
visit [2; 3; 4; 5] [1] ->
visit [3; 4; 5] [2; 1] ->
visit [4; 5] [3; 2; 1] ->
visit [5] [4; 3; 2; 1] ->
visit [] [5; 4; 3; 2; 1] ->
visit [1; 2; 3; 4; 5] [] <- [5; 4; 3; 2; 1]
- : int list = [5; 4; 3; 2; 1]
# traced_look_Ma_no_accumulator [1; 2; 3; 4; 5];;
visit [1; 2; 3; 4; 5] ->
  visit [2; 3; 4; 5] ->
    visit [3; 4; 5] ->
      visit [4; 5] ->
        visit [5] ->
          visit [] ->
          visit [] <- []
        visit [5] <- [5]
      visit [4; 5] <- [4; 5]
    visit [3; 4; 5] <- [3; 4; 5]
  visit [2; 3; 4; 5] <- [2; 3; 4; 5]
visit [1; 2; 3; 4; 5] <- [1; 2; 3; 4; 5]
- : int list = [1; 2; 3; 4; 5]
#

It can be proved that unless the binary operation over the accumulator, in the induction step, is both associative and commutative, accumulator-based and accumulatorless functions yield distinct results:

  • in the list-reversal function above and in the iota function below, the binary operation is List.cons, which is not commutative (witness its type) and not associative (also witness its type); and
  • in the addition function above and the length function below, the binary operation is +, which is both associative and commutative.

A converse of atoi: iota

Given a non-negative integer n, the iota function constructs a list of increasing integers from 0 to n-1, i.e., the list of the first n natural numbers:

let test_iota candidate =
  let b0 = (candidate 0 = [])
  and b1 = (candidate 1 = [0])
  and b2 = (candidate 2 = [0; 1])
  and b3 = (candidate 3 = [0; 1; 2])
  and b4 = (candidate 4 = [0; 1; 2; 3])
  (* etc. *)
  in b0 && b1 && b2 && b3 && b4;;

Obviously, it is the accumulator-based counterpart of atoi:

let iota n_given =
  let rec visit n a =
    match n with
    | 0 ->
       a
    | _ ->
       let n' = pred n
       in visit n' (n' :: a)
  in visit n_given [];;

And it passes its unit test too:

# test_iota iota;;
- : bool = true
#

Exercise 06

Given a non-negative integer, the following function applies both iota and atoi to it, and then adds the elements of the resulting two lists pointwise:

let funny n =
  let rec visit ms ns =
    if ms = []
    then []
    else (List.hd ms + List.hd ns) :: (visit (List.tl ms) (List.tl ns))
  in visit (iota n) (atoi n);;
  1. What is the result of applying funny to a non-negative integer n?
  2. Based on this result, suggest an efficient way to sum the n first consecutive integers (in either direction, i.e., from 0 to n-1 or from n-1 to 0), for any n.

Interlude about List.init

Anton: Aha.

Alfrothul: Yes?

Anton: I see that in the List module, there is also an init function.

Alfrothul: You mean as in the String module?

Anton: Yes:

# List.init;;
- : int -> (int -> 'a) -> 'a list = <fun>
# String.init;;
- : int -> (int -> char) -> string = <fun>
#

Alfrothul: So we can initialize a list. Let’s try with the identity function, to obtain a list of integers:

# List.init 3 (fun i -> i);;
- : int list = [0; 1; 2]
#

Anton: iota, we meet again:

# test_iota (fun n -> List.init n (fun i -> i));;
- : bool = true
#

Alfrothul: What about atoi?

Anton: Well, pretty much as in one of the mini-project, I would think:

# test_atoi (fun n -> let last_index = pred n in List.init n (fun i -> last_index - i));;
- : bool = true
#

Alfrothul: Well, well.

Alphonse Karr: Plus ça change, plus c’est la même chose.

Mimer: Monsieur Karr! Thanks for passing by.

Computing the length of a list using an accumulator

Let us specify a relation between a given list (vs_given), its successive suffixes (vs), and the length of the corresponding prefixes (a). This relation is inductive on the given list and states that adding a to the length of vs gives the length of vs_given:

  • base case (vs = [] and a is the length of the corresponding prefix in vs_given):

    if the suffix of vs_given is the empty list, the corresponding prefix is vs_given, and therefore a is the length of vs_given

  • induction step (vs = v :: vs’ and a is the length of the corresponding prefix):

    succ a is the length of the prefix of vs’ in vs_given

    induction hypothesis: adding succ a to the length of vs’ gives the length of vs_given

    therefore adding a to the length of v :: vs’ also gives the length of vs_given

The following recursive function embodies this inductive relation:

let length_acc vs_given =
  let rec walk vs a =
    match vs with
    | [] ->
       a
    | v :: vs' ->
       walk vs' (succ a)
  in walk vs_given 0;;

Each (tail) call to walk satisfies the relation above:

  • for any call walk vs a that satisfies the relation (i.e., adding the denotation of a to the length of the denotation of vs gives the length of the denotation of vs_given, i.e., of the given list), there are two cases:

    • vs denotes the empty list, which has length 0:

      the relation says that adding the denotation of a to 0 gives the length of the given list; therefore a denotes this length; this call is the final call and therefore the result is the length of the given list;

    • vs denotes a nonempty list and has length 1 + n’, for some natural number n’:

      the relation says that adding the denotation of a to succ n’ gives the length of the given list; since adding the denotation of succ a to n’ (i.e., the length of the tail of the list denoted by vs) gives the same number as adding the denotation of a to succ n’, the next call satisfies the relation;

  • in the initial call, vs denotes the given list, and since adding 0 to the length of this list gives the length of the given list, the relation is satisfied.

So the relation is a loop invariant for walk.

Traced versions of the length functions (defined in the resource file for the present lecture note) illustrate the two constructions of the result:

# traced_length_int [1; 2; 3; 4; 5];;
walk [1; 2; 3; 4; 5] ->
  walk [2; 3; 4; 5] ->
    walk [3; 4; 5] ->
      walk [4; 5] ->
        walk [5] ->
          walk [] ->
          walk [] <- 0
        walk [5] <- 1
      walk [4; 5] <- 2
    walk [3; 4; 5] <- 3
  walk [2; 3; 4; 5] <- 4
walk [1; 2; 3; 4; 5] <- 5
- : int = 5
# traced_length_acc_int [1; 2; 3; 4; 5];;
walk [1; 2; 3; 4; 5] 0 ->
walk [2; 3; 4; 5] 1 ->
walk [3; 4; 5] 2 ->
walk [4; 5] 3 ->
walk [5] 4 ->
walk [] 5 ->
walk [1; 2; 3; 4; 5] 0 <- 5
- : int = 5
#

Since the input list contains 5 elements, in both cases there are 6 calls to walk:

  • 6 calls and 6 subsequent returns take place for length, and
  • 6 tail calls and 1 subsequent return take place for length_acc.

Computing factorial numbers using an accumulator

Likewise, the factorial function lends itself to an accumulator-based counterpart where the multiplications are performed in sync with the (tail) calls, instead of at return time, in sync with the non-tail calls:

let fac n =
  let () = assert (n >= 0) in
  let rec visit i =
    if i = 0
    then 1
    else i * visit (pred i)
  in visit n;;

let fac_acc n =
  let () = assert (n >= 0) in
  let rec visit i a =
    if i = 0
    then a
    else visit (pred i) (i * a)
  in visit n 1;;

Traced versions of these functions (defined in the resource file for the present lecture note) illustrate the two series of multiplications:

# traced_fac 5;;
visit 5 ->
  visit 4 ->
    visit 3 ->
      visit 2 ->
        visit 1 ->
          visit 0 ->
          visit 0 <- 1
        visit 1 <- 1
      visit 2 <- 2
    visit 3 <- 6
  visit 4 <- 24
visit 5 <- 120
- : int = 120
# traced_fac_acc 5;;
visit 5 1 ->
visit 4 5 ->
visit 3 20 ->
visit 2 60 ->
visit 1 120 ->
visit 0 120 ->
visit 5 1 <- 120
- : int = 120
#

Since the input is 5, in both cases there are 6 calls to visit:

  • 6 calls and 6 subsequent returns take place for fac, and
  • 6 tail calls and 1 subsequent return take place for fac_acc.

Food for thought:

  • Characterize the successive values of the accumulator in fac_acc.

Interlude

Pablito: We have seen these successive values of the accumulator, we have seen these successive values of the accumulator.

Bong-sun: Yes we have. In Week 05.

Pablito: Right! In the section about the rise and fall of Factorial numbers. In the recursive implementation, the successive results of visit are the rising Factorial numbers, and in the tail-recursive implementation, the successive values of the accumulator are the falling Factorial numbers.

Bong-sun (facetiously): How about we verify here what Dana verified there?

Pablito: You mean with an assertion?

Bong-sun: I do mean:

let fac_acc_with_an_assertion n =
  let () = assert (n >= 0) in
  let fac_n = fac n
  in let rec visit i a =
       let () = assert (a = fac_n / fac i) in
       if i = 0
       then a
       else visit (pred i) (i * a)
     in visit n 1;;

Halcyon: Checking:

# test_fac fac_acc_with_an_assertion;;
- : bool = true
#

Pablito: Yay.

Bong-sun: Now let’s see:

let fac_acc' n =
  let () = assert (n >= 0) in
  let rec visit i a =
    if i = 0
    then a
    else let i' = pred i
         in visit i' ((n - i') * a)
     in visit n 1;;

Halcyon: Checking:

# test_fac fac_acc';;
- : bool = true
#

Pablito: Wait. <clickety clickety clickety click>:

# traced_fac_acc' 5;;
visit 5 1 ->
visit 4 1 ->
visit 3 2 ->
visit 2 6 ->
visit 1 24 ->
visit 0 120 ->
visit 5 1 <- 120
- : int = 120
#

Pablito: I see.

Bong-sun: Right. Now the accumulator is enumerating the rising Factorial numbers, and we can verify that with an assertion:

let fac_acc'_with_an_assertion n =
  let () = assert (n >= 0) in
  let rec visit i a =
    let () = assert (a = fac (n - i)) in
    if i = 0
    then a
    else let i' = pred i
         in visit i' ((n - i') * a)
     in visit n 1;;

Halcyon: Checking:

# test_fac fac_acc'_with_an_assertion;;
- : bool = true
#

Sets as lists, revisited

As an unashamed excuse for writing structurally recursive functions over lists using an accumulator, let us revisit the representation of sets as the list of their elements (without repetition), since the order of the elements does not matter.

Exercise 07

Re-implement set union (Exercise 12 in the lecture note about representing sets as lists), but this time using an accumulator.

Verify that it passes the unit tests.

Solution for Exercise 07

We had defined set union by induction on its first argument:

let set_union e1s_given e2s_given =
  let rec visit e1s =
    match e1s with
    | [] ->
       e2s_given
    | e1 :: e1s' ->
       if belongs_to e1 e2s_given
       then visit e1s'
       else e1 :: (visit e1s')
  in visit e1s_given;;

Rather than waiting for visit to return to construct the result, we can construct the result as we go using an accumulator:

let set_union_acc e1s_given e2s_given =
  let rec visit e1s a =
    match e1s with
    | [] ->
       a
    | e1 :: e1s' ->
       if belongs_to e1 e2s_given
       then visit e1s' a
       else visit e1s' (e1 :: a)
  in visit e1s_given e2s_given;;

or equivalently, commuting the conditional expression and the application:

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 es2_given;;

Traced versions of these functions (defined in the resource file for the present lecture note) illustrate the two constructions of the result:

  1. Consider the union of two disjoint sets:

    # traced_set_union [1; 2; 3; 4; 5] [6; 7; 8; 9];;
    visit [1; 2; 3; 4; 5] ->
      visit [2; 3; 4; 5] ->
        visit [3; 4; 5] ->
          visit [4; 5] ->
            visit [5] ->
              visit [] ->
              visit [] <- [6; 7; 8; 9]
            visit [5] <- [5; 6; 7; 8; 9]
          visit [4; 5] <- [4; 5; 6; 7; 8; 9]
        visit [3; 4; 5] <- [3; 4; 5; 6; 7; 8; 9]
      visit [2; 3; 4; 5] <- [2; 3; 4; 5; 6; 7; 8; 9]
    visit [1; 2; 3; 4; 5] <- [1; 2; 3; 4; 5; 6; 7; 8; 9]
    - : int list = [1; 2; 3; 4; 5; 6; 7; 8; 9]
    # traced_set_union_acc [1; 2; 3; 4; 5] [6; 7; 8; 9];;
    visit [1; 2; 3; 4; 5] [6; 7; 8; 9] ->
    visit [2; 3; 4; 5] [1; 6; 7; 8; 9] ->
    visit [3; 4; 5] [2; 1; 6; 7; 8; 9] ->
    visit [4; 5] [3; 2; 1; 6; 7; 8; 9] ->
    visit [5] [4; 3; 2; 1; 6; 7; 8; 9] ->
    visit [] [5; 4; 3; 2; 1; 6; 7; 8; 9] ->
    visit [1; 2; 3; 4; 5] [6; 7; 8; 9; 10] <- [5; 4; 3; 2; 1; 6; 7; 8; 9; 10]
    - : int list = [5; 4; 3; 2; 1; 6; 7; 8; 9]
    #
    

    The cardinality of the first set being 5, in both cases, visit is invoked 6 times:

    • since the belongs_to test fails every time, all the calls to visit are non-tail calls; so after the initial call, 5 calls (and 5 returns) take place for set_union before the final return; and
    • after the initial call, 5 tail calls (and 0 returns) take place for set_union_acc before the final return.
  2. Consider the union of the same two sets:

    # traced_set_union [1; 2; 3; 4; 5] [1; 2; 3; 4; 5];;
    visit [1; 2; 3; 4; 5] ->
    visit [2; 3; 4; 5] ->
    visit [3; 4; 5] ->
    visit [4; 5] ->
    visit [5] ->
    visit [] ->
    visit [1; 2; 3; 4; 5] <- [1; 2; 3; 4; 5]
    - : int list = [1; 2; 3; 4; 5]
    # traced_set_union_acc [1; 2; 3; 4; 5] [1; 2; 3; 4; 5];;
    visit [1; 2; 3; 4; 5] [1; 2; 3; 4; 5] ->
    visit [2; 3; 4; 5] [1; 2; 3; 4; 5] ->
    visit [3; 4; 5] [1; 2; 3; 4; 5] ->
    visit [4; 5] [1; 2; 3; 4; 5] ->
    visit [5] [1; 2; 3; 4; 5] ->
    visit [] [1; 2; 3; 4; 5] ->
    visit [1; 2; 3; 4; 5] [1; 2; 3; 4; 5] <- [1; 2; 3; 4; 5]
    - : int list = [1; 2; 3; 4; 5]
    #
    

    The cardinality of the first set being 5, in both cases, visit is also invoked 6 times:

    • since the belongs_to test succeeds every time, all the calls to visit are tail calls; so after the initial call, 5 tail calls (and 0 returns) take place for set_union; and
    • after the initial call, 5 tail calls (and 0 returns) take place for set_union_acc before the final return.
  3. Consider the union of two sets where the first elements in the list representing the first set occur in the second set but not the remaining elements:

    # traced_set_union_acc [1; 2; 3; 4; 5; 11; 12; 13; 14]
                           [1; 2; 3; 4; 5;                21; 22];;
    visit [1; 2; 3; 4; 5; 11; 12; 13; 14] [1; 2; 3; 4; 5; 21; 22] ->
    visit [2; 3; 4; 5; 11; 12; 13; 14] [1; 2; 3; 4; 5; 21; 22] ->
    visit [3; 4; 5; 11; 12; 13; 14] [1; 2; 3; 4; 5; 21; 22] ->
    visit [4; 5; 11; 12; 13; 14] [1; 2; 3; 4; 5; 21; 22] ->
    visit [5; 11; 12; 13; 14] [1; 2; 3; 4; 5; 21; 22] ->
    visit [11; 12; 13; 14] [1; 2; 3; 4; 5; 21; 22] ->
    visit [12; 13; 14] [11; 1; 2; 3; 4; 5; 21; 22] ->
    visit [13; 14] [12; 11; 1; 2; 3; 4; 5; 21; 22] ->
    visit [14] [13; 12; 11; 1; 2; 3; 4; 5; 21; 22] ->
    visit [] [14; 13; 12; 11; 1; 2; 3; 4; 5; 21; 22] ->
    visit [1; 2; 3; 4; 5; 11; 12; 13; 14] [1; 2; 3; 4; 5; 21; 22] <- [14; 13; 12; 11; 1; 2; 3; 4; 5; 21; 22]
    - : int list = [14; 13; 12; 11; 1; 2; 3; 4; 5; 21; 22]
    # traced_set_union [1; 2; 3; 4; 5; 11; 12; 13; 14]
                       [1; 2; 3; 4; 5;                21; 22];;
    visit [1; 2; 3; 4; 5; 11; 12; 13; 14] ->
    visit [2; 3; 4; 5; 11; 12; 13; 14] ->
    visit [3; 4; 5; 11; 12; 13; 14] ->
    visit [4; 5; 11; 12; 13; 14] ->
    visit [5; 11; 12; 13; 14] ->
    visit [11; 12; 13; 14] ->
      visit [12; 13; 14] ->
        visit [13; 14] ->
          visit [14] ->
            visit [] ->
            visit [] <- [1; 2; 3; 4; 5; 21; 22]
          visit [14] <- [14; 1; 2; 3; 4; 5; 21; 22]
        visit [13; 14] <- [13; 14; 1; 2; 3; 4; 5; 21; 22]
      visit [12; 13; 14] <- [12; 13; 14; 1; 2; 3; 4; 5; 21; 22]
    visit [1; 2; 3; 4; 5; 11; 12; 13; 14] <- [11; 12; 13; 14; 1; 2; 3; 4; 5; 21; 22]
    - : int list = [11; 12; 13; 14; 1; 2; 3; 4; 5; 21; 22]
    #
    

    The cardinality of the first set being 9, visit is invoked 10 times:

    • after the initial call, 9 tail calls (and 0 returns) take place for set_union_acc before the final return,
    • after the initial call, 5 tail calls (and 0 returns) take place in set_union since the first 5 elements occur in the second set; then 4 non-tails calls (and 4 returns, subsequently) take place before the final return, since the last 4 elements do not occur in the second set.
  4. Consider the union of two sets where the first elements in the list representing the first set do not occur in the second set:

    # traced_set_union_acc [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11]
                                       [5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15];;
    visit [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11] [5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [2; 3; 4; 5; 6; 7; 8; 9; 10; 11] [1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [3; 4; 5; 6; 7; 8; 9; 10; 11] [2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [4; 5; 6; 7; 8; 9; 10; 11] [3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [5; 6; 7; 8; 9; 10; 11] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [6; 7; 8; 9; 10; 11] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [7; 8; 9; 10; 11] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [8; 9; 10; 11] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [9; 10; 11] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [10; 11] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [11] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [] [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] ->
    visit [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11] [5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15] <- [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
    - : int list = [4; 3; 2; 1; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
    # traced_set_union [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11]
                                   [5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15];;
    visit [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11] ->
      visit [2; 3; 4; 5; 6; 7; 8; 9; 10; 11] ->
        visit [3; 4; 5; 6; 7; 8; 9; 10; 11] ->
          visit [4; 5; 6; 7; 8; 9; 10; 11] ->
            visit [5; 6; 7; 8; 9; 10; 11] ->
            visit [6; 7; 8; 9; 10; 11] ->
            visit [7; 8; 9; 10; 11] ->
            visit [8; 9; 10; 11] ->
            visit [9; 10; 11] ->
            visit [10; 11] ->
            visit [11] ->
            visit [] ->
            visit [5; 6; 7; 8; 9; 10; 11] <- [5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
          visit [4; 5; 6; 7; 8; 9; 10; 11] <- [4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
        visit [3; 4; 5; 6; 7; 8; 9; 10; 11] <- [3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
      visit [2; 3; 4; 5; 6; 7; 8; 9; 10; 11] <- [2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
    visit [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11] <- [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
    - : int list = [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15]
    #
    

    The cardinality of the first set being 11, visit is invoked 12 times:

    • after the initial call, 11 tail calls (and 0 returns) take place for set_union_acc before the final return;
    • after the initial call, 4 non-tail calls (and 4 returns, eventually) take place in set_union since the first 4 elements of the first set do not occur in the second set, and then 7 tail calls (and 0 returns) take place in set_union since the remaining 7 elements occur in the second set; then the 4 returns take place before the final return.

Food for thought:

  • In the last two examples above, why do the results of set_union and set_union_acc differ?
  • Does this difference matter?

Exercise 08

Re-implement set intersection (Exercise 14 in the lecture note about representing sets as lists), but this time using an accumulator.

Verify that it passes the unit tests.

Exercise 09

Re-implement set difference (Exercise 17 in the lecture note about representing sets as lists), but this time using an accumulator.

Verify that it passes the unit tests.

Exercise 10

Re-implement symmetric set difference (Exercise 20 in the lecture note about representing sets as lists), but this time using an accumulator.

Verify that it passes the unit tests.

Exercise 11

The goal of this exercise is to study the interplay between non-tail recursion and accumulators.

  1. Consider the following mixed OCaml function:

    let mixed vs_given =
      let rec visit vs a =
        match vs with
        | [] ->
           a
        | v :: vs' ->
           v :: visit vs' (v :: a)
      in visit vs_given [];;
    

    What does this OCaml function compute?

  2. Consider the following other mixed OCaml function:

    let mixed_too vs_given m =
      let rec visit vs a =
        match vs with
        | [] ->
           m :: a
        | v :: vs' ->
           v :: visit vs' (v :: a)
      in visit vs_given [];;
    

    What does this OCaml function compute?

Resources

Version

Added the interlude about the rise and fall of factorial numbers [18 Mar 2023]

Created [13 Oct 2022]