The functional abstraction and instantiation of tail-recursive functions that use an accumulator

The goal of this lecture note is to demonstrate how nat_fold_left and list_fold_left abstract the pattern of tail-recursive functions that use an accumulator for Peano numbers and for lists.

Resources

• The .v file for the present lecture note (latest version: 12 Apr 2024).

Example: the addition function that adds its first argument to its second

Let us revisit the tail-recursive addition function, which is defined recursively over its first argument and uses its second as an accumulator:

Definition tr_add (n m : nat) : nat :=
  let fix visit i a :=
    match i with
      O =>
      a
    | S i' =>
      visit i' (S a)
    end
  in visit n m.

Example: the power function that exponentiates its first argument with its second

Let us revisit the tail-recursive power function, which is defined recursively over its second argument and uses an accumulator:

Definition tr_power (x n : nat) : nat :=
  let fix visit i a :=
    match i with
      O =>
      a
    | S n' =>
      visit n' (x * a)
    end
  in visit n 1.

The common pattern

The two tail-recursive functions above share a common pattern:

Definition ... (n : nat) ... : ... :=
  let fix visit i a :=
    match i with
      O =>
      a
    | S n' =>
      visit n' (... a ...)
    end
  in visit n ... .

Indeed,

• the first lines of these definitions are Definition tr_add (n m : nat) : nat := and Definition tr_power (x n : nat) : nat, which are instances of Definition ... (n : nat) ... :=;
• in the initial tail-calls to visit, the second arguments are m and 1; and
• in the induction step, the new accumulators in the tail-recursive calls to visit are S a and x * a.

Functional abstraction of the common pattern

So,

• giving a name to the functional abstraction – nat_fold_left,
• naming the accumulator in the initial call – zero_case, and
• naming a function that maps the current accumulator to a new accumulator – succ_case,

we obtain the following implementation:

Definition nat_fold_left (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
  let fix visit i a :=
    match i with
      O =>
      a
    | S n' =>
      visit n' (succ_case a)
    end
  in visit n zero_case.

Instantiating the abstraction towards the addition function

Then, we can

• supply the type of the result of nat_fold_left with the type of the result of tr_add,
• supply m as the initial accumulator, and
• supply fun a => S a as the function to map the current accumulator to a new accumulator,

to obtain the following defition of the addition function as an instance of nat_fold_left:

Definition tr_add_left (n m : nat) : nat :=
  nat_fold_left
    nat
    m
    (fun ih => S ih)
    n.

Instantiating the abstraction towards the power function

Likewise, we can

• supply the type of the result of nat_fold_left with the type of the result of tr_power,
• supply 1 as the initial accumulator, and
• supply fun a => x * a as the function to map the current accumulator to a new accumulator,

to obtain the following defition of the power function as an instance of nat_fold_left:

Definition tr_power_left (x n : nat) : nat :=
  nat_fold_left
    nat
    1
    (fun ih => x * ih)
    n.

Resources

• The .v file for the present lecture note (latest version: 12 Apr 2024).

Version

Updated [15 Apr 2024]

Created [12 Apr 2024]