In mathematics and theoretical computer science, a Kleene algebra (/ˈkleɪni/ 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 term was introduced by Dexter Kozen in the 1980s, who fully characterized their algebraic properties and, in 1994, gave a finite axiomatization.
A Kleene algebra is a set A together with two binary operations + : A × A → A and · : A × A → A and one function * : A → A, written as a + b, ab and a* respectively, so that the following axioms are satisfied.
We further require: 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 *: 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".
S* is defined as the submonoid of M generated by S, which can be described as {e} ∪ S ∪ SS ∪ SSS ∪ ... Then A forms a Kleene algebra with 0 being the empty set and 1 being {e}.
A quite different Kleene algebra can be used to implement the Floyd–Warshall algorithm, computing the shortest path's length for every two vertices of a weighted directed graph, by Kleene's algorithm, computing a regular expression for every two states of a deterministic finite automaton.
Regarding the star operation, we have If A is a Kleene algebra and n is a natural number, then one can consider the set Mn(A) consisting of all n-by-n matrices with entries in A.
Using the ordinary notions of matrix addition and multiplication, one can define a unique *-operation so that Mn(A) becomes a Kleene algebra.
Kleene introduced regular expressions and gave some of their algebraic laws.
[9][10] Although he didn't define Kleene algebras, he asked for a decision procedure for equivalence of regular expressions.
[11] Redko proved that no finite set of equational axioms can characterize the algebra of regular languages.
[12] Salomaa gave complete axiomatizations of this algebra, however depending on problematic inference rules.
[13] The problem of providing a complete set of axioms, which would allow derivation of all equations among regular expressions, was intensively studied by John Horton Conway under the name of regular algebras,[14] however, the bulk of his treatment was infinitary.
In 1981, Kozen gave a complete infinitary equational deductive system for the algebra of regular languages.
[15] In 1994, he gave the above finite axiom system, which uses unconditional and conditional equalities (considering a ≤ b as an abbreviation for a + b = b), and is equationally complete for the algebra of regular languages, that is, two regular expressions a and b denote the same language only if a = b follows from the above axioms.
[17][18] In a Kleene algebra, a* is the least solution to the fixpoint equations: X = aX + 1 and X = Xa + 1.