The goal of this lecture note is to illustrate the many uses of accumulators in functional programming.
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)
(* an 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) (* so much for the dramatic spillage *)
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5;;
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 countdown below is scope-sensitive, in that it uses y_init 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_init y_init =
let () = assert (x_init >= 0) in
let rec countdown x =
if x = 0
then y_init
else let x' = pred x
in let ih = countdown x'
in succ ih
in countdown x_init;;
Or again, unfolding the let-expressions since they are cosmetic:
let add_v1' x_init y_init =
let () = assert (x_init >= 0) in
let rec countdown x =
if x = 0
then y_init
else succ (countdown (pred x))
in countdown x_init;;
Both functions pass the unit test:
# test_add add_v1;;
- : bool = true
# test_add add_v1';;
- : bool = true
#
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 countdown below is scope-insensitive, in that it only uses variables 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_init y_init =
let () = assert (x_init >= 0) in
let rec countdown x y =
if x = 0
then y
else let x' = pred x
in let ih = countdown x'
in succ (ih y)
in countdown x_init y_init;;
Or again, unfolding the let-expressions:
let add_v2' x_init y_init =
let () = assert (x_init >= 0) in
let rec countdown x y =
if x = 0
then y
else succ (countdown (pred x) y)
in countdown x_init y_init;;
And lo and behold, both functions pass the unit test:
# test_add add_v2;;
- : bool = true
# test_add add_v2';;
- : bool = true
#
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_init y_init =
let () = assert (x_init >= 0) in
let rec countdown x y =
if x = 0
then y
else let x' = pred x
in let ih = countdown x'
in ih (succ y)
in countdown x_init y_init;;
Or again, unfolding the let-expressions:
let add_v3' x_init y_init =
let () = assert (x_init >= 0) in
let rec countdown x y =
if x = 0
then y
else countdown (pred x) (succ y)
in countdown x_init y_init;;
Both functions pass the unit test:
# test_add add_v3;;
- : bool = true
# test_add add_v3';;
- : bool = true
#
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_init =
let rec visit vs a =
if vs = []
then a
else visit (List.tl vs) (List.hd vs :: a)
in visit vs_init [];;
let look_Ma_no_accumulator vs_init =
let rec visit vs =
if vs = []
then []
else List.hd vs :: visit (List.tl vs)
in visit vs_init;;
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:
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_init =
let rec visit n a =
match n with
| 0 ->
a
| _ ->
let n' = pred n
in visit n' (n' :: a)
in visit n_init [];;
And it passes its unit test too:
# test_iota iota;;
- : bool = true
#
Given a non-negative integer, the following function applies both iota and atoi to it, and then add 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);;
Let us specify a relation between a given list (vs_init), its successive suffixes (vs), and the length of the corresponding prefixes (a): this relation states that adding a to the length of vs gives the length of vs_init:
base case (vs = [] and a is the length of the corresponding prefix in vs_init):
if the suffix of vs_init is the empty list, the corresponding prefix is vs_init, and therefore a is the length of vs_init
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_init
induction hypothesis: adding succ a to the length of vs’ gives the length of vs_init
therefore adding a to the length of v :: vs’ also gives the length of vs_init
The following recursive function embodies this inductive specification:
let length_acc vs_init =
let rec walk vs a =
match vs with
| [] ->
a
| v :: vs' ->
walk vs' (succ a)
in walk vs_init 0;;
Each (tail) call to walk satisfies the invariant above:
for any call walk vs a that satisfies the invariant (i.e., adding the denotation of a to the length of the denotation of vs gives the length of the denotation of vs_init, i.e., of the given list), there are two cases:
vs denotes the empty list, which has length 0:
the invariant 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 non-empty list and has length 1 + n’, for some natural number n’:
the invariant 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 invariant;
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 invariant is satisfied.
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:
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:
let fac n_init =
let () = assert (n_init >= 0) in
let rec countdown n =
if n = 0
then 1
else n * countdown (pred n)
in countdown n_init;;
let fac_acc n_init =
let () = assert (n_init >= 0) in
let rec countdown n a =
if n = 0
then a
else countdown (pred n) (n * a)
in countdown n_init 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;;
countdown 5 ->
countdown 4 ->
countdown 3 ->
countdown 2 ->
countdown 1 ->
countdown 0 ->
countdown 0 <- 1
countdown 1 <- 1
countdown 2 <- 2
countdown 3 <- 6
countdown 4 <- 24
countdown 5 <- 120
- : int = 120
# traced_fac_acc 5;;
countdown 5 1 ->
countdown 4 5 ->
countdown 3 20 ->
countdown 2 60 ->
countdown 1 120 ->
countdown 0 120 ->
countdown 5 1 <- 120
- : int = 120
#
Since the input is 5, in both cases there are 6 calls to countdown:
Food for thought:
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.
Re-implement set union (Exercise 4 in the lecture note about representing sets as lists), but this time using an accumulator.
Verify that it passes the unit tests.
We had defined set union by induction on its first argument:
let set_union e1s_init e2s_init =
let rec visit e1s =
match e1s with
| [] ->
e2s_init
| e1 :: e1s' ->
if belongs_to e1 e2s_init
then visit e1s'
else e1 :: (visit e1s')
in visit e1s_init;;
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_init e2s_init =
let rec visit e1s a =
match e1s with
| [] ->
a
| e1 :: e1s' ->
if belongs_to e1 e2s_init
then visit e1s' a
else visit e1s' (e1 :: a)
in visit e1s_init e2s_init;;
or equivalently, commuting the conditional expression and the application:
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 es2_init;;
Traced versions of these functions (defined in the resource file for the present lecture note) illustrate the two constructions of the result:
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:
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:
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:
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:
Food for thought:
Re-implement set intersection (Exercise 6 in the lecture note about representing sets as lists), but this time using an accumulator.
Verify that it passes the unit tests.
Re-implement set difference (Exercise 9 in the lecture note about representing sets as lists), but this time using an accumulator.
Verify that it passes the unit tests.
Re-implement symmetric set difference (Exercise 12 in the lecture note about representing sets as lists), but this time using an accumulator.
Verify that it passes the unit tests.
Clarified the terms “lambda-dropped” and “lambda-lifted” [05 Apr 2020]
Streamlined the unit-test functions [08 Jun 2019]
Fixed a typo in the definition of set_union_acc', thanks to Yunjeong Lee’s eagle eye [02 May 2019]
Created [18 Mar 2019]