Several extensions of tree automata have been defined, in order to take in accunt non-linearity in terms. Roughly, these automata allow equality or disequality ocnstrints between subterms. They ahve been sued to get decisio results, e.g.in term rewriting. One natural questio arises when we ocnsider a language recoginzed by such an automation: is this language recognizable, i.e. are the ocnstraints necessary? here we study this problem in the class REC= corresponding to comparions between brothers andwe prove its decidability. It gives e.g. a decision procedure for testing whether the image by a quasi-alphabetic homomorhpism of a recognizable tree language is recognizable.
展开▼
