  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.
