The Meaning of Types From Intrinsic to Extrinsic Semantics
The Meaning of Types From Intrinsic to Extrinsic Semantics
复制标题
从内在语义到外在语义的类型含义
DOI：
--
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
J. C. Reynolds
中科院分区：
文献类型：
--
作者：
J. C. Reynolds
如果一个类型化语言的定义给类型化而不是任意的短语赋予意义，那么它就是“内在的”，因此类型化不好的短语是没有意义的。相反，如果所有短语都有独立于其类型的含义，而类型代表这些含义的属性，则定义被称为“外在的”。对于一个简单类型的lambda演算，扩展与递归，子类型，命名产品，我们给出了一个内在的指称语义和指称语义的底层无类型的语言。然后，我们建立了这两个语义之间的逻辑关系定理，并表明，逻辑关系可以“括号”的两个语义域之间的撤回。从这些结果中，我们得出一个外在的语义，使用部分等价关系。
A definition of a typed language is said to be "intrinsic" if it assigns meanings to typings rather than arbitrary phrases, so that ill-typed phrases are meaningless. In contrast, a definition is said to be "extrinsic" if all phrases have meanings that are independent of their typings, while typings represent properties of these meanings. For a simply typed lambda calculus, extended with recursion, subtypes, and named products, we give an intrinsic denotational semantics and a denotational semantics of the underlying untyped language. We then establish a logical relations theorem between these two semantics, and show that the logical relations can be "bracketed" by retractions between the domains of the two semantics. From these results, we derive an extrinsic semantics that uses partial equivalence relations.