Documentation

Semiring

Ring

A Ring consists of a set equipped with two binary operations that generalize the arithmetic operations of addition and multiplication; it is an abelian group with a second binary operation that is associative, is distributive over the abelian group operation, and has an identity element.

Summary of the laws inherited from the ring super-classes:

zero + a == a
a + zero == a
(a + b) + c == a + (b + c)
a + b == b + a
a - a = zero
negate a = zero - a
negate a + a = zero
a + negate a = zero
one `times` a == a
a `times` one == a
(a `times` b) `times` c == a `times` (b `times` c)
a `times` (b + c) == a `times` b + a `times` c
(a + b) `times` c == a `times` c + b `times` c
a `times` zero == zero
zero `times` a == zero

CRing is a Ring with Multiplicative Commutation. It arises often due to * being defined as a multiplicative commutative operation.

StarSemiring

star a = one + a `times` star a

KleeneAlgebra

a `times` x + x = a ==> star a `times` x + x = x
x `times` a + x = a ==> x `times` 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".