An Extension Theorem with an Application to Formal Tree Series

Stephen L. Bloom
Zoltán Ésik

April 2002

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 distrbutes over all finite sums: $(\sum_{i \in F} f_i) · h= \sum_{i \in F} 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 fixedpoint operation on $T$ such that $T$ is an iteration theory. A second theorem is a Kleene-type result. Assume that $T$ is a 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 \cup \Sigma$

Available as PostScript, PDF, DVI.

Last modified: 2003-06-08 by webmaster.