Logical aspects in the study of tree languages

Reviewer: Robert McNaughton

This paper studies tree languages as characterized by regular expressions and monadic second-order logic. (A tree language is a set of labeled trees, just as a language is a set of words.) If t 1 and t 2 are trees and c a label of arity zero (a vertex so labeled must be a leaf node) then the concatenation t 1 ? 0S c t 2 is the result of taking a copy of t 1 and replacing each vertex labeled c by a copy of t 2. The iteration (star) t c is the set { c, t, t ? 0Sct,( t ? 0Sct) ? C ct, . . .- }. Adding to these operations all the Boolean operations and a notation for representing individual trees, we get the regular expressions over trees. A special tree is one having exactly one vertex labeled c. Most of the paper restricts itself to special trees so that concatenation and iteration resemble more closely their counterpart operations on sets of words. A tree language L is aperiodic if, for some m and all n?, s 0 ? C c( t) n ? 0Scs 1 ? L if and only if s 0 ? 0S c( t) n+1 ? C cs 1 ? L. A tree language is star-free if it is represented by a regular expression without iteration. In the symbolic-logic formalism used to write formula describing trees, each individual variable denotes a node of a tree, and each set variable denotes a set of nodes of a tree. There are the usual truth functions and quantifiers over both kinds of variable; thus the formalism is a monadic second-order logic. A tree language is first-order definable if it is represented as a formula without set variables. The paper considers two modifications of the usual semantic: in the first, set variables denote chains of nodes; in the second, they denote antichains; languages so defined are chain-definable and antichain definable, respectively. It is well known that a tree language is regular if and only if it is definable in this formalism. In this paper, examples are given of (1) tree languages that are both chain definable and antichain definable but not first-order definable, (2) chain definable tree languages that are not antichain definable, (3) antichain definable tree languages that are not chain definable, and (4) regular tree languages that are neither chain nor antichain definable. The paper culminates with the proofs of two theorems: a tree language is star-free if and only if it is antichain definable; and a chain definable tree language is aperiodic if and only if it is first-order definable.