|
Kleene Algebra, Quantales and Relation Algebra in Formal Program Derivation
by
Bernhard Möller
Institut für Informatik, Universität Augsburg
Kleene algebra (see e.g. [, ]) is an algebraic system for calculating with sequential composition, choice and finite iteration. Its classical application has been within the theory of formal languages, where it is one of many equivalent approaches to the description of regular languages.
A special variant of Kleene algebras are quantales (see e.g. []) with a composition operation that is universally disjunctive in both arguments. This can be used to give abstract definitions of the domain and range operations through Galois connections and of the modal operations as used in dynamic algebra [, ]. Also, more generally than pure Kleene algebra, quantales allow a treatment of infinite iteration through greatest fixpoints.
Abstract (and concrete) relation algebras form a particular case of quantales and hence of Kleene algebras. Within the field of formal algorithm derivation they have been applied, among others, to path problems on graphs (being closely related to the algebra of closed semirings) [] and to the formal treatment of pointer algorithms [].
It turns out that many of the notions used in these derivations can be formulated more abstractly in the setting of quantales; this leads to simpler and more perspicuous proofs.
Also, the framework of quantales has been successfully applied to the semantic description of imperative programs with both angelic and demonic non-deterministic choice [, ].
We give a brief summary of these results and point out some open problems.
References
http://www.math.uni-augsburg.de/~moeller/
Date received: January 2, 2001
Copyright © 2001 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cafo-45.