一句话：证明非幂等交类型用于刻画可解与强规范化 lambda 项的若干赋值系统中，居留问题均可判定。
交类型在 lambda 演算中的居留问题已知不可判定。本文研究非幂等交类型情形，考察多个类型赋值系统，这些系统分别刻画可解（solvable）的 lambda 项或强规范化（strongly normalizing）的 lambda 项。作者为每个所考虑的系统构造居留算法，并证明这些算法可靠且完备，由此确立所有系统的居留问题可判定。这一结果给出了非幂等交类型下 inhabitation 的判定边界，并与一般交类型情形形成对照。
The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the decidability of the inhabitation problem for all the systems considered, by providing sound and complete inhabitation algorithms for them.
@article{paperbot389,
title = {Inhabitation for Non-idempotent Intersection Types},
author = {Antonio Bucciarelli and Delia Kesner and Simona Ronchi Della Rocca},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:7)2018}
}