KleeneAlgebra axioms don't quite match literature

[Taneb]

Pinging @Akshobhya1234 on this one who originally added them, to make sure I'm not missing something and to make sure it's not breaking his use case.

We define StarLeftExpansive as e + x ∙ x * ≈ x * (similarly for StarRightExpansive), and StarLeftDestructive as b + a ∙ x ≈ x → a * ∙ b ≈ x`.

The closest definitions I can find are in Dexter Kozen's lecture notes (cited by Wikipedia), which claims to follow an out of print textbook:

Or e + x ∙ x * ≤ x * and b + a ∙ x ≤ x → a * ∙ b ≤ x in the notation I used earlier. But note! ≤ is not ≈. How is it defined? Again, from Dexter Kozen's lecture notes:

Or in our notation, x ≤ y = x + y ≈ y. Rephrasing the laws inlining this definition, we get something like

StarLeftExpansive = e + x ∙ x * + x * ≈ x *
StarLeftDestructive = b + x ∙ a + x ≈ x → a * ∙ b + x ≈ x

I ran into this while trying to implement regular expressions, and finding it impossible to prove StarLeftDestructive. I have not tried to see if my alternate definitions work better for that yet.

[jamesmckinna]

Conway's (1971) book "Regular Algebra and Finite Machines" discusses this in Ch.4, but for yet another axiomatisation (his C1-C14, Ch.3, p.25) but this is not the Kozen one. C1-C10 are the semiring axioms, leaving:

• C11 (sumstar) (x + y)* = (x*y)*x*
• C12 (productstar) (xy)* = 1 + x(yx)*y
• C13 (starstar) (x*)* = x*
• C14n (powerstar, n>0) x* = (x^n)*(x^<n)

where in the last (apologies for clunky notation; superscript < is tricky in markdown!) we have, definitionally

• x^0 = 1
• x^(suc n) = x(x^n)
• x^<0 = 0
• x^<(suc n) = x^<n + x^n

So one first challenge might be to prove C11-C14n hold equationally from the Akshobaya axiomatisation?

Then, he deduces a bunch of things, including idempotence of +, from C1-C12, and various forms of C13/C14n, specifically the weak form of C13 (taking x = 0 in C13, and appealing to y = 1 in C12 to obtain C15, x* = 1 + xx*, and hence C19, 0* = 1).

Happy to do some more digging if need be.

UPDATED: Conway's book appears to be the out-of-print source available for students of Dexter Kozen's course referred to above...

[Akshobhya1234]

I changed these definitions to define partial order axioms as equality in my thesis. I never got opportunity to port it here.
Please take a look at Chapter 7 on Kleene Algebra here -->
https://prod-ms-be.lib.mcmaster.ca/server/api/core/bitstreams/f701290e-a8c1-4372-85c6-f4dd1745783a/content

In Chapter 7.5 I add proofs for some of the properties. Here is the old github link if the above doesn't work -->
https://github.com/Akshobhya1234/MSc-thesis/blob/master/Thesis_Main.pdf

[JacquesCarette]

If we can find some "canonical source" (and saying Kozen's own notes is not is... interesting), we can indeed change this for v3.0. All kidding aside, it is entirely possible that the community has settled on an axiomatization of these that differs from Kozen's early work. We should do that.

Wonder if there's a Rocq library, or something in mathlib we could compare with.

[Taneb]

Here's mathlib's equivalent: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Kleene.html

[jamesmckinna]

I have a sketch that the Akshobhya axiomatisation implies that of Kozen, but not vice versa:

• in both cases, (1 + x)* = x* is provable (and the key to the A to K direction)
• but for K to A, all I think you can prove is that b + a x = x implies a*b ≤ x. But I can't seem to prove x ≤ a*b.

Oh dear!

[jamesmckinna]

I think the problem is that the Akshobhya axiomatisation only ensures that x = a*b is a fixed point of x = b + ax, while the Kozen axiomatisation further ensures that it is the least solution (with the axioms essentially being introduction/elimination rules for x* wrt ≤ qua consequence relation).

So... we should change the definitions, and working out the nicest ergonomics for that is... an interesting challenge.