Editing Kleene algebra (section)

== Definition ==

Various inequivalent definitions of Kleene algebras and related structures have been given in the literature.<ref>For a survey, see: {{cite book | zbl=0732.03047 | last=Kozen | first=Dexter | chapter=On Kleene algebras and closed semirings | title=Mathematical foundations of computer science, Proc. 15th Symp., MFCS '90, Banská Bystrica/Czech. 1990 | series=Lecture Notes Computer Science | volume=452 | pages=26–47 | year=1990 | author-link=Dexter Kozen | editor1-last=Rovan | editor1-first=Branislav | publisher=[[Springer-Verlag]] | chapter-url=http://ecommons.library.cornell.edu/bitstream/1813/6971/1/90-1131.pdf }}</ref> Here we will give the definition that seems to be the most common nowadays.

A Kleene algebra is a [[Set (mathematics)|set]] ''A'' together with two [[binary operation]]s + : ''A'' &times; ''A'' → ''A'' and · : ''A'' &times; ''A'' → ''A'' and one unary function <sup>*</sup> : ''A'' → ''A'', written as ''a'' + ''b'', ''ab'' and ''a''<sup>*</sup> respectively, so that the following axioms are satisfied.
* [[Associativity]] of + and ·: ''a'' + (''b'' + ''c'') = (''a'' + ''b'') + ''c'' and ''a''(''bc'') = (''ab'')''c'' for all ''a'', ''b'', ''c'' in ''A''.
* [[Commutativity]] of +: ''a'' + ''b'' = ''b'' + ''a'' for all ''a'', ''b'' in ''A''
* [[Distributivity]]: ''a''(''b'' + ''c'') = (''ab'') + (''ac'') and (''b'' + ''c'')''a'' = (''ba'') + (''ca'') for all ''a'', ''b'', ''c'' in ''A''
* [[Identity element]]s for + and ·: There exists an element 0 in ''A'' such that for all ''a'' in ''A'': ''a'' + 0 = 0 + ''a'' = ''a''. There exists an element 1 in ''A'' such that for all ''a'' in ''A'': ''a''1 = 1''a'' = ''a''.
* [[absorbing element|Annihilation]] by 0: ''a''0 = 0''a'' = 0 for all ''a'' in ''A''.
The above axioms define a [[semiring]]. We further require:
* + is [[idempotent]]: ''a'' + ''a'' = ''a'' for all ''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 <sup>*</sup>:
* 1 + ''a''(''a''<sup>*</sup>) ≤ ''a''<sup>*</sup>  for all ''a'' in ''A''.
* 1 + (''a''<sup>*</sup>)''a'' ≤ ''a''<sup>*</sup>  for all ''a'' in ''A''.
* if ''a'' and ''x'' are in ''A'' such that ''ax'' ≤ ''x'', then ''a''<sup>*</sup>''x'' ≤ ''x''
* if ''a'' and ''x'' are in ''A'' such that ''xa'' ≤ ''x'', then ''x''(''a''<sup>*</sup>) ≤ ''x'' <ref>Kozen (1990), sect.2.1, p.3</ref>

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 function#Monotonicity in order theory|monotonic]], in the sense that ''a'' ≤ ''b'' implies ''ax'' ≤ ''bx''. The idea behind the star operator is ''a''<sup>*</sup> = 1 + ''a'' + ''aa'' + ''aaa'' + ... From the standpoint of [[programming language theory]], one may also interpret + as "choice", · as "sequencing" and <sup>*</sup> as "iteration".