Pumping by Typing
Pumping by Typing
复制标题
通过打字进行泵送
DOI：
10.1109/lics.2013.46
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Naoki Kobayashi
中科院分区：
文献类型：
--
作者：
趙 昌熙;村上輝夫;澤江義則;中村正樹，ガイナ ダニエル ミルチェア，緒方和博，二木厚吉;Naoki Kobayashi
高阶递归方案（HORS），这是高阶文法生成无限树，最近得到了广泛的研究，在模型检测及其应用程序的高阶程序验证的背景下。我们通过使用一个新颖但简单的交叉型系统来推理λ项的约简，从而发展了HORS的泵引理。我们的证明可以说比Kartzow和帕里斯的可折叠下推自动机的泵引理的证明简单得多。作为应用，我们给出了Kartzow和帕里斯关于HORS生成的树的层次的严格性的结果的另一种证明.
Higher-order recursion schemes (HORS), which are higher-order grammars for generating infinite trees, have recently been studied extensively in the context of model checking and its applications to higher-order program verification. We develop a pumping lemma for HORS by using a novel but simple intersection type system for reasoning about reductions of λ-terms. Our proof is arguably much simpler than the proof of Kartzow and Parys' pumping lemma for collapsible pushdown automata. As an application, we give an alternative proof of Kartzow and Parys' result about the strictness of the hierarchy of trees generated by HORS.