Dependency Tree Automata
Dependency Tree Automata
复制标题
依赖树自动机
DOI：
10.1007/978-3-642-00596-1_8
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
C. Stirling
中科院分区：
文献类型：
--
作者：
C. Stirling
我们介绍了一种新的树自动机，依赖树自动机，这是适合于确定类的条款与绑定的属性。两种类型的这样的自动机的定义，不确定性和交替。我们表明，非确定性自动机有一个可判定的非空性问题，并留下一个悬而未决的问题，这是否是真的交替版本。两种树都能识别的树族在交和并下是封闭的。为了说明自动机的实用性，我们将它们应用于简单类型的lambda演算，并提供了一个自动机理论表征的高阶匹配问题的解决方案。
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.