In mathematics and theoretical computer science, a Kleene algebra ( KLAY-nee; named after Stephen Cole Kleene) is a semiring that generalizes the theory of regular expressions: it consists of a set supporting union (addition), concatenation (multiplication), and Kleene star operations subject to certain algebraic laws. The addition is required to be idempotent ( x + x = x {\displaystyle x+x=x} for all x {\displaystyle x} ), and induces a partial order defined by x ≤ y {\displaystyle x\leq y} if x + y = y {\displaystyle x+y=y} . The Kleene star operation, denoted x ∗ {\displaystyle x^{*}} , must satisfy the laws of a closure operator. Kleene algebras have their origins in the theory of regular expressions and regular languages introduced by Kleene in 1951 and studied by others including V.N. Redko and John Horton Conway, who introduced the term in 1971. The concept was later popularized by Dexter Kozen in the 1980s, who fully characterized their algebraic properties and, in 1994, gave a finite axiomatization. Kleene algebras have a number of extensions that have been studied, including Kleene algebras with tests (KAT) introduced by Kozen in 1997. Kleene algebras and Kleene algebras with tests have applications in formal verification of computer programs. They have also been applied to specify and verify computer networks.
Definition Various inequivalent definitions of Kleene algebras and related structures have been given in the literature. Here we will give the definition that seems to be the most common nowadays. A Kleene algebra is a structure ( A , + , ⋅ , ∗ , 0 , 1 ) {\displaystyle (A,+,\cdot ,^{*},0,1)} , where A {\displaystyle A} is a set containing 0 {\displaystyle 0} and 1 {\displaystyle 1} , the operations + {\displaystyle +} and ⋅ {\displaystyle \cdot } are binary, and the operation ∗ {\displaystyle ^{*}} is unary. The operator ⋅ {\displaystyle \cdot } is often omitted. This structure satisfies the following axioms.
Associativity of + {\displaystyle +} and ⋅ {\displaystyle \cdot } : ( a + b ) + c = a + ( b + c ) {\displaystyle (a+b)+c=a+(b+c)} and ( a b ) c = a ( b c ) {\displaystyle (ab)c=a(bc)} for all a , b , c ∈ A {\displaystyle a,b,c\in A} . Commutativity of + {\displaystyle +} : a + b = b + a {\displaystyle a+b=b+a} for all a , b ∈ A {\displaystyle a,b\in A} . Distributivity: a ( b + c ) = a b + a c {\displaystyle a(b+c)=ab+ac} and ( b + c ) a = b a + c a {\displaystyle (b+c)a=ba+ca} for all a , b , c ∈ A {\displaystyle a,b,c\in A} . Identity elements for + {\displaystyle +} and ⋅ {\displaystyle \cdot } : for all a ∈ A {\displaystyle a\in A} we have a + 0 = 0 + a = a {\displaystyle a+0=0+a=a} and a 1 = 1 a = a {\displaystyle a1=1a=a} . Annihilation by 0 {\displaystyle 0} : a 0 = 0 a = 0 {\displaystyle a0=0a=0} for all a ∈ A {\displaystyle a\in A} . The above axioms define a semiring. We further require
Idempotence of + {\displaystyle +} : a + a = a {\displaystyle a+a=a} for all a ∈ A {\displaystyle a\in A} . It is now possible to define a partial order ≤ on A by setting a ≤ b if and only if a + b = b (or equivalently: a ≤ b if and only if there exists an x in A such that a + x = b; with any definition, a ≤ b ≤ a implies a = b). With this order we can formulate the last four axioms about the operation *:
1 + a(a*) ≤ a* for all a in A. 1 + (a*)a ≤ a* for all a in A. if a and x are in A such that ax ≤ x, then a*x ≤ x if a and x are in A such that xa ≤ x, then x(a*) ≤ x Intuitively, one should think of a + b as the "union" or the "least upper bound" of a and b and of ab as some multiplication which is monotonic, in the sense that a ≤ b implies ax ≤ bx. The idea behind the star operator is a* = 1 + a + aa + aaa + ... From the standpoint of programming language theory, one may also interpret + as "choice", · as "sequencing" and * as "iteration".
Examples
… excerpt ends here. Continue reading the full article.
