Zulip Chat Archive

Stream: new members

Topic: Recursor


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:13):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:14):

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:14):

C a is nat

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:16):

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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:16):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:17):

and add 0 m is by definition m

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:18):

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

view this post on Zulip 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) ?

view this post on Zulip Brandon Brown (Apr 28 2020 at 22:22):

I will try the one-variable case haha

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 22:29):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 29 2020 at 00:08):

they are equal to me

view this post on Zulip Brandon Brown (Apr 29 2020 at 00:09):

the self-referential aspect is obvious in the second style

view this post on Zulip 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