论文标题
逐个呼声的理论（长版）
The Theory of Call-by-Value Solvability (long version)
论文作者
论文摘要
未型lambda-calculus的典型语义是一个围绕可解决术语的概念建立的良好的领域，这些术语以许多不同的方式优雅地表征。特别是，无法解决的术语提供了毫无意义的术语的一致概念。由于某些固有的困难，但由于CBV可解决的术语的研究和理解而不是逐个名称，因此逐个呼叫的lambda-calculus（CBV）的语义仍然处于起步阶段。一方面，我们表明，精心制作的CBV表现使我们能够恢复解决性在逐个名称中具有的许多属性，特别是通过多类型的定性和定量表征。另一方面，我们强调的是，在CBV中，可溶性起着不同的作用：确定毫无意义的术语会引起不一致的理论。
The denotational semantics of the untyped 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.
