论文标题
交叉类型的结构规则和代数特性
Structural Rules and Algebraic Properties of Intersection Types
论文作者
论文摘要
在本文中，我们定义了几个术语扩展的概念，用于定义以较少共享的方式定义术语，但具有相同的术语计算属性，可在相交类型系统中键入。扩展将术语与咖喱类型系统和相关类型系统键入的联想，交换性和势力相交的术语相关联，该术语是由非掌位相互作用的术语与播客类型和线性类型系统中键入的术语键入的术语，该术语是由非竞争和非交互性和非交互性交叉分类系统键入的术语类型类型的典型类型的术语。最后，我们展示了与收缩规则，与交换规则的交换相交以及与类型系统中缺乏结构规则的关联相交的交集如何相关。
In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative, commutative and idempotent intersections with terms typed in the Curry type system and the relevant type system, terms typed by non-idempotent intersections with terms typed in the affine and linear type systems and terms typed by non-idempotent and non-commutative intersections with terms typed in an ordered type system. Finally, we show how idempotent intersection is related with the contraction rule, commutative intersection with the exchange rule and associative intersection with the lack of structural rules in a type system.
