Kleene algebra

From Wikipedia, the free encyclopedia
(Redirected from Regular algebra)

Template:Short description Script error: No such module "about".

In mathematics and theoretical computer science, a Kleene algebra (/ˈklni/ Script error: No such module "Respell".; 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 for all x), and induces a partial order defined by xy if x+y=y. The Kleene star operation, denoted x, must satisfy the laws of a closure operator.[1]

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.[2] 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.[3] Kleene algebras and Kleene algebras with tests have applications in formal verification of computer programs.[4] They have also been applied to specify and verify computer networks.[5]

Definition

Various inequivalent definitions of Kleene algebras and related structures have been given in the literature.[6] Here we will give the definition that seems to be the most common nowadays.

A Kleene algebra is a structure (A,+,,,0,1) , where A is a set containing 0 and 1, the operations + and are binary, and the operation is unary. The operator is often omitted. This structure satisfies the following axioms.

The above axioms define a semiring. We further require

It is now possible to define a partial order ≤ on A by setting ab if and only if a + b = b (or equivalently: ab if and only if there exists an x in A such that a + x = b; with any definition, aba 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*)aa* for all a in A.
  • if a and x are in A such that axx, then a*xx
  • if a and x are in A such that xax, then x(a*) ≤ x [7]

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 ab implies axbx. 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

Notational correspondence between
Kleene algebras and + · * 0 1
Regular expressions | not written * ε

Let Σ be a finite set (an "alphabet") and let A be the set of all regular expressions over Σ. We consider two such regular expressions equal if they describe the same language. Then A forms a Kleene algebra. In fact, this is a free Kleene algebra in the sense that any equation among regular expressions follows from the Kleene algebra axioms and is therefore valid in every Kleene algebra.

Again let Σ be an alphabet. Let A be the set of all regular languages over Σ (or the set of all context-free languages over Σ; or the set of all recursive languages over Σ; or the set of all languages over Σ). Then the union (written as +) and the concatenation (written as ·) of two elements of A again belong to A, and so does the Kleene star operation applied to any element of A. We obtain a Kleene algebra A with 0 being the empty set and 1 being the set that only contains the empty string.

Let M be a monoid with identity element e and let A be the set of all subsets of M. For two such subsets S and T, let S + T be the union of S and T and set ST = {st : s in S and t in T}. S* is defined as the submonoid of M generated by S, which can be described as {e} ∪ SSSSSS ∪ ... Then A forms a Kleene algebra with 0 being the empty set and 1 being {e}. An analogous construction can be performed for any small category.

The linear subspaces of a unital algebra over a field form a Kleene algebra. Given linear subspaces V and W, define V + W to be the sum of the two subspaces, and 0 to be the trivial subspace {0}. Define V · W = span {v · w | v ∈ V, w ∈ W}, the linear span of the product of vectors from V and W respectively. Define 1 = span {I}, the span of the unit of the algebra. The closure of V is the direct sum of all powers of V.

V=i=0Vi

Suppose M is a set and A is the set of all binary relations on M. Taking + to be the union, · to be the composition and * to be the reflexive transitive closure, we obtain a Kleene algebra.

Every Boolean algebra with operations and turns into a Kleene algebra if we use for +, for · and set a* = 1 for all a.

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. Using the extended real number line, take a + b to be the minimum of a and b and ab to be the ordinary sum of a and b (with the sum of +∞ and −∞ being defined as +∞). a* is defined to be the real number zero for nonnegative a and −∞ for negative a. This is a Kleene algebra with zero element +∞ and one element the real number zero. A weighted directed graph can then be considered as a deterministic finite automaton, with each transition labelled by its weight. For any two graph nodes (automaton states), the regular expressions computed from Kleene's algorithm evaluates, in this particular Kleene algebra, to the shortest path length between the nodes.[8]

Properties

Zero is the smallest element: 0 ≤ a for all a in A.

The sum a + b is the least upper bound of a and b: we have aa + b and ba + b and if x is an element of A with ax and bx, then a + bx. Similarly, a1 + ... + an is the least upper bound of the elements a1, ..., an.

Multiplication and addition are monotonic: if ab, then

  • a + xb + x,
  • axbx, and
  • xaxb

for all x in A.

Regarding the star operation, we have

  • 0* = 1 and 1* = 1,
  • ab implies a*b* (monotonicity),
  • ana* for every natural number n, where an is defined as n-fold multiplication of a,
  • (a*)(a*) = a*,
  • (a*)* = a*,
  • 1 + a(a*) = a* = 1 + (a*)a,
  • ax = xb implies (a*)x = x(b*),
  • ((ab)*)a = a((ba)*),
  • (a+b)* = a*(b(a*))*, and
  • pq = 1 = qp implies q(a*)p = (qap)*.[9]

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.

History

Kleene introduced regular expressions and gave some of their algebraic laws.[10][11] Although he didn't define Kleene algebras, he asked for a decision procedure for equivalence of regular expressions.[12] Redko proved that no finite set of equational axioms can characterize the algebra of regular languages.[13] Salomaa gave complete axiomatizations of this algebra, however depending on problematic inference rules.[14] 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,[15] however, the bulk of his treatment was infinitary. In 1981, Kozen gave a complete infinitary equational deductive system for the algebra of regular languages.[16] In 1994, he gave the above finite axiom system, which uses unconditional and conditional equalities (considering ab 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]

Generalization (or relation to other structures)

Kleene algebras are a particular case of closed semirings, also called quasi-regular semirings or Lehmann semirings, which are semirings in which every element has at least one quasi-inverse satisfying the equation: a* = aa* + 1 = a*a + 1. This quasi-inverse is not necessarily unique.[18][19] In a Kleene algebra, a* is the least solution to the fixpoint equations: X = aX + 1 and X = Xa + 1.[19]

