交叉类型学科

在数理逻辑中，交叉类型学科是类型理论的一个分支，包括使用交叉类型构造器的类型系统。{displaystyle(/cap)}来为单个术语分配多种类型。特别是，如果一个术语(因此，相交类型构造器可以用来表达有限异构的临时多态性（与参数化多态性相反）。最引人注目的是，交叉类型系统与β还原下的λ-项的归一化属性密切相关（而且往往完全表征）。在编程语言中，如TypeScript和Scala，交叉类型被用来表达特殊的多态性。

其基本动机是通过类型理论来研究λ-微积分的语义属性（如规范化）。Coppo和Dezani的最初工作为λI微积分建立了强规范化的类型论特征，而Pottinger则将这一特征扩展到λK微积分。此外，Sallé还提出了通用类型的概念在与HenkBarendregt的合作中，我们给出了一个交集类型系统的滤波λ模型，将交集类型与λ-微积分语义更紧密地联系起来。由于与规范化的对应关系，突出交叉类型系统中的类型性（不包括通用类型）是不可解的。作为补充，PawełUrzyczyn证明了突出交叉类型系统中类型栖息的对偶问题的不可解性。

后来，这一结果被完善，显示了等级2交叉类型栖息的指数空间完整性和等级3交叉类型栖息的不可解性。值得注意的是，主要类型栖息是可以在多项式时间内解的。

λ微积分的术语语言是由λ项（或者，λ表达式）给出的。相交类型构造器(∩{displaystylecap})是根据关联性、互换性和等价性来取的。