Contextual isomorphisms
Contextual isomorphisms
复制标题
上下文同构
DOI：
10.1145/3009837.3009898
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Levy P
中科院分区：
文献类型：
--
作者：
Levy P
在简单的类型理论中，类型之间的“同构”的正确概念是什么？传统的答案是：一对与指定同余相反的项。我们首先认为，在存在影响的情况下，这个答案太自由了，需要加以限制，在值类型的情况下使用Führmann的可执行性概念(如在按值调用的情况下)，或在计算类型的情况下使用Munch-Maccagnon i的线性概念(如按名称调用)。然而，这给我们留下了不同类型的同构的不同概念。这种情况是通过一个新的概念来解决的，这是通过在类型层面上类似于术语的上下文对等来解决的。语境态射是一种在判决中可能出现的任何地方用另一种类型替换一种类型的方式，这种方式通过任何有洞的术语的动作来保存。对于纯λ演算类型，我们证明了上下文态射对应于传统同构。对于值类型，上下文同构对应于可转换同构，而对于计算类型，上下文同构对应于线性同构。
What is the right notion of "isomorphism" between types, in a simple type theory? The traditional answer is: a pair of terms that are inverse up to a specified congruence. We firstly argue that, in the presence of effects, this answer is too liberal and needs to be restricted, using Führmann's notion of thunkability in the case of value types (as in call-by-value), or using Munch-Maccagnoni's notion of linearity in the case of computation types (as in call-by-name). Yet that leaves us with different notions of isomorphism for different kinds of type.This situation is resolved by means of a new notion of "contextual" isomorphism (or morphism), analogous at the level of types to contextual equivalence of terms. A contextual morphism is a way of replacing one type with the other wherever it may occur in a judgement, in a way that is preserved by the action of any term with holes. For types of pure λ-calculus, we show that a contextual morphism corresponds to a traditional isomorphism. For value types, a contextual morphism corresponds to a thunkable isomorphism, and for computation types, to a linear isomorphism.
登录
查看更多内容
作为同构的参数性
影响因子：
1.1
作者：
E. Robinson
通讯作者：
E. Robinson
巨型 λ 演算
DOI：
--
发表时间：
2006
期刊：
影响因子：
--
作者：
P. Levy
通讯作者：
P. Levy
控制类别和对偶性：关于 lambda-mu 演算的分类语义
影响因子：
0.5
作者：
P. Selinger
通讯作者：
P. Selinger
偏振和聚焦线性和经典证明
影响因子：
0.8
作者：
Olivier Laurent;Myriam Quatrini;L. Falco
通讯作者：
L. Falco
类型的经典同构
影响因子：
0.5
作者：
Olivier Laurent
通讯作者：
Olivier Laurent