Recursor

Stream: new members

[Brandon Brown]

I previously asked a question on this and thought I got it but on second look, I still don't get it. The recursor on enumerated types makes sense because it doesn't involve recursion, it's just making sure you have a C n for all enumerated n. But for the simplest recursive example using the natural numbers I don't understand where the recursion is happening. Trying to learn lean is my first exposure to lambda calculus let alone dependent type theory so it's taking awhile for my imperative-style brain to figure this stuff out.

/-
nat.rec_on :
Π {C : nat → Sort u_1} (n : nat), C nat.zero → (Π (a : nat), C a → C (nat.succ a)) → C n
-/
def add (n m : nat) : nat :=
nat.rec_on n m (λ n z, nat.succ z)

I understand that we are recursing just over n and that we return m if n = 0, which is the first half of the recursor formula. The second part is a lambda function that I'm not quite understanding.
So take n = 3, m = 1 which is n = succ succ succ zero, m = succ zero
if I try add n m I get the right answer succ succ succ succ zero but I want to understand exactly what's going on.

So add n m will check if n = zero which it is not, so it can't just return m so we enter the lambda function which has two bound variables. The which are (a : nat) and C a I guess, in this we've labeled them n and z. Where are these coming from? And where is the recursion happening?

[Kevin Buzzard]

Why don't you look at an easier example, such as a one-variable example?

[Kevin Buzzard]

Try to define the function which sends n to 2^n using nat.rec_on and then evaluate it with #eval to see if you got it right

[Kevin Buzzard]

This stuff is difficult, it took me a while to get on top of it.

[Kevin Buzzard]

C a is nat

[Kevin Buzzard]

add (succ d) m is by definition succ (add d m)

[Kevin Buzzard]

example (d m : ℕ) : add (succ d) m = succ (add d m) := rfl

[Kevin Buzzard]

add (succ d) m is by definition the value that the function (λ n z, nat.succ z) takes when n=d and z=add d m

[Kevin Buzzard]

and add 0 m is by definition m

[Kevin Buzzard]

In general if you are defining a function $f$ by recursion on the naturals, then $f(n+1)$ is allowed to depend on $n$ and $f(n)$ (which is called z in this case)

[Brandon Brown]

So in the lambda (λ n z, nat.succ z) n corresponds to the input n and z corresponds to f(n) (or add n m in this case) ?

[Brandon Brown]

I will try the one-variable case haha

[Bryan Gin-ge Chen]

I remember this taking a while to click for me as well. Looking at some other sources on type theory might (or might not) help (I guess it depends on your tastes). For me, I got a lot out of the first chapter of the HoTT book.

[Kevin Buzzard]

In general if you're defining $f:\mathbb{N}\to X$ where $X$ is anything, then $C$ is the constant function sending every natural to $X$, and nat.rec_on takes three explicit inputs, first n, then the value of $f(0)$, and then the rule which given $d$ and $f(d)$ tells you what $f(d+1)$ is, and then it outputs what $f(n)$ is.

[Brandon Brown]

open nat
def expon2 (n : ℕ) : ℕ :=
nat.rec_on n (succ zero) (λ nminus1 fn, 2 * fn )

def expon2' : ℕ → ℕ
| zero := 1
| (succ n) := 2 * (expon2' n)

The second style makes a lot more sense

[Kenny Lau]

they are equal to me

[Brandon Brown]

the self-referential aspect is obvious in the second style

[Kenny Lau]

treat it as tail call recursion converted to iteration if it makes you happier