An Extension Theorem with an Application to Formal Tree Series

Abstract

A grove theory is a Lawvere algebraic theory T for which each hom-set T(n,p) is a commutative monoid; composition on the right distributes over all finite sums: (\sum f_i) . h = \sum f_i . h. A matrix theory is a grove theory in which composition on the left and right distributes over finite sums. A matrix theory M is isomorphic to a theory of all matrices over the semiring S = M(1,1). Examples of grove theories are theories of (bisimulation equivalence classes of) synchronization trees, and theories of formal tree series over a semiring S . Our main theorem states that if T is a grove theory which has a matrix subtheory M which is an iteration theory, then, under certain conditions, the fixed point operation on M can be extended in exactly one way to a fixed point operation on T such that T is an iteration theory. A second theorem is a Kleene-type result. Assume that T is an iteration grove theory and M is a sub iteration grove theory of T which is a matrix theory. For a given collection Sigma of scalar morphisms in T we describe the smallest sub iteration grove theory of T containing all the morphisms in M union Sigma .