Documentation

Distributive

\a b c -> a * (b + c) == a * b + a * c

\a b c -> (a + b) * c == a * c + b * c

\a -> zero * a == zero

\a -> a * zero == zero

The sneaking in of the Absorption laws here glosses over the possibility that the multiplicative zero element does not have to correspond with the additive unital zero.

A Ring is an abelian group under addition (Unital, Associative, Commutative, Invertible) and monoidal under multiplication (Unital, Associative), and where multiplication distributes over addition.

\a -> zero + a == a
\a -> a + zero == a
\a b c -> (a + b) + c == a + (b + c)
\a b -> a + b == b + a
\a -> a - a == zero
\a -> negate a == zero - a
\a -> negate a + a == zero
\a -> a + negate a == zero
\a -> one * a == a
\a -> a * one == a
\a b c -> (a * b) * c == a * (b * c)
\a b c -> a * (b + c) == a * b + a * c
\a b c -> (a + b) * c == a * c + b * c
\a -> zero * a == zero
\a -> a * zero == zero

A StarSemiring is a semiring with a unary star operator satisfying the Conway equations:

\a -> star a == one + a * star a                                  -- fixpoint
\a b -> star (a * b) == one + a * star (b * a) * b                -- product-star (sliding)
\a b -> star (a + b) == star (star a * b) * star a                -- sum-star (vanishing)

These three equations are the doctestable core; they are exactly the sliding and vanishing axioms of a traced category in semiring clothing.

A Kleene Algebra is a Star Semiring with idempotent addition.

Idempotent addition gives a natural order a <= b ⟺ a + b == b. In that order, Kozen's induction laws hold as derived facts:

a * x + x <= x  ==>  star a * x + x <= x
x * a + x <= x  ==>  x * star a + x <= x

They are stated here as prose rather than class laws because they involve a partial order and Horn clauses, which do not fit the equational/doctest style of the Conway core.

Conway equations for Bool.

>>> let a = False; b = True in star (a * b) == one + a * star (b * a) * b
True

>>> let a = False; b = True in star (a + b) == star (star a * b) * star a
True

Involutive Ring

adj (a + b) ==> adj a + adj b
adj (a * b) ==> adj a * adj b
adj one ==> one
adj (adj a) ==> a

Note: elements for which adj a == a are called "self-adjoint".

Defining two requires adding the multiplicative unital to itself. In other words, the concept of two is a Ring one.

>>> two
2