Towards kleene algebra with recursion

Abstract

We extend Kozen’s theory KA of Kleene Algebra to axiomatize parts of the equational theory of context-free languages, using a least fixed-point operator µ instead of Kleene’s iteration operator *. Although the equational theory of context-free languages is not recursively axiomatizable, there are natural axioms for subtheories KAF ⊆ KAR ⊆ KAG: respectively, these make µ a least fixed point operator, connect it with recursion, and express S. Greibach’s method to replace left- by right-recursion and vice versa. Over KAF, there are different candidates to define * in terms of µ, such as tail-recursion and reflexive transitive closure. In KAR, these candidates collapse, whence KAR uniquely defines * and extends Kozen’s theory KA. We show that a model M = (M,+,0,.,l,µ) of KAF is a model of KAG, whenever the partial order ≤ on M induced by + is complete, and + and · are Scott-continuous with respect to ≤. The family of all context-free languages over an alphabet of size n is the free structure for the class of submodels of continuous models of KAF in n generators.