Observable sequentiality and full abstraction
Observable sequentiality and full abstraction
复制标题
可观察的顺序性和完全抽象
DOI：
10.1145/143165.143232
复制
发表时间：
1992
影响因子：
1.8
通讯作者：
M. Felleisen
中科院分区：
文献类型：
--
作者：
Robert Cartwright;M. Felleisen
指称语义的主要挑战之一是为顺序编程语言构建完全抽象的模型。在过去的15年里，对这个问题的研究集中在为PCF开发模型上，PCF是一种基于类型化lambda演算的理想化函数式编程语言。与大多数实用语言不同，PCF没有观察和利用过程中参数的求值顺序的设施。由于我们相信，这样的设施是至关重要的理解顺序计算的性质，本文侧重于一个顺序扩展的PCF（称为SPCF），其中包括两类控制算子：错误发生器使我们能够构建一个完全抽象的模型，解释更高的类型作为错误敏感的功能，而不是连续的功能集的SPCF。错误敏感函数形成一个Scott域，该域同构于决策树的域。我们相信，同样的建设将产生完全抽象的模型，函数式语言与不同的控制操作符，以观察评估的顺序。
One of the major challenges in denotational semantics is the construction of fully abstract models for sequential programming languages. For the past fifteen years, research on this problem has focused on developing models for PCF, an idealized functional programming language based on the typed lambda calculus. Unlike most practical languages, PCF has no facilities for observing and exploiting the evaluation order of arguments in procedures. Since we believe that such facilities are crucial for understanding the nature of sequential computation, this paper focuses on a sequential extension of PCF (called SPCF) that includes two classes of control operators: error generators enable us to construct a fully abstract model for SPCF that interprets higher types as sets of error-sensitive functions instead of continuous functions. The error-sensitve functions form a Scott domain that is isomorphic to a domain of decision trees. We believe that the same construction will yield fully abstract models for functional languages with different control operators for observing the order of evaluation.