Principal Type Scheme and Unification for Intersection Type Discipline
Principal Type Scheme and Unification for Intersection Type Discipline
复制标题
主要类型方案和交叉类型规则的统一
DOI：
10.1016/0304-3975(88)90101-6
复制
发表时间：
1988
期刊：
影响因子：
--
通讯作者：
S. D. Rocca
中科院分区：
文献类型：
--
作者：
S. D. Rocca
λ-演算的交型规则（ITD）是咖喱的经典泛函理论的推广.在ITD中，满足给定性质的术语具有扩展含义的主类型方案，即，存在一个可推导的类型概型，通过适当的运算，从该类型概型中，所有且只有可推导的类型概型是可达的。如果一个项的主类型模式存在，那么找到它的问题是半判定的。本文给出了通过构造交型概型的最一般的统一子来构造项的主型概型的过程。
The intersection type discipline for the λ-calculus (ITD) is an extension of the classical functionality theory of Curry. In the ITD a term satisfying a given property has a principal type scheme in an extended meaning, i.e., there is a type scheme deducible for it from which all and only the type schemes deducible for it are reachable, by means of suitable operations. The problem of finding the principal type scheme for a term, if it exists, is semidecidable. In the paper a procedure is shown, building the principal type scheme of a term through the construction of the most general unifier for intersection type schemes.