asymptotics

Stream: CSLib

[Alex Meiburg]

One other thing I was working on over at my circuit complexity stuff was a better general notion of asymptotics, of the kind I see in complexity theory a lot. https://github.com/Timeroot/CircuitComp/blob/main/CircuitComp/GrowthRate.lean

The idea is define important classes like "poly", "exp", "quasipoly", etc. and give their relative containments, closure under addition/multiplication/composition and so on. A lot of things you get from big O notation of course, but there's also a lot missing - I mean, "poly" isn't even a big O class itself. And it 'should' be a one-liner that if f is in poly and g is in log, then f(x+5) * g(x) is also in poly. And stuff like that

And then there's lots of connecting this back and forth to things about reals. Like you should have that Real.log, Real.logb, Nat.log, Nat.log2 are all in log to start with. Similar things with Real.sqrt vs. Nat.sqrt, Real.exp vs real powers vs natural number powers, all that jazz

[Alex Meiburg]

This is something I think CSlib could use, hopefully?

[Alex Meiburg]

Once I've got it decently fleshed out I'm thinking of an aesop-based tactic for trying to mostly automatically prove structural things

[Alex Meiburg]

I'll admit that there's sizable overlap with #announce > New tactic: `compute_asymptotics` @ 💬 which came out after I'd started that, but I think the goals are also different. (More theorems, clearer statements -- like saying "this is in the class foo", less tactic automation to solve existing types of statements)

[Snir Broshi]

Is this related to #maths > Use of embedded Landau notation and FC#1481?
It seems they also try to have common expressions/operations that auto-compute their asymptotics.

[Alex Meiburg]

It has a similar flavor but this is trying to do a different thing

[Alex Meiburg]

In particular, I'm trying to name the common function families I care about.

[Alex Meiburg]

There likely could be some synergy is either one gets sufficiently well-developed, though.