一句话：提出高阶奇偶自动机，将奇偶树自动机推广到无穷简单类型 λ-项，并证明由 λY-项生成的项接受性可判定。
本文把经典奇偶树自动机从无穷有序树推广到无穷简单类型 λ-项，提出高阶奇偶自动机的概念。主要结果为：当无穷 λ-项由有限简单类型 λY-项生成时，该高阶奇偶自动机对它的接受性是可判定的。证明思路融合线性逻辑、指称语义与无穷重写理论：借助线性逻辑揭示 λ-项与自动机之间的对偶结构，用指称语义刻画无穷项的语义行为，并通过无穷重写理论处理归约与求值过程，从而构造出判定过程。该工作拓展了高阶模型检测与无穷项自动机理论的理论基础。
We introduce a notion of higher-order parity automaton which extends to infinitary simply-typed λ-terms the traditional notion of parity tree automaton on infinitary ranked trees. Our main result is that the acceptance of an infinitary λ-term by a higher-order parity automaton A is decidable, whenever the infinitary λ-term is generated by a finite and simply-typed λY-term. The decidability theorem is established by combining ideas coming from linear logic, from denotational semantics and from infinitary rewriting theory.