Observational equivalence of 3rd-order Idealized Algol is decidable
Observational equivalence of 3rd-order Idealized Algol is decidable
复制标题
三阶理想化 Algol 的观测等价性是可判定的
DOI：
10.1109/lics.2002.1029833
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
C. Ong
中科院分区：
文献类型：
--
作者：
C. Ong
利用博弈语义学证明了三阶有限理想化代数(IA)的观测等价是可判定的。通过在我们的游戏中显式地建模状态，我们证明了IA的这个片段(由有限的基类型建立)的项M的表示是一个紧凑的无辜的有状态的策略，即该策略是由一个有限的视图函数f/subM/生成的。给定任何这样的f/subM/，我们构造了一个实时确定性下推自动机(DPDA)，它识别M的已知策略表示的完全作用。由于这种作用具有观察等价性，并且有一个判定任意两个DPDA是否识别相同语言的算法，我们得到了判定三阶有限IA的观察等价性的一个过程。这种程序含义的算法表示是组合的，为对IA和其他同类编程语言的广泛行为属性进行模型检查提供了基础。另一个结果涉及二阶递归IA：我们证明了这个片段的观测等价性是不可判定的。
We prove that observational equivalence of 3rd-order finitary Idealized Algol (IA) is decidable using Game Semantics. By modelling state explicitly in our games, we show that the denotation of a term M of this fragment of IA (built up from finite base types) is a compactly innocent strategy-with-state i.e. the strategy is generated by a finite view function f/sub M/. Given any such f/sub M/, we construct a real-time deterministic pushdown automata (DPDA) that recognizes the complete plays of the knowing-strategy denotation of M. Since such plays characterize observational equivalence, and there is an algorithm for deciding whether any two DPDAs recognize the same language, we obtain a procedure for deciding observational equivalence of 3rd-order finitary IA. This algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of IA and other cognate programming languages. Another result concerns 2nd-order IA with recursion: we show that observational equivalence for this fragment is undecidable.