Fully Abstract Semantics for Observably Sequential Languages
Fully Abstract Semantics for Observably Sequential Languages
复制标题
可观察序列语言的完全抽象语义
DOI：
--
复制
发表时间：
1994
影响因子：
1
通讯作者：
M. Felleisen
中科院分区：
文献类型：
--
作者：
Robert Cartwright;P. Curien;M. Felleisen
指称语义的主要挑战之一是为高阶顺序程序设计语言构造完全抽象的语义。在过去的15年里，对这个问题的研究集中在为PCF开发语义，PCF是一种基于类型化λ演算的理想化函数式编程语言。与大多数实用语言不同，PCF没有观察和利用过程参数的求值顺序的设施。由于我们相信，这些设施发挥了至关重要的作用，顺序计算，本文重点介绍了PCF的顺序扩展，称为SPCF，其中包括两类控制算子：一个可能是空的错误生成器和收集的捕捉和抛出结构。对于每一组错误生成器，本文提出了一个完全抽象的语义SPCF。如果错误生成器集合为空，则语义将所有过程（包括catch和throw）解释为Berry-Curien顺序算法。如果语言包含错误生成器，则过程表示明显的顺序函数。显式序列函数形成了一个与决策树域同构的Scott域，这是序列算法的Berry-Curien域在存在错误的情况下的自然扩展。
Abstract One of the major challenges in denotational semantics is the construction of a fully abstract semantics for a higher-order sequential programming language. For the past fifteen years, research on this problem has focused on developing a semantics for PCF, an idealized functional programming language based on the typed λ-calculus. Unlike most practical languages, PCF has no facilities for observing and exploiting the evaluation order of arguments to procedures. Since we believe that these facilities play a crucial role in sequential computation, this paper focuses on a sequential extension of PCF, called SPCF, that includes two classes of control operators: a possibly empty set of error generators and a collection of catch and throw constructs. For each set of error generators, the paper presents a fully abstract semantics for SPCF. If the set of error generators is empty, the semantics interprets all procedures-including catch and throw-as Berry-Curien sequential algorithms. If the language contains error generators, procedures denote manifestly sequential functions. The manifestly sequential functions form a Scott domain that is isomorphic to a domain of decision trees, which is the natural extension of the Berry-Curien domain of sequential algorithms in the presence of errors.