一句话：证明有界维度交集类型的可类型性在集合论与多重集模型下均可判定，并给出 PSPACE 完全与 NP 复杂度。
本文研究有界维度交集类型（intersection types）的可类型性问题。此前工作引入交集类型的维度概念，并证明有界维度 inhabitation 问题在非幂等交解释下可判定，而在标准集合论模型中不可判定。本文转而研究可类型性，证明其在集合论模型与多重集模型中均可判定。方法上，作者建立依赖维度的界原理：推导的维度界导出类型的宽度界，并获得任意项类型赋予的广义子公式性质。利用该有界宽度性质，可将可类型性问题非确定性地归约为 unification，进而证明集合论模型下可类型性是 PSPACE 完全的，多重集模型下属于 NP。
Recently (authors, POPL 2017), a notion of dimensionality for intersection types was introduced, and it was shown that the bounded-dimensional inhabitation problem is decidable under a non-idempotent interpretation of intersection and undecidable in the standard set-theoretic model. In this paper we study the typability problem for bounded-dimensional intersection types and prove that the problem is decidable in both models. We establish a number of bounding principles depending on dimension. In particular, it is shown that dimensional bound on derivations gives rise to a bounded width property on types, which is related to a generalized subformula property for typings of arbitrary terms. Using the bounded width property we can construct a nondeterministic transformation of the typability problem to unification, and we prove that typability in the set-theoretic model is PSPACE-complete, whereas it is in NP in the multiset model.