Closed semirings and Kleene algebras appear in algebraic path problems, a generalization of the shortest path problem.[19]

See also

References

Page Template:Reflist/styles.css has no content.

  1. ^ Page Module:Citation/CS1/styles.css has no content.Marc Pouly; Jürg Kohlas (2011). Generic Inference: A Unifying Theory for Automated Reasoning. John Wiley & Sons. p. 246. ISBN 978-1-118-01086-0.
  2. ^ Page Module:Citation/CS1/styles.css has no content.Conway, J.H. (1971). Regular algebra and finite machines. London: Chapman and Hall. ISBN 0-412-10620-5. Zbl 0231.94041. Chap.IV.
  3. ^ Page Module:Citation/CS1/styles.css has no content.Kozen, Dexter (1997-05-01). "Kleene algebra with tests". ACM Transactions on Programming Languages and Systems. 19 (3): 427–443. doi:10.1145/256167.256195. ISSN 0164-0925.
  4. ^ Page Module:Citation/CS1/styles.css has no content.Kozen, Dexter; Smith, Frederick (1997). "Kleene algebra with tests: Completeness and decidability". In van Dalen, Dirk; Bezem, Marc (eds.). Computer Science Logic. Lecture Notes in Computer Science. Vol. 1258. Berlin, Heidelberg: Springer. pp. 244–259. doi:10.1007/3-540-63172-0_43. ISBN 978-3-540-69201-0.
  5. ^ Page Module:Citation/CS1/styles.css has no content.Anderson, Carolyn Jane; Foster, Nate; Guha, Arjun; Jeannin, Jean-Baptiste; Kozen, Dexter; Schlesinger, Cole; Walker, David (2014-01-08). "NetKAT: Semantic foundations for networks". ACM SIGPLAN Notices. 49 (1): 113–126. doi:10.1145/2578855.2535862. ISSN 0362-1340.
  6. ^ For a survey, see: Page Module:Citation/CS1/styles.css has no content.Kozen, Dexter (1990). "On kleene algebras and closed semirings" (PDF). In Rovan, Branislav (ed.). Mathematical Foundations of Computer Science 1990. Lecture Notes Computer Science. Vol. 452. Springer-Verlag. pp. 26–47. doi:10.1007/BFb0029594. ISBN 3-540-52953-5. Zbl 0732.03047.
  7. ^ Kozen (1990), sect.2.1, p.3
  8. ^ Page Module:Citation/CS1/styles.css has no content.Gross, Jonathan L.; Yellen, Jay (2003), Handbook of Graph Theory, Discrete Mathematics and Its Applications, CRC Press, p. 65, ISBN 9780203490204.
  9. ^ Kozen (1990), sect.2.1.2, p.5
  10. ^ Page Module:Citation/CS1/styles.css has no content.S.C. Kleene (Dec 1951). Representation of Events in Nerve Nets and Finite Automata (PDF) (Technical report). U.S. Air Force / RAND Corporation. p. 98. RM-704. Here: sect.7.2, p.52
  11. ^ Page Module:Citation/CS1/styles.css has no content.Kleene, Stephen C. (1956). "Representation of Events in Nerve Nets and Finite Automata" (PDF). Automata Studies, Annals of Mathematics Studies. 34. Princeton Univ. Press. Here: sect.7.2, p.26-27
  12. ^ Kleene (1956), p.35
  13. ^ Page Module:Citation/CS1/styles.css has no content.Redko, V.N. (1964). "Об определяющей совокупности соотношений алгебры регулярных событий" [On defining relations for the algebra of regular events] (PDF). Ukrainskii Matematicheskii Zhurnal [uk] (in русский). 16 (1): 120–126. Archived from the original (PDF) on 2018-03-29.
  14. ^ Page Module:Citation/CS1/styles.css has no content.Arto Salomaa (Jan 1966). "Two complete axiom systems for the algebra of regular events". Journal of the ACM. 13 (1): 158–169. doi:10.1145/321312.321326. S2CID 8445404.
  15. ^ Page Module:Citation/CS1/styles.css has no content.Conway, J.H. (1971). Regular algebra and finite machines. London: Chapman and Hall. ISBN 0-412-10620-5. Zbl 0231.94041. Chap.IV.
  16. ^ Page Module:Citation/CS1/styles.css has no content.Dexter Kozen (1981). "On induction vs. *-continuity" (PDF). In Dexter Kozen (ed.). Proc. Workshop Logics of Programs. Lect. Notes in Comput. Sci. Vol. 131. Springer. pp. 167–176.
  17. ^ Page Module:Citation/CS1/styles.css has no content.Dexter Kozen (May 1994). "A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events" (PDF). Information and Computation. 110 (2): 366–390. doi:10.1006/inco.1994.1037. — An earlier version appeared as: Page Module:Citation/CS1/styles.css has no content.Dexter Kozen (May 1990). A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events (Technical report). Cornell. p. 27. TR90-1123.
  18. ^ Page Module:Citation/CS1/styles.css has no content.Jonathan S. Golan (30 June 2003). Semirings and Affine Equations over Them. Springer Science & Business Media. pp. 157–159. ISBN 978-1-4020-1358-4.
  19. ^ a b c Page Module:Citation/CS1/styles.css has no content.Marc Pouly; Jürg Kohlas (2011). Generic Inference: A Unifying Theory for Automated Reasoning. John Wiley & Sons. pp. 232 and 248. ISBN 978-1-118-01086-0.

Further reading