Zulip Chat Archive

Stream: new members

Topic: timeout when #reduce-ing fin n function


Alex Reynaldi (Jun 04 2021 at 13:55):

Hi, Whenever I try to #reduce a function defined recursively on fin n, I get a timeout. However using #eval works just fine. The minimal example is the factorial function in the documentation for fin.has_well_founded:

import data.fin

def factorial {n : } : fin n  
| 0, _ := 1
| i + 1, hi := (i + 1) * factorial i, i.lt_succ_self.trans hi

#reduce factorial 2 --timeout
#eval @factorial 3 2 --works fine

Am I missing something or doing something wrong?

Eric Rodriguez (Jun 04 2021 at 13:57):

Kernel computation is slow :(

Alex Reynaldi (Jun 04 2021 at 13:59):

Is it really just that slow though? because even #reduce factorial 0 seems to timeout

Yakov Pechersky (Jun 04 2021 at 14:05):

It can't figure out which fin n you mean.

Yakov Pechersky (Jun 04 2021 at 14:05):

Because 2 is 0 in fin 0, 1, or 2

Yakov Pechersky (Jun 04 2021 at 14:07):

What happens if you say #reduce factorial (2 : fin 3)?

Kevin Buzzard (Jun 04 2021 at 14:07):

Can you make this a #mwe ? I just tried this and your code doesn't compile -- you're missing imports or opens or something (you can just edit the original message, no need to repost).

Alex Reynaldi (Jun 04 2021 at 14:09):

sorry about that, I just forgot to import data.fin

Kevin Buzzard (Jun 04 2021 at 14:12):

#reduce @factorial 1 0 -- 1
#reduce @factorial 2 0 -- 1

def one : fin 2 := 1, dec_trivial

#reduce factorial one -- nope

Alex Reynaldi (Jun 04 2021 at 14:19):

@Yakov Pechersky , #reduce factorial (2 : fin 3) also timeouts for me. I can reproduce what @Kevin Buzzard put up though.

Alex Reynaldi (Jun 04 2021 at 14:24):

#reduce @factorial 3 1 also timeouts on my end

Gihan Marasingha (Jun 04 2021 at 15:15):

I think the issue is with the code produced by the equation compiler, maybe something to do with the fact that has_well_founded is involved? Anyway, the following works fine.

import data.fin

def factorial {n : } : fin n   :=
λ fn, subtype.rec_on fn (λ m p, nat.rec_on m 1 (λ k ih, (k+1)*ih))

#reduce @factorial 3 1

#reduce factorial (5 : fin 6)

Alex Reynaldi (Jun 04 2021 at 15:31):

Yes this works, thank you!


Last updated: Dec 20 2023 at 11:08 UTC