Collapsing non-idempotent intersection types
Collapsing non-idempotent intersection types
复制标题
折叠非幂等交集类型
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
T. Ehrhard
中科院分区：
文献类型：
--
作者：
T. Ehrhard
最近我们证明了线性逻辑关系模型的外延崩溃与它的Scott模型重合，该模型的对象是前序，态射是向下的闭关系。这一结果是通过构造一个新的模型得到的，该模型的对象可以理解为带有可实现性谓词的前序。我们提出了这个模型，它具有一个新的对偶性，并解释了如何利用它将幂等交类型(通常由可归约性证明)的归一化结果归结为纯组合方法。我们在按值调用lambda演算的情况下说明了这种方法，我们为其引入了一个新的资源演算，但它可以以相同的方式应用于许多不同的演算。
We proved recently that the extensional collapse of the relational model of linear logic coincides with its Scott model, whose objects are preorders and morphisms are downwards closed relations. This result is obtained by the construction of a new model whose objects can be understood as preorders equipped with a realizability predicate. We present this model, which features a new duality, and explain how to use it for reducing normalization results in idempotent intersection types (usually proved by reducibility) to purely combinatorial methods. We illustrate this approach in the case of the call-by-value lambda-calculus, for which we introduce a new resource calculus, but it can be applied in the same way to many different calculi.