Proof nets and the instantiation overflow property
Proof nets and the instantiation overflow property
复制标题
证明网和实例化溢出属性
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Paolo Pistone
中科院分区：
文献类型：
--
作者：
Paolo Pistone
实例化溢出是那些二阶类型的属性，对于这些二阶类型，完全理解的所有实例都可以从原子理解的实例中推导出来。换句话说，当可以通过原子多态性键入实现应用于该类型的完整提取规则的实例的“扩展项”时，该类型具有实例化溢出。这一性质是在由著名的罗素-普拉维茨翻译逻辑连接词到系统F中所产生的类型的情况下进行研究的，但并不局限于这样的类型。此外，它可以与函子多态性有关，函子多态性是系统F中参数性的一种众所周知的范畴方法。在本文中，我们研究的实例溢出性质，利用表示的派生通过线性逻辑证明网。我们开发了一个几何的方法，实例化溢出产生更深入的理解的结构的扩展条款和拉塞尔-Prawitz类型。我们的主要结果是通过Russell-Prawitz类型的推广，对$forall XA$形式的类型类进行了表征，其中$A$是一个简单类型，它享有实例化溢出属性。
Instantiation overflow is the property of those second order types for which all instances of full comprehension can be deduced from instances of atomic comprehension. In other words, a type has instantiation overflow when one can type, by atomic polymorphism, "expansion terms" which realize instances of the full extraction rule applied to that type. This property was investigated in the case of the types arising from the well-known Russell-Prawitz translation of logical connectives into System F, but is not restricted to such types. Moreover, it can be related to functorial polymorphism, a well-known categorial approach to parametricity in System F. In this paper we investigate the instantiation overflow property by exploiting the representation of derivations by means of linear logic proof nets. We develop a geometric approach to instantiation overflow yielding a deeper understanding of the structure of expansion terms and Russell-Prawitz types. Our main result is a characterization of the class of types of the form $forall XA$, where $A$ is a simple type, which enjoy the instantiation overflow property, by means of a generalization of Russell-Prawitz types.
自然演绎的自然性
影响因子：
0.7
作者：
Luca Tranchini;Mattia Petrolo;Paolo Pistone
通讯作者：
Paolo Pistone