## Stream: new members

### Topic: Recursor

#### Brandon Brown (Apr 28 2020 at 22:12):

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 (Apr 28 2020 at 22:13):

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

#### Kevin Buzzard (Apr 28 2020 at 22:13):

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 (Apr 28 2020 at 22:14):

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

C a is nat

#### Kevin Buzzard (Apr 28 2020 at 22:16):

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

#### Kevin Buzzard (Apr 28 2020 at 22:17):

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 (Apr 28 2020 at 22:17):

and add 0 m is by definition m

#### Kevin Buzzard (Apr 28 2020 at 22:18):

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 (Apr 28 2020 at 22:20):

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 (Apr 28 2020 at 22:22):

I will try the one-variable case haha

#### Bryan Gin-ge Chen (Apr 28 2020 at 22:25):

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 (Apr 28 2020 at 22:29):

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 (Apr 29 2020 at 00:03):

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 (Apr 29 2020 at 00:08):

they are equal to me

#### Brandon Brown (Apr 29 2020 at 00:09):

the self-referential aspect is obvious in the second style

#### Kenny Lau (Apr 29 2020 at 00:12):

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

Last updated: May 11 2021 at 00:31 UTC