An Intersection Type System for Deterministic Pushdown Automata
An Intersection Type System for Deterministic Pushdown Automata
复制标题
确定性下推自动机的交集类型系统
DOI：
10.1007/978-3-642-33475-7_25
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Takeshi Tsukada
中科院分区：
文献类型：
--
作者：
Makiko Kashio;et al;加塩麻紀子;C.-H. Luke Ong;加塩麻紀子;Takeshi Tsukada
我们提出了一个通用的方法来决定上下文无关语言和确定性上下文无关语言之间的语言包含问题。我们的方法扩展了一个给定的决策过程的一个子类的另一个决策过程的一个更一般的子类称为前者的细化。为了决定，我们采取两个额外的论点：一个语言的细化，和证明。我们的技术然后精炼证明的证明或反驳。虽然加细过程一般不会终止，但我们给出了加细过程终止的一个充分条件。我们采用基于类型的方法来形式化的想法，灵感来自小林的交叉类型系统的模型检查递归计划。为了证明的有用性，我们采用这种方法来获得更简单的证明，以前的结果Minamide和Tozawa的上下文无关的语言和定期对冲语言之间的包容性，和Greibach和弗里德曼的上下文无关的语言和超确定性语言之间的包容性。
We propose a generic method for deciding the language inclusion problem between context-free languages and deterministic contextfree languages. Our method extends a given decision procedure for a subclass to another decision procedure for a more general subclass called a refinement of the former. To decide, we take two additional arguments: a languageof whichis a refinement, and a proof of. Our technique then refines the proof ofto a proof or a refutation of. Although the refinement procedure may not terminate in general, we give a sufficient condition for the termination. We employ a type-based approach to formalize the idea, inspired from Kobayashi’s intersection type system for model-checking recursion schemes. To demonstrate the usefulness, we apply this method to obtain simpler proofs of the previous results of Minamide and Tozawa on the inclusion between context-free languages and regular hedge languages, and of Greibach and Friedman on the inclusion between context-free languages and superdeterministic languages.
登录
查看更多内容
DOI：
--
发表时间：
2009
期刊：
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009)
影响因子：
--
作者：
Naoki Kobayashi;Types and Higher-Order
通讯作者：
Types and Higher-Order
上下文无关语言的某些子类的包含问题
DOI：
10.1016/s0304-3975(99)00113-9
发表时间：
1999
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
P. Asveld;A. Nijholt
通讯作者：
A. Nijholt
DOI：
10.1109/lics.2009.29
发表时间：
2009-08
期刊：
2009 24th Annual IEEE Symposium on Logic In Computer Science
影响因子：
--
作者：
N. Kobayashi;C. Ong
通讯作者：
N. Kobayashi;C. Ong
无类型递归方案和无限交集类型
DOI：
--
发表时间：
2010
期刊：
Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'10) 6014
影响因子：
--
作者：
Takeshi Tsukada;Naoki Kobayashi
通讯作者：
Naoki Kobayashi
超确定性掌上电脑
DOI：
10.1145/322217.322224
发表时间：
1980
期刊：
Journal of the ACM (JACM)
影响因子：
--
作者：
S. Greibach;E. P. Friedman
通讯作者：
E. P. Friedman