Computational Adequacy via "Mixed" Inductive Definitions
Computational Adequacy via "Mixed" Inductive Definitions
复制标题
通过“混合”归纳定义的计算充分性
DOI：
--
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
A. Pitts
中科院分区：
文献类型：
--
作者：
A. Pitts
对于其指称语义使用混合方差域构造函数的不动点的编程语言，操作语义和指称语义之间（或两个不同指称语义之间）的对应性证明通常取决于指定为非单调算子的不动点的关系的存在。本文介绍了一种新的方法来构建这样的关系，避免了深入到递归定义域本身的详细建设。该方法是通过例子介绍，通过考虑在一个简单的，无类型的函数式编程语言的表达式评估的指称语义的计算充分性的证明。
For programming languages whose denotational semantics uses fixed points of domain constructors of mixed variance, proofs of correspondence between operational and denotational semantics (or between two different denotational semantics) often depend upon the existence of relations specified as the fixed point of non-monotonic operators. This paper describes a new approach to constructing such relations which avoids having to delve into the detailed construction of the recursively defined domains themselves. The method is introduced by example, by considering the proof of computational adequacy of a denotational semantics for expression evaluation in a simple, untyped functional programming language.