Zulip Chat Archive

Stream: new members

Topic: deep recursion error reducing strings


view this post on Zulip Kevin Sullivan (Feb 25 2020 at 15:16):

I'm wondering why using #reduce to evaluate even one-character strings leads to a stack overflow in the default configuration of Lean? To replicate, try this.

#reduce "-"

view this post on Zulip Rob Lewis (Feb 25 2020 at 15:21):

A string is a list of chars. A char is a pair of a nat n and a proof of n < 55296 ∨ 57343 < n ∧ n < 1114112. The normal form of that proof is very very large.

view this post on Zulip Gabriel Ebner (Feb 25 2020 at 15:28):

Already the numbers that Rob posted are huge when you unfold them completely:

#reduce 15153 -- works
#reduce 15154 -- stack overflow

view this post on Zulip Kevin Sullivan (Feb 25 2020 at 16:27):

I see. Ok. For pedagogy, this is inconvenient, as reduce doesn't work to show terms involving strings and #eval prints them in kernel rather than source format. But it is what it is, and I understand there's no workaround. Thank you, gentlemen.

Gabriel Ebner said:

Already the numbers that Rob posted are huge when you unfold them completely:

#reduce 15153 -- works
#reduce 15154 -- stack overflow

view this post on Zulip Rob Lewis (Feb 25 2020 at 16:30):

#eval prints them in kernel rather than source format

Not sure exactly what you mean by this, but do you want #eval repr "-"? (Same on that example, but compare with something with new lines or whatever.)


Last updated: May 14 2021 at 02:15 UTC