Combining Equational Tree Automata over AC and ACI Theories

In this paper, we study combining equational tree automata in two different senses: (1) whether decidability results about equational tree automata over disjoint theories

${\mathcal{E}}_1$

and

${\mathcal{E}}_2$

imply similar decidability results in the

combined theory

${\mathcal{E}}_1 \cup {\mathcal{E}}_2$

; (2) checking emptiness of a language obtained from the

Boolean combination

of regular equational tree languages. We present a negative result for the first problem. Specifically, we show that the intersection-emptiness problem for tree automata over a theory containing at least one AC symbol, one ACI symbol, and 4 constants is undecidable despite being decidable if either the AC or ACI symbol is removed. Our result shows that decidability of intersection-emptiness is a

non-modular

property even for the union of disjoint theories. Our second contribution is to show a decidability result which implies the decidability of two open problems: (1) If idempotence is treated as a rule

f

(

x

,

x

) →

x

rather than an equation

f

(

x

,

x

) = 

x

, is it decidable whether an AC tree automata accepts an idempotent normal form? (2) If

${\mathcal{E}}$

contains a single ACI symbol and arbitrary free symbols, is emptiness decidable for a Boolean combination of regular

${\mathcal{E}}$

-tree languages?