可解性 = 可类型化 + 居留
Solvability = Typability + Inhabitation
AI总结：
将可解性概念扩展到带模式匹配的λ-演算，证明可解性可由非幂等交集类型系统中的可类型化与居留共同完整刻画，并给出居留问题的算法。
摘要：
我们将经典的可解性概念扩展到配备模式匹配的λ-演算。我们证明，在基于非幂等类型的交集类型系统P中，可解性可以通过可类型化和居留来刻画。我们首先证明系统P刻画了具有规范形式的项集合，即一个项是可类型化的当且仅当它归约到规范形式。但可解项的集合严格包含于规范形式集合之中。因此，与λ-演算的情况不同，仅凭可类型化不足以刻画可解性。接着我们证明，可类型化与居留相结合，提供了可解性的完整刻画，即一个项是可解化的当且仅当它是可类型化的且其所有参数的类型都是可居留的。我们通过为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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
