Editing Kleene algebra (section)

== History ==

Kleene introduced regular expressions and gave some of their algebraic laws.<ref>{{cite tech report| author=S.C. Kleene| title=Representation of Events in Nerve Nets and Finite Automata|date=Dec 1951| number=RM-704| pages=98| institution=U.S. Air Force / RAND Corporation| url=http://www.rand.org/content/dam/rand/pubs/research_memoranda/2008/RM704.pdf}} Here: sect.7.2, p.52</ref><ref>{{cite journal| author=Kleene, Stephen C.| title=Representation of Events in Nerve Nets and Finite Automata| journal=Automata Studies, Annals of Mathematical Studies| year=1956| volume=34| publisher=Princeton Univ. Press| url=http://www.dlsi.ua.es/~mlf/nnafmc/papers/kleene56representation.pdf}} Here: sect.7.2, p.26-27</ref>
Although he didn't define Kleene algebras, he asked for a decision procedure for equivalence of regular expressions.<ref>Kleene (1956), p.35</ref>
Redko proved that no finite set of ''equational'' axioms can characterize the algebra of regular languages.<ref>{{cite journal|last=Redko |first=V.N. |url=http://umj.imath.kiev.ua/archiv/1964/01/umj_1964_01_10002_20139.pdf |title=Об определяющей совокупности соотношений алгебры регулярных событий |trans-title=On defining relations for the algebra of regular events| journal={{ill|Ukrainskii Matematicheskii Zhurnal|uk|Український математичний журнал}} | year=1964| volume=16| number=1 | pages=120–126 |language=ru |url-status=dead |archive-url=https://web.archive.org/web/20180329121044/http://umj.imath.kiev.ua/archiv/1964/01/umj_1964_01_10002_20139.pdf |archive-date=2018-03-29 }}</ref>
Salomaa gave complete axiomatizations of this algebra, however depending on problematic inference rules.<ref>{{cite journal| author=Arto Salomaa| title=Two complete axiom systems for the algebra of regular events| journal= Journal of the ACM|date=Jan 1966| volume=13| number=1| pages=158–169| url=http://www.diku.dk/hjemmesider/ansatte/henglein/papers/salomaa1966.pdf| doi=10.1145/321312.321326| s2cid=8445404| author-link=Arto Salomaa}}</ref>
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'',<ref>{{cite book | first=J.H. | last=Conway | author-link=John Horton Conway | title=Regular algebra and finite machines | publisher=Chapman and Hall | year=1971 | isbn=0-412-10620-5 | zbl=0231.94041 | location=London }}  Chap.IV.</ref> however, the bulk of his treatment was infinitary.
In 1981, [[Dexter Kozen|Kozen]] gave a complete infinitary equational deductive system for the algebra of regular languages.<ref>{{cite book| author=Dexter Kozen| chapter=On induction vs. <sup>*</sup>-continuity| title=Proc. Workshop Logics of Programs| year=1981| volume=131| pages=167–176| publisher=Springer| editor=Dexter Kozen| series=Lect. Notes in Comput. Sci.| chapter-url=http://www.cs.cornell.edu/~kozen/papers/indvsstarcont.pdf}}</ref>
In 1994, he gave the [[#Definition|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 [[#Definition|above]] axioms.<ref>{{cite journal| author=Dexter Kozen| title=A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events| journal=Information and Computation|date=May 1994| volume=110| number=2| pages=366–390| url=http://www.cs.cornell.edu/~kozen/papers/ka.pdf| doi=10.1006/inco.1994.1037}} &mdash; An earlier version appeared as: {{cite tech report| author=Dexter Kozen| title=A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events|date=May 1990| number=TR90-1123| pages=27| institution=Cornell| url=http://ecommons.library.cornell.edu/handle/1813/6963}}</ref>