The congruence theory of closure properties of regular tree languages

AbstractBoolean operations, tree homomorphisms and their converses, and forest product, in special cases σ-catenation, x-product, x-quotient and x-iteration, preserve the regularity of forests. These closure properties are proved algebraically by using congruences of term algebras which saturate the forests operated on and constructing, by means of them, a congruence which saturates the product forest. The index of the constructed congruence is finite, if the congruences saturating the forests to operate are of finite indexes. The cardinalities of ranked and frontier alphabets are arbitrary. The preservation of recognizability is a straightforward consequence of those congruence constructions and the Nerode type of congruence characterization for recognizable forests. Furthermore, the constructed congruences can also be applied directly to construct explictly tree automatas to recognize the product forests