按值调用可解性理论（长版）
The Theory of Call-by-Value Solvability (long version)
摘要：
非类型化代数演算的指称语义是围绕可解项的概念而建立的一个发展良好的领域，可解项的特征有许多不同的方式。特别是，不可解项提供了无意义项的一致概念。非类型化的按值调用演算（call-by-value calculus，CbV）的语义仍然处于起步阶段，这是由于一些固有的困难，也是因为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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
