Action algebra

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•(aa)* ≤ 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. Action algebras were introduced by Vaughan Pratt in the European Workshop JELIA'90.[1]

  1. ^ 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.