Action algebra
Encyclopedia
In algebraic logic
, an action algebra is an algebraic structure
which is both a residuated semilattice and a Kleene algebra
. It adds the star or reflexive transitive closure operation of the latter to the former, while adding the left and right residuation or implication operations of the former to the latter. Unlike dynamic logic
and other modal logics of programs, for which programs and propositions form two distinct sorts, action algebra combines the two into a single sort. It can be thought of as a variant of intuitionistic logic
with star and with a noncommutative conjunction whose identity need not be the top element. Unlike Kleene algebras, action algebras form a variety
, which furthermore is finitely axiomatizable, the crucial axiom being a•(a → a)* ≤ a. Unlike models of the equational theory of Kleene algebras (the regular expression equations), the star operation of action algebras is reflexive transitive closure in every model of the equations.
such that (A, ∨, •, 1, ←, →) forms a residuated semilattice while (A, ∨, 0, •, 1, *) forms a Kleene algebra
. That is, it is any model of the joint theory of both classes of algebras. Now Kleene algebras are axiomatized with quasiequations, that is, implications between two or more equations, whence so are action algebras when axiomatized directly in this way. What makes action algebras of special interest is that they have an equivalent axiomatization that is purely equational.
In the following we write the inequality a ≤ b as an abbreviation for the equation a ∨ b = b. This allows us to axiomatize the theory using inequalities yet still have a purely equational axiomatization when the inequalities are expanded to equalities.
The equations axiomatizing action algebra are those for a residuated semilattice, together with the following equations for star.
The first equation can be broken out into three equations, 1 ≤ a*, a*•a* ≤ a*, and a ≤ a*. These force a* to be reflexive, transitive, and greater or equal to a respectively. The second axiom asserts that star is monotone. The third axiom can be written equivalently as a•(a→a)* ≤ a, a form which makes its role as induction more apparent. These two axioms in conjunction with the axioms for a residuated semilattice force a* to be the least reflexive transitive element of the semilattice greater or equal to a. Taking that as the definition of reflexive transitive closure of a, we then have that for every element a of any action algebra, a* is the reflexive transitive closure of a.
The equational theory of the star-free fragment of action algebras, those equations not containing star, can be shown to coincide with the equational theory of Kleene algebras, also known as the regular expression
equations. In that sense the above axioms constitute a finite axiomatization of regular expressions. Redko showed in 1967 that these equations had no finite axiomatization, for which John Horton Conway
gave a shorter proof in 1971. Salomaa gave an equation schema axiomatizing this theory which Kozen subsequently reformulated as a finite axiomatization using quasiequations or implications between equations, the crucial quasiequations being those of induction: if x•a ≤ x then x•a* ≤ x, and if a•x ≤ x then a*•x ≤ x. Kozen defined a Kleene algebra to be any model of this finite axiomatization.
Conway showed that the equational theory of regular expressions admit models in which a* was not the reflexive transitive closure of a, by giving a four-element model 0 ≤ 1 ≤ a ≤ a* in which a•a = a. In Conway's model, a is reflexive and transitive, whence its reflexive transitive closure should be a. However the regular expressions do not enforce this, allowing a* to be strictly greater than a. Such anomalous behavior is not possible in an action algebra.
(and hence any Boolean algebra) is made an action algebra by taking • to be ∧ and a* = 1. This is necessary and sufficient for star because the top element 1 of a Heyting algebra is its only reflexive element, and is transitive as well as greater or equal to every element of the algebra.
The set 2Σ* of all formal language
s (sets of finite strings) over an alphabet Σ forms an action algebra with 0 as the empty set, 1 = {ε}, ∨ as union, • as concatenation, L←M as the set of all strings x such that xM ⊆ L (and dually for M→L), and L* as the set of all strings of strings in L (Kleene closure).
The set 2X² of all binary relations on a set X forms an action algebra with 0 as the empty relation, 1 as the identity relation or equality, ∨ as union, • as relation composition, R←S as the relation consisting of all pairs (x,y) such that for all z in X, ySz implies xRz (and dually for S→R), and R* as the reflexive transitive closure of R, defined as the union over all relations Rn for integers n ≥ 0.
The two preceding examples are power sets, which are Boolean algebras under the usual set theoretic operations of union, intersection, and complement. This justifies calling them Boolean action algebras. The relational example constitutes a relation algebra
equipped with an operation of reflexive transitive closure. Note that every Boolean algebra is a Heyting algebra and therefore an action algebra by virtue of being an instance of the first example.
Algebraic logic
In mathematical logic, algebraic logic is the study of logic presented in an algebraic style.What is now usually called classical algebraic logic focuses on the identification and algebraic description of models appropriate for the study of various logics and connected problems...
, an action algebra is an algebraic structure
Algebraic structure
In abstract algebra, an algebraic structure consists of one or more sets, called underlying sets or carriers or sorts, closed under one or more operations, satisfying some axioms. Abstract algebra is primarily the study of algebraic structures and their properties...
which is both a residuated semilattice and a Kleene algebra
Kleene algebra
In mathematics, a Kleene algebra is either of two different things:* A bounded distributive lattice with an involution satisfying De Morgan's laws , additionally satisfying the inequality x∧−x ≤ y∨−y. Kleene algebras are subclasses of Ockham algebras...
. It adds the star or reflexive transitive closure operation of the latter to the former, while adding the left and right residuation or implication operations of the former to the latter. Unlike dynamic logic
Dynamic logic (modal logic)
Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs and later applied to more general complex behaviors arising in linguistics, philosophy, AI, and other fields.-Language:...
and other modal logics of programs, for which programs and propositions form two distinct sorts, action algebra combines the two into a single sort. It can be thought of as a variant of intuitionistic logic
Heyting algebra
In mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...
with star and with a noncommutative conjunction whose identity need not be the top element. Unlike Kleene algebras, action algebras form a variety
Algebraic variety
In mathematics, an algebraic variety is the set of solutions of a system of polynomial equations. Algebraic varieties are one of the central objects of study in algebraic geometry...
, which furthermore is finitely axiomatizable, the crucial axiom being a•(a → a)* ≤ a. Unlike models of the equational theory of Kleene algebras (the regular expression equations), the star operation of action algebras is reflexive transitive closure in every model of the equations.
Definition
An action algebra (A, ∨, 0, •, 1, ←, →, *) is an algebraic structureAlgebraic structure
In abstract algebra, an algebraic structure consists of one or more sets, called underlying sets or carriers or sorts, closed under one or more operations, satisfying some axioms. Abstract algebra is primarily the study of algebraic structures and their properties...
such that (A, ∨, •, 1, ←, →) forms a residuated semilattice while (A, ∨, 0, •, 1, *) forms a Kleene algebra
Kleene algebra
In mathematics, a Kleene algebra is either of two different things:* A bounded distributive lattice with an involution satisfying De Morgan's laws , additionally satisfying the inequality x∧−x ≤ y∨−y. Kleene algebras are subclasses of Ockham algebras...
. That is, it is any model of the joint theory of both classes of algebras. Now Kleene algebras are axiomatized with quasiequations, that is, implications between two or more equations, whence so are action algebras when axiomatized directly in this way. What makes action algebras of special interest is that they have an equivalent axiomatization that is purely equational.
In the following we write the inequality a ≤ b as an abbreviation for the equation a ∨ b = b. This allows us to axiomatize the theory using inequalities yet still have a purely equational axiomatization when the inequalities are expanded to equalities.
The equations axiomatizing action algebra are those for a residuated semilattice, together with the following equations for star.
-
-
- 1 ∨ a*•a* ∨ a ≤ a*
- a* ≤ (a∨b)*
- (a → a)* ≤ a → a
-
The first equation can be broken out into three equations, 1 ≤ a*, a*•a* ≤ a*, and a ≤ a*. These force a* to be reflexive, transitive, and greater or equal to a respectively. The second axiom asserts that star is monotone. The third axiom can be written equivalently as a•(a→a)* ≤ a, a form which makes its role as induction more apparent. These two axioms in conjunction with the axioms for a residuated semilattice force a* to be the least reflexive transitive element of the semilattice greater or equal to a. Taking that as the definition of reflexive transitive closure of a, we then have that for every element a of any action algebra, a* is the reflexive transitive closure of a.
The equational theory of the star-free fragment of action algebras, those equations not containing star, can be shown to coincide with the equational theory of Kleene algebras, also known as the regular expression
Regular expression
In computing, a regular expression provides a concise and flexible means for "matching" strings of text, such as particular characters, words, or patterns of characters. Abbreviations for "regular expression" include "regex" and "regexp"...
equations. In that sense the above axioms constitute a finite axiomatization of regular expressions. Redko showed in 1967 that these equations had no finite axiomatization, for which John Horton Conway
John Horton Conway
John Horton Conway is a prolific mathematician active in the theory of finite groups, knot theory, number theory, combinatorial game theory and coding theory...
gave a shorter proof in 1971. Salomaa gave an equation schema axiomatizing this theory which Kozen subsequently reformulated as a finite axiomatization using quasiequations or implications between equations, the crucial quasiequations being those of induction: if x•a ≤ x then x•a* ≤ x, and if a•x ≤ x then a*•x ≤ x. Kozen defined a Kleene algebra to be any model of this finite axiomatization.
Conway showed that the equational theory of regular expressions admit models in which a* was not the reflexive transitive closure of a, by giving a four-element model 0 ≤ 1 ≤ a ≤ a* in which a•a = a. In Conway's model, a is reflexive and transitive, whence its reflexive transitive closure should be a. However the regular expressions do not enforce this, allowing a* to be strictly greater than a. Such anomalous behavior is not possible in an action algebra.
Examples
Any Heyting algebraHeyting algebra
In mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...
(and hence any Boolean algebra) is made an action algebra by taking • to be ∧ and a* = 1. This is necessary and sufficient for star because the top element 1 of a Heyting algebra is its only reflexive element, and is transitive as well as greater or equal to every element of the algebra.
The set 2Σ* of all formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
s (sets of finite strings) over an alphabet Σ forms an action algebra with 0 as the empty set, 1 = {ε}, ∨ as union, • as concatenation, L←M as the set of all strings x such that xM ⊆ L (and dually for M→L), and L* as the set of all strings of strings in L (Kleene closure).
The set 2X² of all binary relations on a set X forms an action algebra with 0 as the empty relation, 1 as the identity relation or equality, ∨ as union, • as relation composition, R←S as the relation consisting of all pairs (x,y) such that for all z in X, ySz implies xRz (and dually for S→R), and R* as the reflexive transitive closure of R, defined as the union over all relations Rn for integers n ≥ 0.
The two preceding examples are power sets, which are Boolean algebras under the usual set theoretic operations of union, intersection, and complement. This justifies calling them Boolean action algebras. The relational example constitutes a relation algebra
Relation algebra
In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra expanded with an involution called converse, a unary operation...
equipped with an operation of reflexive transitive closure. Note that every Boolean algebra is a Heyting algebra and therefore an action algebra by virtue of being an instance of the first example.