The goal of this lecture note is to describe accumulators.
Consider the “copy” function over Peano numbers:
Fixpoint copy_nat (n : nat) : nat :=
match n with
O =>
O
| S n' =>
S (copy_nat n')
end.
Let us visualize its successive calls and returns when copy_nat is applied to 3, tagging the calls with --> and the returns with <-- followed by what is returned:
copy_nat (S (S (S O))) -->
copy_nat (S (S O)) -->
copy_nat (S O) -->
copy_nat O -->
copy_nat O <-- 0
copy_nat (S O) <-- 1
copy_nat (S (S O)) <-- 2
copy_nat (S (S (S O))) <-- 3
Note how the indentation makes it clear that the recursive calls are nested: for each recursive call, there is a corresponding return later on. Graphically:
copy_nat (S (S (S O))) -->
+-------------------------
| copy_nat (S (S O)) -->
| +---------------------
| | copy_nat (S O) -->
| | +-----------------
| | | copy_nat O -->
| | | copy_nat O <-- 0
| | +-----------------
| | copy_nat (S O) <-- 1
| +---------------------
| copy_nat (S (S O)) <-- 2
+-------------------------
copy_nat (S (S (S O))) <-- 3
Now consider the exponentiation function:
Fixpoint power (x n : nat) : nat :=
match n with
O =>
1
| S n' =>
x * (power x n')
end.
Let us visualize its successive calls and returns when power is applied to 10 and 3, tagging the calls with --> and the returns with <-- followed by what is returned:
power 10 (S (S (S O))) -->
power 10 (S (S O)) -->
power 10 (S O) -->
power 10 O -->
power 10 O <-- 1
power 10 (S O) <-- 10
power 10 (S (S O)) <-- 100
power 10 (S (S (S O))) <-- 1000
Again, note how the indentation makes it clear that the recursive calls are nested: for each recursive call, there is a corresponding return later on, and so there are as many calls as there are returns.
The point of this chapter is to relocate computations from return time to call time, which often – but not always – has the effect of transforming the calls into tail calls, i.e., the last calls to be performed in the body of each function.
What happens to the result of a recursive call? For copy_nat, this result is the argument of S and for power, this result is the multiplicand in a multiplication where the multiplicator is x. S is applied at return time, i.e., after copy_nat returns and the multiplication takes place at return time, i.e., after power return.
But we don’t need to apply S and perform the multiplication after the functions return, as long as we perform this application and this multiplication as many times as the functions returns. For example, if we equip copy_nat and power with an extra argument that is initialized with that they return in their base case, we can perform this application and this multiplication at call time, i.e., before the equipped version of copy_nat and power are applied, and accumulate the result of this application and this multiplication for subsequent use. Here, since there is nothing to do anymore at return time, the calls of the equipped version of copy_nat and power become tail calls.
Here is such an equipped (or again, “accumulator-based”) version of the “copy” function over Peano numbers:
Fixpoint copy_nat_acc (n a : nat) : nat :=
match n with
O =>
a
| S n' =>
copy_nat_acc n' (S a)
end.
Definition copy_nat_alt (n : nat) : nat :=
copy_nat_acc n 0.
The main function, copy_nat_alt, tail calls an auxiliary recursive function, copy_nat_acc, with its argument and with what copy_nat returns in the base case. The second argument of copy_nat_alt is said to be an “accumulator”. The auxiliary function
Let us visualize its successive calls and returns when copy_nat_alt is applied to 3, tagging the calls (which are now tail calls) with --> and the return with <-- followed by what is returned:
copy_nat_alt (S (S (S O))) -->
copy_nat_acc (S (S (S O))) O -->
copy_nat_acc (S (S O)) 1 -->
copy_nat_acc (S O) 2 -->
copy_nat_acc O 3 -->
copy_nat_acc O 3 <-- 3
Observe how S is now applied at (tail-) call time, and note how the indentation makes it clear that the tail calls are not nested: for all the tail calls, there is one return eventually.
Likewise, here is an accumulator-based version of the exponentiation function:
Fixpoint power_acc (x n a : nat) : nat :=
match n with
O =>
a
| S n' =>
power_acc x n' (x * a)
end.
Definition power_alt (x n : nat) : nat :=
power_acc x n 1.
The main function, power_alt, tail calls an auxiliary recursive function, power_acc, with its argument and with what power returns in the base case. The auxiliary function
Let us visualize its successive tail calls and return when power is applied to 10 and 3, tagging the tail calls with --> and not indenting them and tagging the return with <-- followed by what is returned:
power_alt 10 (S (S (S O))) -->
power_acc 10 (S (S (S O))) 1 -->
power_acc 10 (S (S O)) 10 -->
power_acc 10 (S O) 100 -->
power_acc 10 O 1000 -->
power_acc 10 O 1000 <-- 1000
Again, observe how the multiplication now takes place at (tail-) call time, and note how the indentation makes it clear that the tail calls are not nested: for all the tail calls, there is one return eventually.
Informally, the two alternative versions are correct because they carry out the same computations as the original versions, albeit not in the same order: at tail-call time, simultaneously, instead of at call time and then at return time.
Soon, we will formalize this intuition with a theorem, which we shall prove by induction over n.
Consider the ordinary factorial function:
Fixpoint fac (n : nat) : nat :=
match n with
O =>
1
| S n' =>
S n' * fac n'
end.
This case is more complicated because what happens at return time depends on the argument of the recursive call, which it did not for copy_nat (it was S ...) and for power (it was x * ...). Here, it is S n' * ....
Let us visualize its successive calls and returns when fac is applied to 3, tagging the calls with --> and the returns with <-- followed by what is returned:
fac (S (S (S O))) -->
fac (S (S O)) -->
fac (S O) -->
fac O -->
fac O <-- 1
fac (S O) <-- 1
fac (S (S O)) <-- 2
fac (S (S (S O))) <-- 6
As before, note how the indentation makes it clear that the recursive calls are nested: for each recursive call, there is a corresponding return later on.
Question: What happens to the result of the recursive call fac i?
Answer: It is the multiplicand of a multiplication whose multiplicator is S i.
We can anticipate this multiplication from return time to call time by using an accumulator:
Fixpoint fac_acc (n a : nat) : nat :=
match n with
O =>
a
| S n' =>
fac_acc n' (S n' * a)
end.
Definition fac_alt (n : nat) : nat :=
fac_acc n 1.
Let us visualize its successive tail calls and return when fac_alt is applied to 3, tagging the tail calls with --> and not indenting them and tagging the return with <-- followed by what is returned:
fac_alt (S (S (S O))) -->
fac_acc (S (S (S O))) 1 -->
fac_acc (S (S O)) 3 -->
fac_acc (S O) 6 -->
fac_acc O 6 -->
fac_acc O 6 <-- 6
Observe how the order of multiplications has changed. Applying the recursive factorial function to 3 computes 3 * (2 * (1 * 1)) outside in whereas applying the tail-recursive factorial function to 3 computes 1 * (2 * (3 * 1)) inside out. So the same computations take place, albeit not in the same order.
Informally, the alternative version is correct because multiplication is associative and commutative.
Soon, we will formalize this intuition with a theorem, which we shall prove by induction over n.
Implement an accumulator-based version of the multiplication function. Informally, is your implementation correct? Why?
Implement a recursive function over a Peano number such that the operation carried out on the result of the recursive call is not associative and not commutative. (For example, this operation could be the subtraction function.)
Can you implement an accumulator-based version of your recursive function? If your implementation is correct, informally explain why. If your implementation is incorrect, give a counter-example that illustrates this incorrectness.
Let us revisit binary trees of natural numbers with payloads in their leaves, renaming their constructors into a shorter version:
Inductive binary_tree_nat : Type :=
L : nat -> binary_tree_nat
| N : binary_tree_nat -> binary_tree_nat -> binary_tree_nat.
Consider the function that computes the height of a given tree:
Fixpoint height (t : binary_tree_nat) : nat :=
match t with
L n =>
0
| N t1 t2 =>
S (max (height t1) (height t2))
end.
Let us visualize its successive calls and returns when height is applied to N (N (L 1) (L 2)) (N (L 3) (L 4)), traversing this tree from left to right and tagging the tail calls with --> and not indenting them and tagging the return with <-- followed by what is returned:
height (N (N (L 1) (L 2)) (N (L 3) (L 4))) -->
height (N (L 1) (L 2)) -->
height (L 1) -->
height (L 1) <-- 0
height (L 2) -->
height (L 2) <-- 0
height (N (L 1) (L 2)) <-- 1
height (N (L 3) (L 4)) -->
height (L 3) -->
height (L 3) <-- 0
height (L 4) -->
height (L 4) <-- 0
height (N (L 3) (L 4)) <-- 1
height (N (N (L 1) (L 2)) (N (L 3) (L 4))) <-- 2
Here is another visualization when height is applied to N (N (L 1) (L 2)) (N (L 3) (L 4)):
height (N (N (L 0) (N (L 1) (L 2))) (N (N (L 3) (L 4)) (N (N (L 5) (L 6)) (L 7)))) -->
height (N (L 0) (N (L 1) (L 2))) -->
height (L 0) -->
height (L 0) <-- 0
height (N (L 1) (L 2)) -->
height (L 1) -->
height (L 1) <-- 0
height (L 2) -->
height (L 2) <-- 0
height (N (L 1) (L 2)) <-- 1
height (N (L 0) (N (L 1) (L 2))) <-- 2
height (N (N (L 3) (L 4)) (N (N (L 5) (L 6)) (L 7))) -->
height (N (L 3) (L 4)) -->
height (L 3) -->
height (L 3) <-- 0
height (L 4) -->
height (L 4) <-- 0
height (N (L 3) (L 4)) <-- 1
height (N (N (L 5) (L 6)) (L 7)) -->
height (N (L 5) (L 6)) -->
height (L 5) -->
height (L 5) <-- 0
height (L 6) -->
height (L 6) <-- 0
height (N (L 5) (L 6)) <-- 1
height (L 7) -->
height (L 7) <-- 0
height (N (N (L 5) (L 6)) (L 7)) <-- 2
height (N (N (L 3) (L 4)) (N (N (L 5) (L 6)) (L 7))) <-- 3
height (N (N (L 0) (N (L 1) (L 2))) (N (N (L 3) (L 4)) (N (N (L 5) (L 6)) (L 7)))) --> 4
And here is a last visualization when height is applied to a “flat” tree:
height (N (L 0) (N (L 1) (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6))))))) -->
height (L 0) -->
height (L 0) <-- 0
height (N (L 1) (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6)))))) -->
height (L 1) -->
height (L 1) <-- 0
height (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6))))) -->
height (L 2) -->
height (L 2) <-- 0
height (N (L 3) (N (L 4) (N (L 5) (L 6)))) -->
height (L 3) -->
height (L 3) <-- 0
height (N (L 4) (N (L 5) (L 6))) -->
height (L 4) -->
height (L 4) <-- 0
height (N (L 5) (L 6)) -->
height (L 5) -->
height (L 5) <-- 0
height (L 6) -->
height (L 6) <-- 0
height (N (L 5) (L 6)) <-- 1
height (N (L 4) (N (L 5) (L 6))) <-- 2
height (N (L 3) (N (L 4) (N (L 5) (L 6)))) <-- 3
height (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6))))) <-- 4
height (N (L 1) (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6)))))) <-- 5
height (N (L 0) (N (L 1) (N (L 2) (N (L 3) (N (L 4) (N (L 5) (L 6))))))) <-- 6
In all cases, the visualization provides a homomorphic rendition of the structure of the tree.
Question: What happens to the results of the two recursive calls?
Answer: Their max is computed and then incremented.
The max depends on the specific results of the two recursive calls, but not the increment. So as earlier for Peano numbers, we can anticipate this increment from return time to call time by using an accumulator:
Fixpoint height_acc (t : binary_tree_nat) (a : nat) : nat :=
match t with
L n =>
a
| N t1 t2 =>
max (height_acc t1 (S a)) (height_acc t2 (S a))
end.
Definition height_alt (t : binary_tree_nat) : nat :=
height_acc t 0.
Let us visualize its successive calls and returns when height_alt is applied to a “flat” tree:
height_alt (N (L 0) (N (L 1) (N (L 2) (L 3)))) -->
height_acc (N (L 0) (N (L 1) (N (L 2) (L 3)))) 0 -->
height_acc (L 0) 1 -->
height_acc (L 0) 1 <-- 1
height_acc (N (L 1) (N (L 2) (L 3))) 1 -->
height_acc (L 1) 2 -->
height_acc (L 1) 2 <-- 2
height_acc (N (L 2) (L 3)) 2 -->
height_acc (L 2) 3 -->
height_acc (L 2) 3 <-- 3
height_acc (L 3) 3 -->
height_acc (L 3) 3 <-- 3
height_acc (N (L 2) (L 3)) 2 <-- 3
height_acc (N (L 1) (N (L 2) (L 3))) 1 <-- 3
height_acc (N (L 0) (N (L 1) (N (L 2) (L 3)))) 0 <-- 3
Observations:
Anton: Bummer that we can’t traverse a binary tree tail recursively.
Alfrothul: Well, maybe the glass is actually half full.
Anton: Half full now? How?
Alfrothul: Well, whether we traverse the tree from left to right or from right to left, in each node, the first subtree needs to be traversed with a recursive call.
Anton: Well, both subtrees need to be traversed, look:
Fixpoint number_of_leaves (t : binary_tree_nat) : nat :=
match t with
L _ =>
1
| N t1 t2 =>
number_of_leaves t1 + number_of_leaves t2
end.
Alfrothul: Yes, yes, but once we traversed either subtree with a recursive call, maybe we could traverse the second subtree with a tail-recursive call if somehow we use an accumulator. Wishful thinking, I know, but why not entertain this thought.
Anton: Harrumph.
Alfrothul: Consider the recursive calls to compute the number of leaves of a given tree:
| N t1 t2 =>
number_of_leaves t1 + number_of_leaves t2
Anton: OK?
Alfrothul: Assume that somehow we have an accumulator. Then a recursive call on either subtree and the accumulator would give a new accumulator.
Anton: Oh. And then the recursive call on the other subtree and the resulting accumulator would be a tail call.
Alfrothul: Precisely. Assume that we have such an accumulator-based function:
| N t1 t2 =>
number_of_leaves_acc t2 (number_of_leaves_acc t1 a)
Anton: OK, the tree is still traversed from left to right since t1 is first traversed with the current accumulator, using a non-tail call.
Alfrothul: Right. The result is a new accumulator, and then t2 is traversed with this new accumulator, using a tail call.
Pablito (diligent): So we are looking at something like the following:
Fixpoint number_of_leaves_acc (t : binary_tree_nat) (a : nat) : nat :=
match t with
L _ =>
???
| N t1 t2 =>
number_of_leaves_acc t2 (number_of_leaves_acc t1 a)
end.
Definition number_of_leaves_alt (t : binary_tree_nat) : nat :=
number_of_leaves_acc t 0.
Alfrothul: Right. At the outset, the alternative function that computes the number of leaves in a tree calls the accumulator-based function with an initial accumulator which is 0.
Anton: And then the accumulator-based function does its thing.
Dana: It does its thing in the induction step, for sure, but what about in the base case?
Pablito (helpful): That’s why I put three questions marks.
Dana: Yes, thanks for that.
Bong-sun: Let me see. In the base case, we have a leaf and we have an accumulator, so how about incrementing the accumulator?
Pablito: You mean writing S a instead of ????
Bong-sun: Yes.
Pablito: Let me try, let me try. <clickety clickety click>... OK, it is both syntactically correct and type correct. Just a sec. <clickety clickety click>... And it passes the unit tests too!
Halcyon: Wow.
Dana: I guess we will prove the soundness of this implementation sometimes soon?
Mimer (benevolently hovering in the background): Yes you will.
Alfrothul: Meanwhile how about we visualize the calls?
Anton (on a roll): Yes, let’s:
number_of_leaves_alt (N (N (L 1) (L 2)) (N (L 3) (L 4))) -->
number_of_leaves_acc (N (N (L 1) (L 2)) (N (L 3) (L 4))) 0 -->
number_of_leaves_acc (N (L 1) (L 2)) 0 -->
number_of_leaves_acc (L 1) 0 -->
number_of_leaves_acc (L 1) 0 <-- 1
number_of_leaves_acc (L 2) 1 -->
number_of_leaves_acc (L 2) 1 <-- 2
number_of_leaves_acc (N (L 3) (L 4)) 2 -->
number_of_leaves_acc (L 3) 2 -->
number_of_leaves_acc (L 3) 2 <-- 3
number_of_leaves_acc (L 4) 3 -->
number_of_leaves_acc (L 4) 3 <-- 4
Pablito: Wow.
Alfrothul: See how the call to each first subtree is a non-tail call and how the call to each second subtree is a tail call?
Dana: I guess that a tree that is completely slanted to the right...
Pablito: Slanted to the right?
Dana: Sorry. I mean a tree where all the first subtrees are leaves.
Pablito: Ah, right. Such a tree is slanted to the right. Thanks.
Dana: You are most welcome. Traversing such a tree will be done iteratively, with one tail call for every right subtree.
Bong-sun: And traversing a tree that is completely slanted to the left will be done very much recursively, with one non-tail call for every left subtree.
Alfrothul: That’s the way the cookie crumbles.
Implement a function that computes the number of nodes of a given tree, using an accumulator so that half of the calls are recursive calls and the other half are tail-recursive calls, and verify that your implementation passes your unit tests from Week 01.
Pablito: So indeed the glass is half full. We can traverse a binary tree recursively half of the time and tail recursively the other half.
Anton: That’s because we use an accumulator.
Dana (amused): If we used a continuation, the glass would be completely full.
Halcyon: Completely full?
Pablito: A continuation?
Dana: An accumulator stores the result of computations done at call time instead of at return time. A continuation is a function that stores what to do next.
Pablito: Er... OK?
Dana: So for example, rather than computing f (g x), we equip g with a continuation – a function that represents what to do with the result of g – and we tail-call this equipped version of g with this continuation: g_cps x (fun r => f r).
Pablito: Harrumph.
Dana: Initially, the continuation is the identity function:
Fixpoint number_of_nodes (t : binary_tree_nat) : nat :=
match t with
L _ =>
0
| N t1 t2 =>
S (number_of_nodes t1 + number_of_nodes t2)
end.
Fixpoint number_of_nodes_cps (t : binary_tree_nat) (k : nat -> nat) : nat :=
match t with
L _ =>
k 0
| N t1 t2 =>
number_of_nodes_cps t1 (fun n1 =>
number_of_nodes_cps t2 (fun n2 =>
k (S (n1 + n2))))
end.
Definition number_of_nodes_alt2 (t : binary_tree_nat) : nat :=
number_of_nodes_cps t (fun n => n).
Anton: OK, OK, all calls are tail calls.
Dana: In the base case, number_of_nodes_cps continues with 0 instead of returning 0, as number_of_nodes does.
Halcyon: I see.
Pablito: And it does that with a tail call to k.
Dana: Yes. And in the induction step, t1 is traversed tail recursively with a continuation that will be applied to the number of nodes in t1.
Alfrothul: And when this continuation is applied, t2 is traversed tail recursively with a continuation that will be applied to the number of nodes in t2.
Bong-sun: And when this continuation is applied, these two numbers are added and the result is incremented.
Dana: And all of that with tail calls, look:
number_of_nodes_alt2 (N (N (L 1) (L 2)) (N (L 3) (L 4))) -->
number_of_nodes_cps (N (N (L 1) (L 2)) (N (L 3) (L 4))) (fun n => n) -->
number_of_nodes_cps (N (L 1) (L 2)) (fun n1 => ...) -->
number_of_nodes_cps (L 1) (fun n1 => ...) -->
number_of_nodes_cps (L 2) (fun n2 => ...) -->
number_of_nodes_cps (N (L 3) (L 4)) (fun n2 => ...) -->
number_of_nodes_cps (L 3) (fun n1 => ...) -->
number_of_nodes_cps (L 4) (fun n2 => ...) -->
number_of_nodes_cps (L 4) (fun n2 => ...) <-- 3
Halcyon: I need a theorem...
Mimer: That’s the spirit, Halcyon. That’s the spirit!
Added explanations about copy_nat_alt and power_alt in the analysis of what happens at call time and at return time [25 Jan 2025]
Renamed the constructors of binary_tree_nat from Leaf_nat to L and from Node_nat to N, for conciseness in the traces [24 Jan 2025]
Completed [24 Jan 2025]
Created [24 Jan 2025]