We study tree languages that can be denned in △{sub}2. These are tree languages definable by a first-order formula whose quantifier prefix is {exist}{sup}*{arbitrary}{sup}*, and simultaneously by a first-order formula whose quantifier prefix is {arbitrary}{sup}*{exist}{sup}*, both formulas over the signature with the descendant relation. We provide an effective characterization of tree languages definable in △{sub}2. This characterization is in terms of algebraic equations. Over words, the class of word languages definable in △{sub}2 forms a robust class, which was given an effective algebraic characterization by Pin and Weil [11].
展开▼
