Power series arithmetic library

Stream: general

[Geoffrey Irving]

Discussion thread for Power series arithmetic library about the series library.

[Geoffrey Irving]

Since the library has generic Newton solvers in place, it is straightforward to add new verified operations that build on top of Newton solves and therefore have optimal time complexity (Newton steps double precision, and thus solves are linear time). For example, one typically implements exp on series via a Newton solve on terms of log, and log is easy too (via integral of inverse).

[Bhavik Mehta]

Can you say to what extent native_decide is used here?

[Geoffrey Irving]

For example, in this Mandelbrot area bound: The rest of the lines reduce the proof to evaluating spray 256, which is three nested layers of power series Newton solvers on top of Dyadic arithmetic using Karatsuba multiplication and such. I haven't made any effort to make it work with decide +kernel, but there's nothing fundamental blocking it other than "native_decide is faster".

[Geoffrey Irving]

Ah, actually it's very array heavy, and possibly arrays interact very badly with the kernel? If the kernel treats them as lists then the complexity would jump by a quadratic factor.

[Bhavik Mehta]

Yeah, to my understanding the kernel treats arrays as lists, but I'd be a bit surprised if they can't be folded away?

Is Karatsuba multiplication implemented in Lean here? I'm slightly surprised that that's faster than the default, which would use GMP for multiplying large integers, and is probably very heavily optimised in C already

[Geoffrey Irving]

Karatsuba for power series, not for Nat: https://github.com/girving/series/blob/6627b8572f4f5628acdc2d6c265e5569bcf1f28c/Series/Series/Mul.lean#L36

[Geoffrey Irving]

It's quite possible that multiplication could be rewritten into a kernel-friendly form. A general principle is that the library is very layered: Newton, inverse, sqrt do not know in any way that multiplication uses Karatsuba.

[Henrik Böving]

Bhavik Mehta said:

Yeah, to my understanding the kernel treats arrays as lists

yes

[Bhavik Mehta]

That makes sense, thanks! The extensibility here is very neat :)

[Geoffrey Irving]

So Karatsuba on a list would be very slow, but Karatsuba on a specific binary tree data structure (splitting top-down) would be very clean and should be kernel friendly. If there is demand signal I could implement this.

[Geoffrey Irving]

The downside is that the Series data structure is then hand-chosen to fit the multiplication operation, but every operation simpler than multiply is trivial and every operation more complex treats multiply as a black box, so it would be okay. Of course, if one later wanted FFT multiply it would need to be rewritten.

[Henrik Böving]

There already exists a kernel efficient array structure with docs#Lean.RArray though it is mostly built for reflection proofs at the moment.

[Geoffrey Irving]

My guess is that unless RArray is power-of-two specific, it would be easier given the Karatsuba context to do it custom.

[Geoffrey Irving]

Hmm, actually RArray is really close to perfect, so maybe I do just want RArrays with some invariant about them stored separately.

[Henrik Böving]

You would also need to prove some theory about it given that this is currently non existent

[Henrik Böving]

I guess it might be interesting to have an abstract notion of an Array with similar axioms as the SMT-LIB array theory so people can write programs that abstract about runtime and kernel efficient arrays? Not sure

[Geoffrey Irving]

That might be useful separate from this, but here Karatsuba has a recursive structure related to power-of-two-sized chunks, so the adjusted multiply routine would be recursing directly on the tree structure rather than using an abstract Array-like API.

[Bas Spitters]

That looks very nice. How does it relate to the porting effort of exact real numbers from Rocq to Lean?
I believe they are working both on the old corn real numbers and the faster type class based ones.
http://arxiv.org/abs/1105.2751

In speed it will likely be incomparable, since Lean is using (unverified) GMP.

[Geoffrey Irving]

This library is power series on top of whatever kind of scalar arithmetic one wants, assuming it has an Approx instance saying it approximates your designed mathematical scalar type. So I don’t think it is closely related to exact real numbers.

[Mauricio Collares]

Geoffrey Irving said:

I proved it correct, then tested it, and the tests did not work

Just want to say I love the Knuth reference

[Geoffrey Irving]

@Henrik Böving @Bhavik Mehta Here's all the ring operations in a hopefully kernel-friendly form, using a data structure similar to RArray but specialised to power-of-two sizes.

https://gist.github.com/girving/db7a31fe4df064f4a9aba76927cab14a

The proofs of correctness are way simpler than for the array version, since everything is more natural functional programming. I think I'll probably switch the whole library to this, but I'll need to do various translation first.

[Geoffrey Irving]

Nearly all of the case analysis logic was written by Sonnet 4.5 against Sonnet 4.5-written unit tests, and then I put the correctness proofs in place after the fact.