Before we define recursors, let's first introduce the idea of an inductive type. We'll do this by examining how lean defines natural numbers.

    inductive Nat where
    | zero : Nat
    | succ (n : Nat) : Nat
  

Before we define recursors, let's first introduce the idea of an inductive type. We'll do this by examining how lean defines natural numbers.

    inductive Nat where
    | zero : Nat
    | succ (n : Nat) : Nat
  

The idea here being that we can construct natural numbers by either using the constructor zero to get 0, or by applying the constructor succ to an existing natural number to get its successor. For example, we can construct 3 as follows:

    def three : Nat := Nat.succ (Nat.succ (Nat.succ Nat.zero))
  

We can equivalently express this definition using the type formation and term introduction rules:

While this explanation for inductive types usually gives most people I think enough intuition to understand the basic notions of how to use them to construct something like natural numbers, I think it kind of misses the deeper idea of what an inductive type and by extension a recursor really is. To attempt to explain this we'll take a look into some categorical semantics behind inductive types.

While at first this definition seems a bit needlessly abstract, it actually captures what the inductive type of natural numbers really is. The basic thing to recognize is that the two morphisms (just think of them as functions for now) in reality don't have anything to do with natural numbers directly. Instead, they act as a kind of blueprint for how we can use the properties or constraints of natural numbers to make anything. Here on a high level we can describe the two functions / constructors as follows:

• \(0 : 1 \to \mathbb {N}\) - The represents the abstract idea of having some starting point or base case. Within natural numbers this is represented by 0, but in reality it denotes an abstract concept of having a starting point.
• \(s : \mathbb {N} \to \mathbb {N}\) - This represents the abstract idea of being able to build upon existing things to create new things. Within natural numbers this is represented by the successor function.

Now this might quite fairly still seem a bit confusing and abstract. How can we use properties to make anything?. To describe this more formally lets constrain ourselves to the category of sets, \(\mathbf {Set}\). If you are unfamiliar with category theory it's sufficient to think of this as just a collection of all kinds of sets and functions between them.

So in plain English what this is saying is that given any set \(X\) where we have some starting point \(x \in X\) and some way of building upon existing elements of \(X\) (the function \(f : X \to X\)), we can use the properties of natural numbers to create a unique function \(u : \mathbb {N} \to X\) that maps natural numbers to elements of \(X\) in a way that respects our starting point and building function. A natural next question to have might be

But what does it mean to respect the starting point and building function?

Here I'd fast say intuitively you can just imagine construct which has some notion of a start and some way of building upon existing things. For example let's imagine the following graph:

Clearly here with have:

• Starting point: Our start here is the node \(a\).
• Building function: Our building function i.e. successor mechanism here is just following the arrows to the next node.

So our two morphisms then are:

• \(x : 1 \to X\) where \(x\) maps to \(a\).
• \(f : X \to X\) where \(f\) maps each node to the next node along the arrow. That is

  
          f(a) = b
          f(b) = c
          f(c) = d
          f(d) = e
          ...
        

Creating a minimal replica of this in Lean we could do something like:

    inductive Node where
    | start : Node           -- this will play the role of “a”
    | next  : Node → Node

    def succNode (v : Node) : Node :=
      Node. next v

    def natToNode : ℕ → Node
      | 0       => Node.start
      | n + 1   => succNode (natToNode n)
  

So we can see our function \(u : \mathbb {N} \to X\) here is represented by natToNode. Where the function maps 0 to a and each successor natural number to the next node along the arrow.

Something you might notice here is that if our natToNode function is replaced by just an identity, i.e.:

    def natToNat : ℕ → ℕ
      | 0       => 0
      | n + 1   => n + 1
  

Then we get just the natural numbers themselves as defined by their properties. This is precisely what's expressed by the earlier commutative diagram we say. The two arrows:

Are just the natural numbers defined by their properties. So in a sense the natural numbers are the most basic instantiation of their own properties. So now a fair thing to wonder is:

So what does this have to do with recursers?

Well the key insight here is that our functions natToNat and natToNode both are our recursers for the natural numbers. A recursor is just a function that allows us to define functions out of an inductive type by specifying how to handle each constructor of the inductive type. So equivalently we can express our recursor for natural numbers as:

    def recNat {C : Type} (z : C) (s : C → C) : ℕ → C
      | 0       => z
      | n + 1   => s (recNat z s n)
  

If we examine the actual type signature generated by #check Nat.rec we have:

      «Nat».rec.{u}
      {motive : ℕ → Sort u}
      (zero : motive «Nat».zero)
      (succ : (n : ℕ)
        → motive n
        → motive n.succ)
      (t : ℕ) : motive t
    

In our examples above we can see that the motive is just the type we are mapping to (either \(\mathbb {N}\) or \(X\)), the zero is our starting point (either 0 or a) and the succ is our building function (either the successor function or following the arrows). So using the recursor we can rewrite our earlier natToNat and natToNode functions as:

      def natToNat : ℕ → ℕ :=
        Nat.rec
          0                 -- | 0     => 0
          (fun n => n + 1)  -- | n + 1 => n + 1

      def natToNode : ℕ → Node :=
        Nat.rec
          Node.start            -- | 0     => Node.start
          (fun n => succNode n) -- | n + 1 => succNode (natToNode n)
    

