Categorical models for local names
Categorical models for local names
复制标题
本地名称的分类模型
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
I. Stark
中科院分区：
文献类型：
--
作者：
I. Stark
本文描述了u演算的范畴模型的构造，u演算是一种将高阶函数与动态创建的名称相结合的语言。名字是在局部作用域中创建的，它们可以相互比较，并通过函数应用程序传递，但仅此而已。这种语言背后的意图是研究标准ML的命令式特征的一个方面：通过动态创建引用来使用局部状态。nu演算等价于ML的某个片段，省略了副作用、异常、数据库和递归。即使没有所有这些特征，名称创建与高阶函数的交互也可能是复杂而微妙的;特别是难以描述表达式的可观察行为。Moggi风格的分类单子被用来为nu演算构建指称模型。一个中间阶段是使用计算元语言，它在类型系统中区分值和计算。提出了分类模型的一般要求，并详细描述了两个具体的例子。这些为nu演算提供了一个合理的指称语义，并且可以用来推理语言中的可观察等价。特别地，使用逻辑关系的模型对于一阶表达式是完全抽象的。
This paper describes the construction of categorical models for thenu-calculus, a language that combines higher-order functions with dynamically creatednames. Names are created with local scope, they can be compared with each other and passed around through function application, but that is all.The intent behind this language is to examine one aspect of the imperative character of Standard ML: the use of local state by dynamic creation of references. The nu-calculus is equivalent to a certain fragment of ML, omitting side effects, exceptions, datatypes and recursion. Even without all these features, the interaction of name creation with higher-order functions can be complex and subtle; it is particularly difficult to characterise theobservable behaviour of expressions.Categorical monads, in the style of Moggi, are used to build denotational models for the nu-calculus. An intermediate stage is the use of a computational metalanguage, which distinguishes in the type system between values and computations.The general requirements for a categorical model are presented, and two specific examples described in detail. These provide a sound denotational semantics for the nu-calculus, and can be used to reason about observable equivalence in the language. In particular a model using logical relations is fully abstract for first-order expressions.