Relational Interpretations of Recursive Types in an Operational Setting
Relational Interpretations of Recursive Types in an Operational Setting
复制标题
操作环境中递归类型的关系解释
DOI：
--
复制
发表时间：
1999
影响因子：
1
通讯作者：
R. Harper
中科院分区：
文献类型：
--
作者：
L. Birkedal;R. Harper
类型系统的关系解释对于建立编程语言的属性是有用的。对于具有递归类型的语言，很难确定关系解释的存在性。通常的方法是传递到语言的领域理论模型，并利用模型的结构来派生语言的关系属性。我们在纯操作设置中研究递归类型的关系解释的构造，借鉴领域理论和操作语义的最新思想作为指导。我们证明了具有递归类型的PCF的扩展的句法最小不变性，这是Freyd和Pitts用来表征递归类型的域解释的最小不变性性质的句法模拟。正如皮茨在域的设置中所表明的那样，句法最小不变性足以建立关系解释的存在。我们给出了这种结构的两种应用。首先，我们推导出语言表达式的逻辑等价概念，我们证明该概念与实验等价一致，并且由于其构造，验证了递归类型推理的有用归纳法和协归纳法原则。其次，我们给出了在函数式语言的编译器中使用的连续传递转换正确性的关系证明。
Abstract Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is difficult to establish the existence of a relational interpretation. The usual approach is to pass to a domain-theoretic model of the language and, exploiting the structure of the model, to derive relational properties of it. We investigate the construction of relational interpretations of recursive types in a purely operational setting, drawing on recent ideas from domain theory and operational semantics as a guide. We prove syntactic minimal invariance for an extension of PCF with a recursive type, a syntactic analogue of the minimal invariance property used by Freyd and Pitts to characterize the domain interpretation of a recursive type. As Pitts has shown in the setting of domains, syntactic minimal invariance suffices to establish the existence of relational interpretations. We give two applications of this construction. First, we derive a notion of logical equivalence for expressions of the language that we show coincides with experimental equivalence and which, by virtue of its construction, validates useful induction and coinduction principles for reasoning about the recursive type. Second, we give a relational proof of correctness of the continuation-passing transformation, which is used in some compilers for functional languages.