Plays as Resource Terms via Non-idempotent Intersection Types
Plays as Resource Terms via Non-idempotent Intersection Types
复制标题
通过非幂等交集类型充当资源项
DOI：
10.1145/2933575.2934553
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Takeshi Tsukada and C.-H. Luke Ong
中科院分区：
文献类型：
--
作者：
Naonori Kakimura;Naoyuki Kamiyama;Kenjiro Takazawa;Takeshi Tsukada and C.-H. Luke Ong
一个程序被解释为一个集合的资源项的泰勒展开，作为一个集合的游戏的游戏语义，并作为一个集合的类型由一个非幂等交集类型分配系统。本文探讨了这些模型之间的联系，旨在表明它们在某种意义上本质上是相同的。从技术上讲，我们研究的关系解释的资源条款和播放，这可以被看作是非幂等交集型分配系统的资源条款和播放，分别。我们表明，这两个关系的解释是单射的，有相同的图像，并尊重组成。这一结果使我们能够通过使用资源演算的语法来研究博弈模型的属性，反之亦然。
A program is interpreted as a collection of resource terms by the Taylor expansion, as a collection of plays by game semantics, and as a collection of types by a non-idempotent intersection type assignment system. This paper investigates the connection between these models and aims to show that they are essentially the same in a certain sense. Technically we study the relational interpretations of resource terms and of plays, which can be seen as non-idempotent intersection type assignment systems for resource terms and plays, respectively. We show that both relational interpretations are injective, have the same image, and respect composition. This result allows us to study a property of the game model by using the syntax of a resource calculus and vice versa.