A very important property of recursors emerges when we make the motive dependent. To elaborate on what that means let's first consider the situation of simple stepwise induction.

Something we can notice here just by superficial observation alone is that this seems to look an awful lot like the recursor for natural numbers we defined earlier. In fact, it is an application of the recursor for natural numbers for the dependent motive \(P : \mathbb {N} \to \texttt {Prop}.\). To make this a little more concrete let's define a simple property over natural numbers:

      def P (n : ℕ) : Prop := n + 0 = n
    

Now its important to note that in an abstract sense this is no different from any other function from natural numbers to some type. The dependency comes into play when we try to use the recursor i.e. the properties of naturals with this motive.

      def natToProp (n : ℕ) : (P n) :=
        Nat.rec
          (motive := P)
          (by simp [P])                    -- base case: P 0
          (fun n ih => by simp [P])        -- inductive step: P n → P (n+1)
          n
    

A few things we can observe here:

• The recursor here represents a dependent function, which is to say that the return type of the function depends on the input value. Contrasting this to the earlier case where the return type was always just \(\mathbb {N}\) or \(X\).
• Base case - Importantly here as opposed to providing a function that returns some value of type \(C\) for the base case, we instead provide a proof that the property \(P(0)\) holds.
• Inductive step - Similarly for the inductive step we provide a function that takes an arbitrary natural number \(n\) and a proof that \(P(n)\) holds (the inductive hypothesis) and returns a proof that \(P(n + 1)\) holds.

If we view this through the lens of the Curry-Howard correspondence it quite nicely illustrates how our proof here is just a program which constructs witnesses (valid proofs) for each natural number that the property \(P(n)\) holds. In the same way that our earlier recursor provided elements on the correct type, this dependent recursor provides proofs on the correct property. As this application of a recursor to a proposition represents said proposition being true for all natural numbers, we can equivalently use this within a theorem.

      theorem add_zero (n : ℕ) : n + 0 = n := natToProp n
    

As a little kind of case study I want to give an example of an inductive type (and its recursor) that most people become familiar with; in a sense; as early as primary school: the operational semantics of binary operators. We'll start by defining some basic syntax for arithmetic expressions:

      inductive BinOp where
      | add : BinOp
      | sub : BinOp
      | mul : BinOp
      | div : BinOp

      inductive Expr where
      | const : ℕ → Expr
      | binop : BinOp → Expr → Expr → Expr
    

So here we have defined a simple language of arithmetic expressions consisting of natural number constants and binary operations. This provides us with the means to construct expressions like:

      #check Expr.binop BinOp.add (Expr.const 10) (Expr.const 20)
    

If we want to actually define the semantics of how to evaluate these expressions we'll need to define a set of rewrite rules that describe how we can take an expression and reduce it to a value i.e. evaluate it. To evaluate an expression we want to traverse the expression tree and whenever we encounter a binary operation with two constant operands we want to apply the operation and replace the entire sub-expression with the resulting constant. We express this as 3 rewrite rules:

