A fundamental issue in the $\lambda$-calculus is to find appropriate notions for meaningfulness. Inspired by well-known results for the call-by-name $\lambda$-calculus (CbN), where meaningful terms are identified to the solvable ones, this paper validates the challenging claim that the notion of potential valuability (aka scrutability), previously introduced in the literature, adequately represents meaningfulness in the call-by-value $\lambda$-calculus (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, we use a novel approach based on stratified reduction, indifferently applicable to CbN and CbV. The second property concerns consistency of the smallest congruence relation resulting from equating all meaningless terms (without equating all terms). We also show that such a congruence has a unique consistent and maximal extension, which coincides with a natural notion of observational equivalence. Our results thus supply the formal concepts and tools that validate the informal notion of meaningfulness underlying CbN and CbV.

翻译：$\lambda$-演算中的一个基本问题是寻找合适的有意义性概念。受调用名$\lambda$-演算（CbN）中众所周知的结果（其中有意义项被识别为可解项）启发，本文验证了一个具有挑战性的主张：先前文献中引入的潜在可赋值性（即可审查性）概念，在调用值$\lambda$-演算（CbV）中恰当地代表了有意义性。与CbN类似，这一主张通过证明两个基本性质得到证实。第一个性质是通用性，它指出无意义子项对正规化项的计算没有影响。为证明这一点，我们采用了一种基于分层归约的新方法，该方法可无差别地应用于CbN和CbV。第二个性质涉及将所有无意义项（但并非所有项）等同化后所得最小同余关系的一致性。我们还证明了该同余关系具有唯一的一致且最大扩展，该扩展与自然意义上的观测等价性保持一致。因此，我们的结果为验证CbN和CbV背后有意义性的非形式化概念提供了形式化概念与工具。