Primitive recursion

Any function that is expressible as an instance of nat_fold_right is said to be “primitive iterative”. There, the induction-step parameter (i.e., succ_case) is applied to the result of the recursive call over a smaller natural number. If the induction-step parameter is also applied to this smaller natural number, then the pattern is that of “primitive recursion”:

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

Resources

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

Version

Created [12 Apr 2024]