Rewriting in the partial algebra of typed terms modulo ACI

Thomas Colcombet


Abstract

We study the partial algebra of typed terms with an associative commutative and idempotent operator (typed ACI-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 ACI-terms can be simply raised to the level of typed ACI-terms. The examples are the results on rational subsets (closure by complement, decidability of the emptyness) and the property reachability problem for ground rewrite systems (equivalently process rewrite systems).