Tree algebras and varieties of tree languages

We consider several aspects of Wilke’s [T. Wilke, An algebraic characterization of frontier testable tree languages, Theoret. Comput. Sci. 154 (1996) 85–106] tree algebra formalism for representing binary labelled trees and compare it with approaches that represent trees as terms in the traditional way. A convergent term rewriting system yields normal form representations of binary trees and contexts, as well as a new completeness proof and a computational decision method for the axiomatization of tree algebras. Varieties of binary tree languages are compared with varieties of tree languages studied earlier in the literature. We also prove a variety theorem thus solving a problem noted by several authors. Syntactic tree algebras are studied and compared with ordinary syntactic algebras. The expressive power of the language of tree algebras is demonstrated by giving equational definitions for some well-known varieties of binary tree languages.