Dependency Tree Automata

Colin Stirling

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computational Structures
Subtitle of host publication12th 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
EditorsLuca de Alfaro
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Print)978-3-642-00595-4
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Cite this