Rewriting in the partial algebra of typed terms modulo AC

AbstractWe 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)