交叉类型学科

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

交叉类型学科

编辑

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

交叉类型学科的历史

编辑

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

交叉类型学科

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

术语语言

编辑

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

内容由匿名用户提供,本内容不代表vibaike.com立场,内容投诉举报请联系vibaike.com客服。如若转载,请注明出处:https://vibaike.com/170749/

(2)
词条目录
  1. 交叉类型学科
  2. 交叉类型学科的历史
  3. 术语语言

轻触这里

关闭目录

目录
全球百科疯狂618活动进行中→点击传送门