An Extension Theorem with an Application to Formal Tree Series

Authors

  • Stephen L. Bloom
  • Zoltán Ésik

DOI:

https://doi.org/10.7146/brics.v9i19.21736

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 .

Downloads

Published

2002-04-05

How to Cite

Bloom, S. L., & Ésik, Z. (2002). An Extension Theorem with an Application to Formal Tree Series. BRICS Report Series, 9(19). https://doi.org/10.7146/brics.v9i19.21736