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 an additional unary operator (star) satisfying:

\a -> star a = one + a * star a

A Kleene Algebra is a Star Semiring with idempotent addition.

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

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