A fundamental issue in the $\lambda$-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name $\lambda$-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the call-by-value $\lambda$-calculus (CbV). This paper validates the challenging claim that yet another notion, previously introduced in the literature as potential valuability, appropriately represents meaningfulness in CbV. Akin to CbN, this claim is corroborated by proving two essential properties. The first one is genericity, stating that meaningless subterms have no bearing on evaluating normalizing terms. To prove this (which was an open problem), we use a novel approach based on stratified reduction, indifferently applicable to CbN and CbV, and in a quantitative way. The second property concerns consistency of the smallest congruence relation resulting from equating all meaningless terms. While the consistency result is not new, we provide the first direct operational proof of it. We also show that such a congruence has a unique consistent and maximal extension, which coincides with a well-known notion of observational equivalence. Our results thus supply the formal concepts and tools that validate the informal notion of meaningfulness underlying CbN and CbV.

翻译：λ-演算中的一个基本问题是寻找适当的意义性概念。众所周知，在按名调用λ-演算（CbN）中，有意义的项可被识别为可解项，但这一概念并不适用于按值调用λ-演算（CbV）。本文验证了一个具有挑战性的主张：先前文献中引入的另一种概念——潜在可估值性——能恰当地表征CbV中的意义性。与CbN类似，这一主张通过证明两个基本性质得到证实。第一个性质是通用性，即无意义子项对正规化项的计算没有影响。为证明这一性质（此前为开放问题），我们采用了一种基于分层归约的新方法，该方法可无差别地定量应用于CbN和CbV。第二个性质涉及将所有无意义项等同化后所得最小同余关系的一致性。尽管该一致性结果并非新发现，但我们首次给出了直接的运算证明。我们还证明，该同余关系存在唯一一致的极大扩展，且该扩展与一个著名的观测等价概念相吻合。因此，我们的成果提供了验证CbN和CbV所隐含的非形式化意义性概念的形式化概念与工具。