The functional abstraction and instantiation of recursive functions

The goal of this lecture note is to demonstrate how nat_fold_right and list_fold_right abstract the pattern of recursive functions for Peano numbers and for lists.

For simplicity and ease of discourse, in this lecture note, all the implementations are lambda-dropped, i.e., each global main function calls a auxiliary function locally instead of globally.

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 recursive addition function, which is defined recursively over its first argument:

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

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

Let us revisit the recursive power function, which is defined recursively over its second argument:

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

The common pattern

The two recursive functions above share a common pattern:

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

Indeed,

• the first lines of these definitions are Definition r_add (n m : nat) : nat := and Definition r_power (x n : nat) : nat, which are instances of Definition ... (n : nat) ... :=;
• in the base case, the consequents in these definitions are m and 1; and
• in the induction step, the consequents in these definitions are S (visit i') and x * visit i'.

Functional abstraction of the common pattern

So,

• giving a name to the functional abstraction – nat_fold_right,
• naming the consequent in the base case – zero_case, and
• naming a function that is given the result of the recursive call (which implements the induction hypothesis) – succ_case,

we obtain the following implementation:

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

Instantiating the abstraction towards the addition function

Then, we can

• supply the type of the result of nat_fold_right with the type of the result of r_add,
• supply m as the consequent in the base case, and
• supply fun ih => S ih as the function to be applied to the result of the recursive call,

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

Definition r_add_right (n m : nat) : nat :=
  nat_fold_right
    nat
    m
    (fun ih => S ih)
    n.

This implementation passes the unit tests.

Instantiating the abstraction towards the power function

Likewise, we can

• supply the type of the result of nat_fold_right with the type of the result of r_power,
• supply 1 as the consequent in the base case, and
• supply fun ih => x * ih as the function to be applied to the result of the recursive call,

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

Definition r_power_right (x n : nat) : nat :=
  nat_fold_right
    nat
    1
    (fun ih => x * ih)
    n.

This implementation passes the unit tests.

Interlude

Pablito: But how do we know, for example, that r_add_right implements the addition function?

Halcyon (thoughtful): Because testing only proves incorrectness, not correctness.

Edsger W. Dijkstra: How true, how true.

Mimer: Prof. Dijkstra! Thanks for dropping by!

Halcyon (raffish): So we should state and prove a theorem to the effect that r_power and r_power_right are equivalent.

Pablito: Right. That’s simple to do with the lambda-lifted versions of r_power and of nat_fold_right and their associated fold-unfold lemmas.

Mimer: That’s good to hear.

Pablito: But still.

[...calculate, see the resource file (for now)...]

Resources

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

Version

Created [12 Apr 2024]