一句话：用分层归约证明 CbV 中可审查性刻画有意义项，并给出泛性与一致性结果。
本文研究 λ 演算中有意义项的刻画。CbN 中有意义项可由可解性刻画，但该概念不适用于 CbV。作者验证一个挑战性观点：文献中的 potential valuability（后称 scrutability）恰当地刻画 CbV 的有意义性。为此提出基于分层归约（stratified reduction）的新方法，可统一处理 CbN 与 CbV，并给出定量证明。关键结果有二：一是泛性，即无意义子项不影响规范化项求值，解决了此前开放问题；二是等同所有无意义项的最小同余关系具有一致性，作者给出首个直接操作证明，并证明其唯一一致极大扩展与已知观察等价重合。
A fundamental issue in the λ-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name λ-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the call-by-value λ-calculus (CbV). This paper validates the challenging claim that yet another notion, previously introduced in the literature as potential valuability (and later renamed scrutability), 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.