Typed Kleene Algebras

Kleene algebras provide a convenient and powerful algebraic axiomatisation of a complete lattice that is endowed with a sequential composition operation. Models include formal languages under concatenation, relations under standard composition, sets of graph paths under path concatenation and sets of streams under concatenation. The least and greatest fixpoint operators of a complete lattice allow definitions of the finite and infinite iteration operators * and w, resp. The abstract setting of Kleene algebras was used in [3] for the schematic derivation of a class of algorithms that abstracts layer-oriented graph traversals such as breadth-first search. It was also shown that the standard efficiency improvement for such algorithms, viz. carrying along a set of already visited vertices, can completely be transferred to the abstract level. The set of already visited vertices is used to restrict the underlying graph appropriately. So we need abstract counterparts of the notions of (sub)sets and restriction. The former role is taken over by elements of the Kleene algebra that are called types, whereas restriction can be modeled, as in the case of relations, by composition with a type. The paper provides the corresponding definitions and proves a number of useful properties of types and restriction. In particular, we give algebraic characterisations of the domain and codomain operations. They are presented in such a way that they can also be used for "one-sided" Kleene algebras. An instance of this is presented by the algebra of streams; there the domain of a set S of streams is the set of first letters that occur in streams in S, whereas a corresponding co-domain operation does not make sense if infinite streams occur in the set. This treatment fits well with systems such as R. Dijkstra's computation calculus [5]. We also relate the theory to the abstract treatment of assertions presented in [11]