Kleene Algebras #
This file defines idempotent semirings and Kleene algebras, which are used extensively in the theory of computation.
An idempotent semiring is a semiring whose addition is idempotent. An idempotent semiring is
naturally a semilattice by setting a ≤ b
if a + b = b
.
A Kleene algebra is an idempotent semiring equipped with an additional unary operator ∗
, the
Kleene star.
Main declarations #
IdemSemiring
: Idempotent semiringIdemCommSemiring
: Idempotent commutative semiringKleeneAlgebra
: Kleene algebra
Notation #
a∗
is notation for kstar a
in locale Computability
.
References #
- [D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events] [Koz94]
- https://planetmath.org/idempotentsemiring
- https://encyclopediaofmath.org/wiki/Idempotent_semi-ring
- https://planetmath.org/kleene_algebra
TODO #
Instances for AddOpposite
, MulOpposite
, ULift
, Subsemiring
, Subring
, Subalgebra
.
Tags #
kleene algebra, idempotent semiring
An idempotent semiring is a semiring with the additional property that addition is idempotent.
- add : α → α → α
- zero : α
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- sup : α → α → α
- bot : α
The bottom element of an idempotent semiring:
0
by default - bot_le (a : α) : IdemSemiring.bot ≤ a
Instances
An idempotent commutative semiring is a commutative semiring with the additional property that addition is idempotent.
- add : α → α → α
- zero : α
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- sup : α → α → α
- bot : α
Instances
The Kleene star operator on a Kleene algebra
Equations
- Computability.«term_∗» = Lean.ParserDescr.trailingNode `Computability.«term_∗» 1024 1024 (Lean.ParserDescr.symbol "∗")
Instances For
A Kleene Algebra is an idempotent semiring with an additional unary operator kstar
(for Kleene
star) that satisfies the following properties:
1 + a * a∗ ≤ a∗
1 + a∗ * a ≤ a∗
- If
a * c + b ≤ c
, thena∗ * b ≤ c
- If
c * a + b ≤ c
, thenb * a∗ ≤ c
- add : α → α → α
- zero : α
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- sup : α → α → α
- bot : α
- kstar : α → α
- one_le_kstar (a : α) : 1 ≤ KStar.kstar a
- mul_kstar_le_kstar (a : α) : a * KStar.kstar a ≤ KStar.kstar a
- kstar_mul_le_kstar (a : α) : KStar.kstar a * a ≤ KStar.kstar a
- mul_kstar_le_self (a b : α) : b * a ≤ b → b * KStar.kstar a ≤ b
- kstar_mul_le_self (a b : α) : a * b ≤ b → KStar.kstar a * b ≤ b
Instances
Equations
- IdemSemiring.toOrderBot = OrderBot.mk ⋯
Construct an idempotent semiring from an idempotent addition.
Equations
- IdemSemiring.ofSemiring h = IdemSemiring.mk ⋯ 0 ⋯
Instances For
Alias of the reverse direction of add_eq_left_iff_le
.
Alias of the reverse direction of add_eq_right_iff_le
.
Equations
- IdemSemiring.toCanonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯
Equations
- Prod.instIdemSemiring = IdemSemiring.mk ⋯ ⊥ ⋯
Equations
- Prod.instIdemCommSemiring = IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯
Equations
- Prod.instKleeneAlgebra = KleeneAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Pi.instIdemSemiring = IdemSemiring.mk ⋯ ⊥ ⋯
Equations
- Pi.instIdemCommSemiringForall = IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯
Equations
- Pi.instKleeneAlgebraForall = KleeneAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯
Pullback an IdemSemiring
instance along an injective function.
Equations
- Function.Injective.idemSemiring f hf zero one add mul nsmul npow natCast sup bot = IdemSemiring.mk ⋯ ⊥ ⋯
Instances For
Pullback an IdemCommSemiring
instance along an injective function.
Equations
- Function.Injective.idemCommSemiring f hf zero one add mul nsmul npow natCast sup bot = IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯
Instances For
Pullback a KleeneAlgebra
instance along an injective function.
Equations
- Function.Injective.kleeneAlgebra f hf zero one add mul nsmul npow natCast sup bot kstar = KleeneAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