We introduce a new kind of tree automaton, a dependency tree automaton, that is suitable for deciding properties of classes of terms with binding. Two kinds of such automaton are defined, nondeterministic and alternating. We show that the nondeterministic automata have a decidable nonemptiness problem and leave as an open question whether this is true for the alternating version. The families of trees that both kinds recognise are closed under intersection and union. To illustrate the utility of the automata, we apply them to terms of simply typed lambda calculus and provide an automata-theoretic characterisation of solutions to the higher-order matching problem.
|Title of host publication||Foundations of Software Science and Computational Structures|
|Subtitle of host publication||12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings|
|Editors||Luca de Alfaro|
|Number of pages||15|
|Publication status||Published - 2009|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|