Finitary PCF is not decidable
Finitary PCF is not decidable
复制标题
有限 PCF 不可判定
DOI：
10.1016/s0304-3975(00)00194-8
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
R. Loader
中科院分区：
文献类型：
--
作者：
R. Loader
有限PCF的观测排序的可判定性问题被提出（Jung和斯托顿，在：M. Bezem，J.F. Groote（Eds.），类型λ演算和应用，计算机科学讲义，卷。664，施普林格，柏林，1993年，页。230-244）给出PCF的完全抽象问题的数学内容（米尔纳，Theoret. Comput. Sci. 4（1977）1-22）。我们证明了该排序实际上是不可判定的。这个结果限制了完全抽象模型的表示可以有多明确。它也稍微加强了作者早期关于类型λ -可定义性的结果（Loader，in：A.安德森，M. Zeleny（Eds.），教会纪念卷，Kluwer学术出版社，多尔德雷赫特，出现）。
The question of the decidability of the observational ordering of finitary PCF was raised (Jung and Stoughton, in: M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993, pp. 230–244) to give mathematical content to the full abstraction problem for PCF (Milner, Theoret. Comput. Sci. 4 (1977) 1–22). We show that the ordering is in fact undecidable. This result places limits on how explicit a representation of the fully abstract model can be. It also gives a slight strengthening of the author's earlier result on typed λ -definability (Loader, in: A. Anderson, M. Zeleny (Eds.), Church Memorial Volume, Kluwer Academic Press, Dordrecht, to appear).