Third-order Idealized Algol with iteration is decidable
Third-order Idealized Algol with iteration is decidable
复制标题
具有迭代的三阶理想化 Algol 可判定
DOI：
10.1016/j.tcs.2007.09.022
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
I. Walukiewicz
中科院分区：
文献类型：
--
作者：
A. Murawski;I. Walukiewicz
研究了带迭代的理想化Algol三阶片段(IA3*)的上下文等价和逼近问题。它们是通过游戏语义和语言理论的结合来实现的。结果表明，对于每个 IA3* 项，可以构造一个下推自动机，识别该项引发的策略的表示。自动机具有一些附加属性，确保相关的等价和包含问题可以在 Ptime 中解决。这给出了针对 β-正规项的上下文等价和近似问题的 Exptime 决策过程。还显示了问题的 Exptime-hardness，即使对于没有迭代的项也是如此。
The problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (IA3∗). They are approached via a combination of game semantics and language theory. It is shown that for each IA3∗-term one can construct a pushdown automaton recognizing a representation of the strategy induced by the term. The automata have some additional properties ensuring that the associated equivalence and inclusion problems are solvable in Ptime. This gives an Exptime decision procedure for the problems of contextual equivalence and approximation for β-normal terms. Exptime-hardness of the problems, even for terms without iteration, is also shown.