In mathematics, a Kleene algebra (ˈkleɪni ; named after Stephen Cole Kleene) is an idempotent (and thus partially ordered) semiring endowed with a closure operator. It generalizes the operations known from regular expressions.
Various inequivalent definitions of Kleene algebras and related structures have been given in the literature. Here we will give the definition that seems to be the most common nowadays.
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.
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 elements 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: a1 = 1a = a.
Annihilation by 0: a0 = 0a = 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 :
1 + a(a) ≤ a* for all a in A.
1 + (a*)a ≤ a* for all a in A.
if a and x are in A such that ax ≤ x, then ax ≤ x
if a and x are in A such that xa ≤ x, then x(a) ≤ x
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".
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language in
In abstract algebra, a semiring is an algebraic structure. It is a generalization of a ring, dropping the requirement that each element must have an additive inverse. At the same time, it is a generalization of bounded distributive lattices. The smallest semiring that is not a ring is the two-element Boolean algebra, e.g. with logical disjunction as addition. A motivating example that is neither a ring nor a lattice is the set of natural numbers under ordinary addition and multiplication, when including the number zero.
In theoretical computer science and formal language theory, a regular language (also called a rational language) is a formal language that can be defined by a regular expression, in the strict sense in theoretical computer science (as opposed to many modern regular expression engines, which are augmented with features that allow the recognition of non-regular languages). Alternatively, a regular language can be defined as a language recognized by a finite automaton.
In mathematical logic and computer science, the Kleene star (or Kleene operator or Kleene closure) is a unary operation, either on sets of strings or on sets of symbols or characters. In mathematics, it is more commonly known as the free monoid construction. The application of the Kleene star to a set is written as . It is widely used for regular expressions, which is the context in which it was introduced by Stephen Kleene to characterize certain automata, where it means "zero or more repetitions".
In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, st ...
The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under ...
Assoc Computing Machinery2015
, ,
We introduce a precise interprocedural effect analysis for programs with mutable state, dynamic object allocation, and dynamic dispatch. Our analysis is precise even in the presence of dynamic dispatch where the context-insensitive estimate on the number o ...