Action algebra
In
Definition
An action algebra (A, ∨, 0, •, 1, ←, →, *) is an
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*. Defining a to be reflexive when 1 ≤ a and transitive when a•a ≤ a by abstraction from binary relations, the first two of those equations force a* to be reflexive and transitive while the third forces a* to be greater or equal to a. The next axiom asserts that star is monotone. The last 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 of elements 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.
Properties
The equational theory of the implication-free fragment of action algebras, those equations not containing → or ←, can be shown to coincide with the equational theory of Kleene algebras, also known as the
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, which forces a* to be the least transitive reflexive element.
Examples
Any Heyting 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 languages (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
See also
References
- ^ Pratt, Vaughan (1990), "Action Logic and Pure Induction" (PDF), Logics in AI: European Workshop JELIA '90 (ed. J. van Eijck), LNCS 478, Springer-Verlag, pp. 97–120.
- Trans. Amer. Math. Soc.45: 335–54. Reprinted in Bogart, K, Freese, R., and Kung, J., eds. (1990) The Dilworth Theorems: Selected Papers of R.P. Dilworth Basel: Birkhäuser.
- ^ Kozen, Dexter (1990), "On Kleene algebras and closed semirings" (PDF), in B. Rovan (ed.), Mathematical Foundations of Computer Science (MFCS), LNCS 452, Springer-Verlag, pp. 26–47
- MR 1295061.
- Zbl 0231.94041.
- ^ V.N. Redko, On defining relations for the algebra of regular events (Russian), Ukrain. Mat. Z., 16:120–126, 1964.