• Left Evaluation: If the left operand of a binary operation can be reduced, then we reduce it.
• Right Evaluation: If the left operand is a constant and the right operand can be reduced, then we reduce the right operand.
• Operation Evaluation: If both operands are constants, we apply the binary operation and replace the entire sub-expression with the resulting constant.

      def eval_op : BinOp → (Nat → Nat → Nat)
      | .add => Nat.add
      | .sub => Nat.sub
      | .mul => Nat.mul
      | .div => Nat.div

      inductive Step : Expr -> Expr -> Prop
      | ST_BinOp1 (op : BinOp)
          (e₁ e₁' e₂ : Expr)
          (h : Step e₁ e₁') :
          Step (Expr.binop op e₁ e₂)
               (Expr.binop op e₁' e₂)
      | ST_BinOp2 (op : BinOp)
          (v₁ : Nat)
          (e₂ e₂' : Expr)
          (h : Step e₂ e₂') :
          Step (Expr.binop op (Expr.const v₁) e₂)
               (Expr.binop op (Expr.const v₁) e₂')
      | ST_BinOpConst (op : BinOp) (v₁ v₂ : Nat) :
          Step (Expr.binop op (Expr.const v₁) (Expr.const v₂))
               (Expr.const (eval_op op v₁ v₂))
    

Since expressions can naturally require multiple evaluations steps it makes sense to define a multistep evaluation relation as the reflexive transitive closure of the single step evaluation relation defined above. This we can define as:

      abbrev MultiStep := Relation.ReflTransGen Step

      -- helper notation to express multi-step evaluation
      notation:50 e " ->ⁿ " e' =>  MultiStep e e'
    

Let's also define a small helper syntax and macro to make it easier to write arithmetic expressions:

          declare_syntax_cat arithTm

          -- atoms
          syntax num                      : arithTm
          syntax "(" arithTm ")"          : arithTm

          -- multiplicative level (higher precedence)
          syntax:70 arithTm:70 "*" arithTm:71 : arithTm
          syntax:70 arithTm:70 "/" arithTm:71 : arithTm

          -- additive level (lower precedence)
          syntax:60 arithTm:60 "+" arithTm:61 : arithTm
          syntax:60 arithTm:60 "-" arithTm:61 : arithTm

          syntax "ex{" arithTm "}" : term

          macro_rules
            -- numerals
            | `(ex{ $n:num }) =>
                `(Expr.const $n)

            -- parentheses
            | `(ex{ ($t:arithTm) }) =>
                `(ex{$t})

            -- addition
            | `(ex{ $e₁:arithTm + $e₂:arithTm }) =>
                `(Expr.binop BinOp.add (ex{$e₁}) (ex{$e₂}))

            -- subtraction
            | `(ex{ $e₁:arithTm - $e₂:arithTm }) =>
                `(Expr.binop BinOp.sub (ex{$e₁}) (ex{$e₂}))

            -- multiplication
            | `(ex{ $e₁:arithTm * $e₂:arithTm }) =>
                `(Expr.binop BinOp.mul (ex{$e₁}) (ex{$e₂}))

            -- division
            | `(ex{ $e₁:arithTm / $e₂:arithTm }) =>
                `(Expr.binop BinOp.div (ex{$e₁}) (ex{$e₂}))
        

        example : -- ((2 * 3) + 4) ->ⁿ 10
        ex{ ((2 * 3) + 4) } ->ⁿ ex{ 10 } :=
          .trans (rw_lhs (rw_const .mul 2 3)) (rw_const .add 6 4)
      

        +(lhs [op] rhs)
        |
        +-+(rw_lhs) ->ⁿ lhs' [op] rhs    (1) reduce lhs some number of steps
          |
          +-+(rw_rhs) ->ⁿ lhs [op] rhs'  (2) reduce rhs some number of steps
            |
            +- (rw_const) -> value       (3) reduce both to a constant value
      

        lemma rw_lhs (lhs_rw : lhs ->ⁿ lhs') :
          (lhs [op] rhs) ->ⁿ (lhs' [op] rhs) :=
        match lhs_rw with
        | .refl       => .refl
        | .tail S₁ S₂ => (rw_lhs S₁).tail (.ST_BinOp1 S₂)

        lemma rw_rhs (rhs_rw : rhs ->ⁿ rhs') :
          ((.const lhs) [op] rhs) ->ⁿ ((.const lhs) [op] rhs') :=
        match rhs_rw with
        | .refl       => .refl
        | .tail S₁ S₂ => (rw_rhs S₁).tail (.ST_BinOp2 S₂)

        lemma rw_const (op : BinOp) (lhs rhs : Nat) :
          ((.const lhs) [op] (.const rhs)) ->ⁿ .const (eval_op op lhs rhs) :=
        .single (.ST_BinOpConst op lhs rhs)
      

        lemma rw_rhs' (rhs_rw : rhs ->ⁿ rhs') :
          ((.const lhs) [op] rhs) ->ⁿ ((.const lhs) [op] rhs') :=
        .rec
          (refl := .refl)
          (tail := by
            intro _ _ _ hcb ih
            exact ih.tail (.ST_BinOp2 hcb)
          ) rhs_rw

        lemma rw_rhs'' (rhs_rw : rhs ->ⁿ rhs') :
          ((.const lhs) [op] rhs) ->ⁿ ((.const lhs) [op] rhs') :=
        .head_induction_on
          (refl := .refl)
          (head := by
            intro _ _ hac _ ih
            exact ih.head (.ST_BinOp2 hac)
          ) rhs_rw
      

        @[simp]
        def eval : Expr -> Nat
          | Expr.const n => n
          | Expr.binop op e₁ e₂ =>
              let v₁ := eval e₁
              let v₂ := eval e₂
              eval_op op v₁ v₂
      

        (e : Expr) : -- for any expression e
          (∃ v : Nat), -- there exists a value v
            (eval e = v) ∧ (e ->ⁿ (.const v))
            -- such that eval e = v and e reduces to the constant v
      

        theorem eval_correct (e : Expr) :
        ∃ v : Nat, (eval e = v) ∧ (e ->ⁿ (.const v)) := by
        induction e with
        | const n => exists n
        | binop op lhs rhs eval_lhs eval_rhs =>
          rcases eval_lhs with ⟨lhs_v, ⟨rhs_is_v, lhs_rw⟩⟩
          rcases eval_rhs with ⟨rhs_v, ⟨lhs_is_v, rhs_rw⟩⟩
          simp [rhs_is_v, lhs_is_v]

          exact
            (rw_lhs lhs_rw).trans (
              (rw_rhs rhs_rw).trans (
                rw_const op lhs_v rhs_v
              )
            )