# Zulip Chat Archive

## 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.

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

`C a`

is `nat`

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

`add (succ d) m`

is by definition `succ (add d m)`

#### 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