具有给定交集类型的术语集合研究
摘要：关于具有给定交集类型的项集，我们在Coppo，Dezani-Ciancaglini和Venneri [1981]的交集类型赋值系统的变种中证明了几个事实。我们的主要结果是，每个强正规化的项M都具有唯一类型，即一个对$(Gamma,A)$的一对， 1) $Gamma vdash M : A$ 2) $Gamma vdash N : A Longrightarrow M =\_{etaeta} N$ 我们还讨论了交集类型代数的几种表示以及相应的类型赋值规则的选择。 此外，我们证明了具有给定类型的闭合项集是均匀可分的，如果无限的话，形成一个充分的数字系统。证明这一事实使用了一种针对给定交集类型的项的内部B"ohm-out技术的版本。
作者：Andrew Polonsky and Richard Statman
论文ID：1809.08169
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22