Zulip Chat Archive

Stream: maths

Topic: Redefining Cantor's normal form

Violeta Hernández (May 23 2022 at 14:08):

Right now, docs#ordinal.CNF has very little API. I presume a lot of the reason is the particularly odd data structure used, a list of pairs of ordinals.

Violeta Hernández (May 23 2022 at 14:09):

Having a list instead of a set is a nice way to represent finiteness, but I think there's better approaches

Violeta Hernández (May 23 2022 at 14:10):

I was thinking defining Cantor normal form as a finitely supported function from ordinals to nat. This would ditch support for bases other than w, but those are exceedingly rare anyways, and the w case has a lot more properties than the others.

Violeta Hernández (May 23 2022 at 14:11):

One very nice advantage is that by doing this, we can state CNF (a # b) = CNF a + CNF b. This could probably be used to golf a bunch of lemmas on natural addition later down the line.

Violeta Hernández (May 23 2022 at 14:12):

I don't know if lexicographic ordering is defined on finitely supported functions, but if it is, then we could also prove a < b \iff CNF a < CNF b

Violeta Hernández (May 23 2022 at 14:14):

We might even be able to define a polynomial-like multiplication in order to state the result on the Cantor normal form of the natural multiplication

Violeta Hernández (May 23 2022 at 14:20):

Oh and also, we'd get an extensionality lemma from this

Violeta Hernández (May 23 2022 at 14:20):

If CNF a i = CNF b i for all i, then a = b

Violeta Hernández (May 23 2022 at 14:25):

I'm interested in @Mario Carneiro's opinion (I presume he was the one who made the current CNF definition)

Junyan Xu (May 23 2022 at 15:36):

https://leanprover-community.github.io/mathlib_docs/data/pi/lex.html

Violeta Hernández (May 23 2022 at 15:39):

No, that's not it. I mean lexicographic order as in dictionary order.

Violeta Hernández (May 23 2022 at 15:40):

(1, 2, 3) > (1, 1000, 2)

Yaël Dillies (May 23 2022 at 15:40):

Yeah, that's exactly what pi.lex does.

Violeta Hernández (May 23 2022 at 15:40):

Ah, really?

Violeta Hernández (May 23 2022 at 15:40):

Oh wow

Yaël Dillies (May 23 2022 at 15:41):

Yeah. The definition reads "x and y agree up to some point, and x i < y iat that point".

Violeta Hernández (May 23 2022 at 15:41):

Do we have this on finsupp though?

Yaël Dillies (May 23 2022 at 15:41):

No but I can cook it for you if needed.

Violeta Hernández (May 23 2022 at 15:42):

That would be much appreciated!

Yaël Dillies (May 23 2022 at 15:42):

Are you sure you want it, though? Can you not use to_lex ⇑f ≤ to_lex ⇑g directly?

Violeta Hernández (May 23 2022 at 15:42):

That's probably a better idea

Junyan Xu (May 23 2022 at 15:45):

You may be able to get the ring structure as a subring of https://leanprover-community.github.io/mathlib_docs/ring_theory/hahn_series.html

I'd like to keep the general base, but maybe change one coordinate to the subtype of ordinals less than the base, then when the base is omega you can use the equiv between the subtype and N.

Violeta Hernández (May 23 2022 at 15:46):

hahn_series can have infinite support though, can't they?

Violeta Hernández (May 23 2022 at 15:47):

Also, the pseudo-polynomial multiplication on Cantor normal forms is a bit subtler, since you need to add the exponents via natural addition. So I don't think that's going to help much

Violeta Hernández (May 23 2022 at 15:49):

I don't like the idea of a general base, since it introduces a lot of complexity we just don't care about most of the time. Like having to use the conversion between ω.out.α and ℕ, and having to consistently exclude degenerate bases like 1 or 0.

Junyan Xu (May 23 2022 at 15:49):

Yes, so I said "subring". But maybe monoid_algebra works

Violeta Hernández (May 23 2022 at 15:50):

I guess we could just have the API specialized for the ω case when appropriate, though

Junyan Xu (May 23 2022 at 15:50):

maybe add_monoid_algebra nat_ordinal

Violeta Hernández (May 23 2022 at 15:51):

Hmm... that seems reasonable actually

Junyan Xu (May 23 2022 at 15:53):

I guess you could develop new API and don't replace the old one if the new one less general

Violeta Hernández (May 23 2022 at 15:54):

Actually, I think non-ω bases might introduce further problem if we follow this approach, since the ordinals lesser than another are generally not closed under addition

Violeta Hernández (May 23 2022 at 15:54):

Well, it's not like we make much use of the current API anyways

Violeta Hernández (May 23 2022 at 15:54):

The few results below docs#ordinal.CNF are all we have

Violeta Hernández (May 23 2022 at 15:55):

And even if there's really any use for non-ω bases, I still think we should redefine what we currently have

Junyan Xu (May 23 2022 at 16:05):

maybe rename the original to CNFb, in analogy to docs#real.logb

Junyan Xu (May 23 2022 at 16:06):

log with base omega is really "natural" log!

Junyan Xu (May 23 2022 at 16:15):

Actually, I think non-ω bases might introduce further problem if we follow this approach, since the ordinals lesser than another are generally not closed under addition

Maybe they are closed under addition iff the ordinal is of the form alpha*omega, and under multiplication iff it's of the form alpha^omega? I think I can show the if direction.

Violeta Hernández (May 23 2022 at 16:26):

I actually already proved which ordinals are closed under addition and multiplication

Violeta Hernández (May 23 2022 at 16:28):

docs#ordinal.principal_add_iff_zero_or_omega_opow and docs#ordinal.principal_mul_iff_le_two_or_omega_opow_opow

Violeta Hernández (May 23 2022 at 16:30):

omega^omega is closed under addition but not of the form a * omega

Violeta Hernández (May 23 2022 at 16:30):

I do prove in that same file a * omega is either 0 or a power of omega, so the if direction is true

Violeta Hernández (May 23 2022 at 16:31):

Even then, turning a principal ordinal into an additive monoid seems like a hard thing to set up

Violeta Hernández (May 23 2022 at 16:32):

If we can't provide this polynomial structure on general Cantor normal forms, I think defining them as finsupp might be the best approach

Violeta Hernández (May 23 2022 at 16:33):

We could then provide glue between the general Cantor normal form and the one for omega

Violeta Hernández (May 23 2022 at 16:35):

... Although, I don't think the definition of CNF should depend on nat_ordinal

Violeta Hernández (May 23 2022 at 16:35):

Perhaps we can define it as a finsupp always, and then, in order to prove the theorem about the CNF of natural multiplication, we make another definition with this extra structure

Violeta Hernández (May 23 2022 at 16:39):

Because treating the CNF as a polynomial is a really niche thing you really only do to state those two theorems on natural operations

Violeta Hernández (May 23 2022 at 16:43):

Yeah, I think defining CNFb and CNF as finsupps with a bit of glue between both is the best approach

Mario Carneiro (May 23 2022 at 23:36):

I don't think the existing definition should be changed, but you are free to add another definition if you like, and possibly rename the original one if the new definition is significantly more useful

Mario Carneiro (May 23 2022 at 23:37):

in particular I don't think it would be a good idea to drop support for other bases. It's not like other bases can be written in terms of the omega-logarithm, so the analogy with ln doesn't really hold up

Mario Carneiro (May 23 2022 at 23:42):

If there are theorems that only hold for omega, well then state them using CNF omega, I don't really see the issue

Violeta Hernández (May 24 2022 at 02:14):

Hmm, I found a problem with the finsupp definition. I can't use finsupp.sum because ordinal addition isn't commutative

Violeta Hernández (May 24 2022 at 02:14):

Is there an ordered version of that?

Violeta Hernández (May 24 2022 at 02:28):

Doesn't seem to be

Violeta Hernández (May 24 2022 at 02:28):

Well, I guess that's the end of that idea

Violeta Hernández (May 24 2022 at 02:29):

Perhaps I should keep the current definition, which allows us to state results like "the sum of the terms in the normal form is the ordinal", but also define a finsupp in terms of it, which makes it easier to refer to specific coefficients and allows us to state theorems like when a CNF is less than another

Violeta Hernández (May 24 2022 at 03:35):

Yeah you know, working with CNF, I'm beginning to see its virtues

Violeta Hernández (May 24 2022 at 03:35):

I do still think it's missing a huge amount of API

Mario Carneiro (May 24 2022 at 04:31):

I think what is there is everything I needed / everything I could think of, so if you have more ideas feel free to extend it

Mario Carneiro (May 24 2022 at 04:31):

in particular a coefficient extraction function sounds like a good idea

Violeta Hernández (May 24 2022 at 05:16):

Here's some missing theorems I've found, modulo exceptions with small bases:

every term in the CNF is less or equal to the ordinal
the terms are decreasing (not just the exponents)
if (x, y) belongs to the CNF of o, then o / b ^ x % b = y, and viceversa for positive y

Violeta Hernández (May 24 2022 at 05:17):

I want the last theorem in order to code the coefficient extraction function

Violeta Hernández (May 24 2022 at 05:17):

Of course, these are just basic theorems. It would be nice to eventually have lemmas on how the normal form interacts with the ordinal operations

Mario Carneiro (May 24 2022 at 05:18):

the last one doesn't sound right

Violeta Hernández (May 24 2022 at 05:19):

Sorry, fixed

Mario Carneiro (May 24 2022 at 05:19):

Ah yeah that's better

Violeta Hernández (May 24 2022 at 05:19):

I also believe there should be some induction theorem to prove something about all entries of a CNF (CNF_rec inducts on ordinals, I want something more direct). I bet this could be used to golf a bunch of the proofs

Violeta Hernández (May 24 2022 at 05:20):

Can't quite figure out what this induction principle would be, though

Mario Carneiro (May 24 2022 at 05:20):

I'm not sure what you mean

Mario Carneiro (May 24 2022 at 05:20):

what kind of constructs do you expect in the induction statement?

Mario Carneiro (May 24 2022 at 05:21):

I mean it's obviously defined by recursive application of ^ and % so an induction principle that says as much wouldn't be hard

Violeta Hernández (May 24 2022 at 05:21):

Something like "if when a proposition holds for all entries of CNF b (o / b ^ log b o), it also holds for all entries of CNF b o, then it holds for all entries of a CNF"