一句话：系统研究传值调用 λ 演算的可解性，给出多重类型刻画并指出其与传名调用的语义差异。
未类型化传名调用 λ 演算的语义以可解项为核心，不可解项可视为无意义项；而传值调用（CbV）的可解性研究仍不成熟。本文重新设计一种精细的 CbV 演算表述，借此恢复传名调用中可解性的许多性质，特别是通过 multi types（多重类型）给出定性与定量刻画。同时，作者强调 CbV 中可解性作用不同：若像传名调用那样把不可解项等同于无意义项，会导出不一致的理论。
The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.