Editing Kleene algebra (section)

{{Short description|Idempotent semiring endowed with a closure operator}}
{{about|the Kleene algebra with a closure operation—a generalization of regular expressions|the Kleene algebra with involution—a generalization of Kleene's ternary logic—|Kleene algebra (with involution)}}

In [[mathematics]] and [[theoretical computer science]], a '''Kleene algebra''' ({{IPAc-en|ˈ|k|l|eɪ|n|i}} {{respell|KLAY|nee}}; named after [[Stephen Cole Kleene]]) is a [[semiring]] that generalizes the theory of [[regular expression]]s: it consists of a [[set (mathematics)|set]] supporting union (addition), concatenation (multiplication), and [[Kleene star]] operations subject to certain algebraic laws. The addition is required to be idempotent (<math>x + x = x</math> for all <math>x</math>), and induces a [[partially ordered set|partial order]] defined by <math>x \le y</math> if <math>x + y = y</math>. The Kleene star operation, denoted <math>x*</math>, must satisfy the laws of the [[closure operator]].<ref name="PoulyKohlas2012">{{cite book|author1=Marc Pouly|author2=Jürg Kohlas|title=Generic Inference: A Unifying Theory for Automated Reasoning|year=2011|publisher=John Wiley & Sons|isbn=978-1-118-01086-0|page=246}}</ref>

Kleene algebras have their origins in the theory of regular expressions and [[regular language]]s introduced by Kleene in 1951 and studied by others including V.N. Redko and [[John Horton Conway]]. The term was introduced 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.<ref name=KAT>{{Cite journal |last=Kozen |first=Dexter |date=1997-05-01 |title=Kleene algebra with tests |url=https://dl.acm.org/doi/abs/10.1145/256167.256195 |journal=ACM Trans. Program. Lang. Syst. |volume=19 |issue=3 |pages=427–443 |doi=10.1145/256167.256195 |issn=0164-0925}}</ref> Kleene algebras and Kleene algebras with tests have applications in [[formal verification]] of computer programs.<ref>{{Cite book |last1=Kozen |first1=Dexter |last2=Smith |first2=Frederick |date=1997 |editor-last=van Dalen |editor-first=Dirk |editor2-last=Bezem |editor2-first=Marc |chapter=Kleene algebra with tests: Completeness and decidability |chapter-url=https://link.springer.com/chapter/10.1007/3-540-63172-0_43 |title=Computer Science Logic |series=Lecture Notes in Computer Science |volume=1258 |language=en |location=Berlin, Heidelberg |publisher=Springer |pages=244–259 |doi=10.1007/3-540-63172-0_43 |isbn=978-3-540-69201-0}}</ref> They have also been applied to specify and verify [[computer network]]s.<ref>{{Cite journal |last1=Anderson |first1=Carolyn Jane |last2=Foster |first2=Nate |last3=Guha |first3=Arjun |last4=Jeannin |first4=Jean-Baptiste |last5=Kozen |first5=Dexter |last6=Schlesinger |first6=Cole |last7=Walker |first7=David |date=2014-01-08 |title=NetKAT: semantic foundations for networks |url=https://dl.acm.org/doi/abs/10.1145/2578855.2535862 |journal=SIGPLAN Not. |volume=49 |issue=1 |pages=113–126 |doi=10.1145/2578855.2535862 |issn=0362-1340}}</ref>