完全交叉类型理论的完整刻画
摘要：关于lambda演算的完全交集类型分配系统，我们对于三个基本的集合论语义：推理语义、简单语义和F-语义，对产生这些交集类型的交集类型理论进行了描述。这些语义通过将类型的解释视为适用结构的子集，将交集构造器的解释视为集合论的包含关系，并根据Scott的箭头构造器的解释，从任意可能的功能集、最大功能集或最小功能集中选择。 这些结果在至少三个方面加强和推广了文献中所有早期结果的我们所知。首先，推理语义以前没有被考虑过。其次，这些特征只是通过对类型上的预序关系进行简单的闭包条件给出，而不是对类型判断本身给出。因此，检查条件的任务变得更加可行。最后，我们不仅局限于lambda模型，而是适用于任何允许有解释函数的适用结构。因此，我们还可以处理限制的lambda演算模型。 Complete Intersection-Type Assignment Systems for Lambda-Calculi with Respect to Set-Theoretical Semantics
作者：M. Dezani-Ciancaglini, F. Honsell and F. Alessi
论文ID：cs/0011039
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23