Tree acceptors and some of their applications

摘要

This paper concerns a generalization of finite automata, the “tree acceptors,” which have as their inputs finite trees of symbols rather than the usual sequences of symbols. Ordinary finite automata prove to be special cases of tree acceptors, and many of the results of finite automata theory continue to hold in their appropriately generalized forms. The tree acceptors provide new characterizations of the classes of regular sets and of context-free languages. The theory of tree acceptors is applied to a decision problem of mathematical logic. It is shown here that the weak secondorder theory of two successors is decidable, thus settling a problem of Buchi. This result is in turn applied to obtain positive solutions to the decision problems for various other theories, e.g., the weak second-order theories of order types built up from the finite types, ω, and η (the type of the rationals) by finitely many applications of the operations of order type addition, multiplication, and converse; and the weak second-order theory of locally free algebras with only unary operations.