相交类型的有限模型性质
A Finite Model Property for Intersection Types
摘要：
我们表明，被称为BCD的交集类型的关系理论具有有限模型属性，即BCD是完全的有限模型。我们的证明使用重写技术，作为一个直接的副产品的多项式时间的可判定性的前序<=（虽然这也遵循所谓的β健全的BCD）。
英文摘要：
We show that the relational theory of intersection types known as BCD has the finite model property; that is, BCD is complete for its finite models. Our proof uses rewriting techniques which have as an immediate by-product the polynomial time decidability of the preorder <= (although this also follows from the so called beta soundness of BCD).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
