一句话：将可解性推广到带模式匹配的 lambda 演算，并证明其恰由非幂等交类型的可类型性与居留性刻画。
论文研究带模式匹配的 lambda 演算中的可解性（solvability）。作者将其经典定义推广到该演算，并引入基于非幂等交类型的类型系统 P。首先证明 P 恰好刻画具有规范形（canonical form）的项：项可类型当且仅当它能归约到规范形。但可解项集合是规范形集合的真子集，因此与纯 lambda 演算不同，仅靠可类型性不足以刻画可解性。进一步证明，项可解当且仅当它可类型，且其所有参数的类型均居留（inhabited），从而得到“可类型性 + 居留性”的完整刻画。最后给出系统 P 居留性问题的判定算法。
We extend the classical notion of solvability to a lambda-calculus equipped with pattern matching. We prove that solvability can be characterized by means of typability and inhabitation in an intersection type system P based on non-idempotent types. We show first that the system P characterizes the set of terms having canonical form, i.e. that a term is typable if and only if it reduces to a canonical form. But the set of solvable terms is properly contained in the set of canonical forms. Thus, typability alone is not sufficient to characterize solvability, in contrast to the case for the lambda-calculus. We then prove that typability, together with inhabitation, provides a full characterization of solvability, in the sense that a term is solvable if and only if it is typable and the types of all its arguments are inhabited. We complete the picture by providing an algorithm for the inhabitation problem of P.
@article{paperbot1344,
title = {Solvability = Typability + Inhabitation},
author = {Antonio Bucciarelli and Delia Kesner and Simona Ronchi Della Rocca},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:7)2021}
}