Rewriting in the partial algebra of typed terms modulo AC

We study the partial algebra of typed terms with an associative commutative and idempotent operator (typed AC-terms). The originality lies in the representation of the typing policy by a graph which has a decidable monadic theory. In this paper we show on two examples that some results on AC-terms can be raised to the level of typed AC-terms. The examples are the results on rational languages (in particular their closure by complement) and the property reachability problem for ground rewrite systems (equivalently process rewrite systems).

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Thomas Colcombet
• Keywords: Associative Commutative, Decidable Monadic Theory, ENTCS 2002, Partial Algebra