# Genericity Through Stratification

Victor Arrial  0000-0002-1607-7403 Université Paris Cité, CNRS,
IRIFParisFrance ,  Giulio Guerrieri  0000-0002-0469-4279 Aix Marseille Univ,
CNRS, LISMarseilleFrance and  Delia Kesner  0000-0003-4254-3129 Université
Paris Cité, CNRS, IRIFParisFrance

(2024; 20 February 2007; 12 March 2009; 5 June 2009)

###### Abstract.

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.

Lambda-calculus, solvability, genericity

††copyright: acmcopyright††journalyear: 2024††doi:
XXXXXXX.XXXXXXX††conference: Thirty-Ninth Annual ACM/IEEE Symposium on Logic
in Computer Science; 8–12 July 2024; Tallinn, Estonia††price: 15.00††isbn:
978-1-4503-XXXX-X/18/06††ccs: Mathematics of computing Lambda calculus

##  1\. Introduction

#### Meaningfulness and Meaninglessness

One of the aims of programming language theory is to establish semantics
describing the meaning of computer programs (see (Hutton, 2023) for a survey).
It is then natural to search for criteria that distinguish, among
syntactically correct (i.e. compiling) programs, the meaningful ones (those
computing something) from the meaningless ones (those not computing anything,
for instance because they always diverge for every input).

In the context of the pure untyped $\lambda$-calculus (the prototypical kernel
common to all functional programming languages and many proof assistants),
this question has been extensively studied since the 70s (Scott, 1970; Scott
and Strachey, 1971; Barendregt, 1971; Wadsworth, 1971; Scott, 1972; Hyland,
1975; Wadsworth, 1976; Barendregt92a). Setting up a semantic for the
$\lambda$-calculus amounts to fixing an _equivalence_ relation $\equiv$ on
$\lambda$-terms, with the underlying intuition that two equivalent
$\lambda$-terms share the _same meaning_. Two primary requirements for
$\equiv$ must be considered:

  1. (1)

_Invariance under computation:_ $\equiv$ must include $\beta$-equivalence
$=_{\beta}$, which is the reflexive, symmetric and transitive closure of
$\beta$-reduction. In other words, if $t=_{\beta}u$ then $t\equiv u$. Roughly,
if $t=_{\beta}u$ then $t$ and $u$ have a common $\beta$-reduct (by the Church-
Rosser theorem), meaning that $t$ and $u$ represent different stages of the
same computation and thus share the same meaning.

  2. (2)

_Compositionality:_ $\equiv$ must be preserved when plugging $\lambda$-terms
into the same context, i.e. if $t\equiv u$ then
$\mathtt{C}\\!\left<t\right>\equiv\mathtt{C}\\!\left<u\right>$ for every
context $\mathtt{C}$. Essentially this means that the meaning of a compound
$\lambda$-term is defined solely by the meaning of its subterms.

Equivalence relations fulfilling Items 1 and 2 are usually called _$\lambda$
-theories_ (Barendregt and Manzonetto, 2022). In programming language theory,
there are at least three more desiderata for them:

  1. (3)

_Consistency:_ Equivalence $\equiv$ must not equate all $\lambda$-terms, i.e.
$t\not\equiv u$ for at least two $\lambda$-terms $t$ and $u$, otherwise the
semantics would be trivial and convey no information.

  2. (4)

_Sensibility:_ All meaningless $\lambda$-terms should be equated by $\equiv$.
Essentially, there should be no semantic difference between two
$\lambda$-terms that have no meaning!

  3. (5)

_Genericity:_ Meaningless subterms are computationally irrelevant —in the
sense that they do not play any role— in the evaluation of $\beta$-normalizing
$\lambda$-terms

Genericity says that a meaningless subterm $t$ of a $\beta$-normalizing term
$\mathtt{C}\\!\left<t\right>$ does not impact on the computation from
$\mathtt{C}\\!\left<t\right>$ to its $\beta$-normal form $u$, and hence $t$ is
_generic_ , that is, it can be replaced by any other $\lambda$-term $s$ and
still $\mathtt{C}\\!\left<s\right>$ $\beta$-reduces to $u$.

A $\lambda$-theory gives insights into denotational and operational semantics
of the $\lambda$-calculus, e.g. it may stem from a denotational model (by
equating exactly the $\lambda$-terms with the same interpretation), or may
reflect a particular observational equivalence (by equating exactly the
observationally equivalent $\lambda$-terms). Two $\lambda$-terms $t$ and $u$
are _observationally equivalent_ with respect to a notion of observable if
$\mathtt{C}\\!\left<t\right>$ reduces to an observable exactly when
$\mathtt{C}\\!\left<u\right>$ does. In programming language theory, this is a
way to determine when programs can be considered equivalent as they have the
same behavior.

#### A Naive Notion of Meaningfulness

A naive approach to set a semantics for the pure untyped $\lambda$-calculus is
to define the meaning of a $\beta$-normalizing $\lambda$-term as its normal
form, and equating all $\lambda$-terms that do not $\beta$-normalize. The
underlying idea is that, as $\beta$-reduction represents evaluation and a
normal form stands for its outcome, all _non_ -$\beta$-normalizing
$\lambda$-terms are considered as meaningless (intuitively, they represent
non-terminating programs).

Evidence that this naive approach to semantics is flawed is that it equates
every fixed point combinator (any $\lambda$-term $Y$ such that
$t(Yt)=_{\beta}t$ for every $\lambda$-term $t$) with the prototypical
diverging $\lambda$-term $\Omega=(\lambda x.xx)\lambda x.xx$. While both $Y$
and $\Omega$ fail to $\beta$-normalize, the former is essential for
representing recursive functions in the $\lambda$-calculus, suggesting it
should carry some non-trivial semantics, while $\Omega$ is indisputably
meaningless. This suggests the idea that the $\beta$-normalizing
$\lambda$-terms are not the only meaningful $\lambda$-terms.

Indeed, as thoroughly discussed in (Barendregt, 1984, Chapter 2), the naive
approach has some major drawbacks. In particular, any $\lambda$-theory
equating all non-$\beta$-normalizing $\lambda$-terms is _inconsistent_ : it
equates all $\lambda$-terms, not just the meaningless ones!

#### Solvable as meaningful

In the 70s, Wadsworth (Wadsworth, 1971, 1976) and Barendregt (Barendregt,
1971, 1973, 1977, 1984) showed that the meaningful $\lambda$-terms can be
identified with the _solvable_ ones. The definition of solvability seems
technical: a $\lambda$-term $t$ is _solvable_ if there is a special kind of
context, called _head_ context $\mathtt{H}$, sending $t$ to the identity
function $\mathtt{I}=\lambda z.z$, meaning that $\mathtt{H}\\!\left<t\right>$
$\beta$-reduces to $\mathtt{I}$. Roughly, a solvable $\lambda$-term $t$ may be
divergent, but its diverging subterms can be removed via interaction with a
suitable head context $\mathtt{H}$ which cannot merely discard $t$. For
instance, $x\Omega$ is divergent but solvable (take the head context
$\mathtt{H}=(\lambda x.\diamond)\lambda y.\mathtt{I}$). It turns out that
_unsolvable_ $\lambda$-terms constitutes a strict subset of the
non-$\beta$-normalizing ones (notably all fixed point combinators are
solvable). Moreover, the smallest $\lambda$-theory that equates all unsolvable
$\lambda$-terms —let us call it $\mathcal{H}$— is _consistent_ (Item 3).
Following the key idea in Barendregt’s book (Barendregt, 1984), if we identify
_solvable as meaningful_ , and hence  _unsolvable as meaningless_ , we have
that:

  * •

The $\lambda$-theory $\mathcal{H}$ gives rise to a _sensible_ semantics (Item
4), and

  * •

_Genericity_ holds (Item 5), meaning that if $t$ is _unsolvable_ and
$\mathtt{C}\\!\left<t\right>$ $\beta$-reduces to _some_ $\beta$-normal term
$u$ for some context $\mathtt{C}$, then $\mathtt{C}\\!\left<s\right>$
$\beta$-reduces to $u$ for _every_ $\lambda$-term $s$.

Not only is genericity an interesting operational property _per se_ , but it
is also a crucial ingredient to prove consistency of $\mathcal{H}$ in a
_direct way_ (not relying on consistency of other $\lambda$-theories),
following (Barendregt, 1984).

The fact that Items 3, 4 and 5 hold is the main rationale for embracing
solvability as a formal representation of the informal notion of
meaningfulness in the pure untyped $\lambda$-calculus, as extensively
discussed in (Barendregt, 1984). This semantic approach gives rise to an
elegant and successful theory of the $\lambda$-calculus, see (Wadsworth, 1971;
Barendregt, 1971, 1973, 1977; Wadsworth, 1976; Coppo and Dezani-Ciancaglini,
1978, 1980; Barendregt, 1984; Barendregt92a; Barendregt and Manzonetto, 2022).

#### Call-by-Name & Call-by-Value

Solvability has been extensively studied in the standard pure untyped
$\lambda$-calculus, which we refer to as _call-by-name_ (CbN for short). This
approach does not require the argument to be evaluated before being passed to
the calling function. In the 70s, Plotkin (Plotkin, 1975) introduced the
_call-by-value_ (CbV, for short) variant of the pure untyped
$\lambda$-calculus, which is closer to actual implementation of functional
programming languages and proof assistants. The key distinction lies in its
reduction rule $\beta_{v}$: a restriction of $\beta$-reduction that allows a
redex to be fired only when the argument is a _value_ , that is, a variable or
an abstraction. Among $\lambda$-theories, we distinguish _$\lambda_{n}$
-theories_ (for CbN) and _$\lambda_{v}$ -theories_ (for CbV) if their
invariance is under $\beta$\- and $\beta_{v}$-reduction, respectively.

It is tempting to adapt the notion of solvability to CbV, by simply replacing
$\beta$-reduction with $\beta_{v}$-reduction in its definition. It has been
proved that CbV solvability has appealing properties (Paolini and Ronchi Della
Rocca, 1999; Rocca and Paolini, 2004; Accattoli and Paolini, 2012; Carraro and
Guerrieri, 2014; Guerrieri et al., 2017; Accattoli and Guerrieri, 2022).
Unfortunately, as it is well-known, any $\lambda_{v}$-theory (Items 1 and 2)
that equates all CbV unsolvable $\lambda$-terms (Item 4) cannot be consistent
(Item 3), see e.g. (Accattoli and Guerrieri, 2022). Furthermore, Accattoli and
Guerrieri (Accattoli and Guerrieri, 2022) have showed that genericity (Item 5)
fails for CbV unsolvable $\lambda$-terms. Therefore, meaningfulness in CbV
cannot be identified with CbV solvability, unless we are willing to relinquish
to the desired properties outlined in Items 3, 4 and 5. Identifying
appropriate notions to capture CbV meaningful $\lambda$-terms and formally
validating these notions is a longstanding and challenging open question.

#### Our First Contribution: Scrutable as Meaningful in CbV

Facing these negative results, our paper investigates the notion of
meaningfulness in CbV using a different approach, in the vein of what
Barendregt (Barendregt, 1984) did for CbN. Indeed, we look for a suitable of
CbV meaningfulness such that the smallest $\lambda_{v}$-theory it _generates_
(according to Items 4, 1 and 2) fulfills the other desired properties (Items 3
and 5).

Paolini and Ronchi Della Rocca (Paolini and Ronchi Della Rocca, 1999; Rocca
and Paolini, 2004) introduced the notion of _potentially valuability_ for CbV,
also studied in (Paolini et al., 2006; Accattoli and Paolini, 2012; Carraro
and Guerrieri, 2014; García-Pérez and Nogueira, 2016) and renamed _(CbV)
scrutability_ in (Accattoli and Guerrieri, 2022): a $\lambda$-term is
_scrutable_ if there is a _head_ context $\mathtt{H}$ sending $t$ to some
value, that is, such that $\mathtt{H}\\!\left<t\right>$ _$\beta_{v}$ -reduces_
to some value. Scrutable $\lambda$-terms form a _proper superset_ of the CbV
solvable ones, for instance $\lambda x.\Omega$ is scrutable but not CbV
solvable. Akin to CbV solvability, scrutability has appealing
characterizations (Paolini and Ronchi Della Rocca, 1999; Rocca and Paolini,
2004; Paolini et al., 2006; Accattoli and Paolini, 2012; Carraro and
Guerrieri, 2014; Guerrieri et al., 2017; Accattoli and Guerrieri, 2022). But
there is more than that. Indeed, one of the main contributions of our paper is
to prove that we can identify _scrutable as CbV meaningful_ , and hence
_inscrutable as CbV meaningless_ , in that we prove the following properties:

  * •

_Genericity_ (Item 5): in CbV, if $t$ is _CbV meaningless_ and
$\mathtt{C}\\!\left<t\right>$ reduces to a normal form $u$ for some context
$\mathtt{C}$, then $\mathtt{C}\\!\left<s\right>$ reduces to $u$ for every
$\lambda$-term $s$;

  * •

_Consistency_ (Item 3): the smallest $\lambda_{v}$-theory (Items 1 and 2) that
equates all CbV meaningless $\lambda$-terms (Item 4) is consistent.

The main and non-trivial challenge is to prove genericity, conjectured but not
proved in (Accattoli and Guerrieri, 2022). Concerning consistency, it is
already proved in the literature —or can be easily derived— from the
consistency of some related $\lambda_{v}$-theories (Egidi et al., 1992;
Paolini and Ronchi Della Rocca, 1999; Carraro and Guerrieri, 2014; Accattoli
and Guerrieri, 2022; Accattoli and Lancelot, 2024). But we provide the first
direct operational proof of consistency, using genericity.

#### Our Second Contribution: Stratified Genericity, Modularly

We claim that our approach to prove genericity is _finer_ than the ones in the
literature, and above all _robust_ , in that it indifferently applies to CbN
and CbV in a modular way.

Why our approach is finer? What is called genericity in the literature, is
called here _full genericity_ , because it is about the behavior of
meaningless $\lambda$-terms that are plugged in _full_ contexts (i.e. contexts
without any restriction) when they reduce to _full_ normal forms (i.e. normal
forms for unrestricted reduction). We also study _non-full_ genericity, by
considering non-full contexts and non-full normal forms, which amounts to
looking at contexts and normal forms until a certain _depth_. Thus, a natural
notion of _stratified genericity_ arises, depending on how deep we consider
contexts and normal forms. Our approach proves stratified genericity for _any_
depth, the full case (the usual one considered in the literature) being only a
special case where there is no limit to the depth. Another special case is
_surface genericity_ , that is, stratified genericity where the depth is $0$.

Moreover, our approach does not only bring forward _qualitative_ aspects of
genericity, but also _quantitative_ ones: if $t$ is meaningless and
$\mathtt{C}\\!\left<t\right>$ normalizes to $u$ for some context $\mathtt{C}$
in $m$ steps, then $\mathtt{C}\\!\left<s\right>$ normalizes to $u$ for _every_
$\lambda$-term $s$ in exactly $m$ steps. Thus, $t$ is not only qualitative
irrelevant, but also quantitatively irrelevant.

#### Our third contribution: $\mathcal{H}$ and $\mathcal{H}^{*}$ in CbV

The literature on $\lambda_{n}$-theories (for CbN) is vast (Barendregt, 1984;
Barendregt92a; Berline, 2000; Berline et al., 2007, 2009; Breuvart, 2014;
Breuvart et al., 2016; Barendregt and Manzonetto, 2022), and the set of
$\lambda_{n}$-theories forms a very rich mathematical structure. In
particular, the aforesaid $\mathcal{H}$ has a unique maximal consistent
extension called $\mathcal{H}^{*}$ (Hyland, 1975).

Concerning CbV, instead, the study of $\lambda_{v}$-theories is still in its
early stages (Egidi et al., 1992; Rocca and Paolini, 2004; Accattoli and
Guerrieri, 2022), also because of the intricacies of CbV semantics. We already
mentioned that the smallest $\lambda_{v}$-theory equating all CbV meaningless
$\lambda$-terms is consistent. As a further contribution, thanks again to
genericity, we prove that such a $\lambda_{v}$-theory has a unique maximal
consistent extension, which coincides with a well known notion of CbV
observational equivalence (Plotkin, 1975), the one where the notion of
observable is to reduce to some value.

All these results in CbV are perfectly analogous to well known results for CbN
(Hyland, 1975; Barendregt, 1984; Barendregt and Manzonetto, 2022), suggesting
that there is a sort of _canonicity_ in the proposal to identify CbV
meaningfulness with scrutability.

#### Methodological Remark

In this paper, we do not work in the standard CbN (CHURCH, 1941) and CbV
(Plotkin, 1975) $\lambda$-calculi, but in their respective variants with
_explicit substitution_ s and reduction _at a distance_ (Accattoli and Kesner,
2010; Accattoli and Paolini, 2012). Indeed, our technique for both CbN and CbV
relies on an existing _operational characterization_ of meaningfulness: a
$\lambda$-term $t$ is meaningful if and only if a _certain_ reduction starting
at $t$ terminates. Such a reduction is given by the notion of _head reduction_
for CbN (Wadsworth, 1971, 1976), which is _internal_ to the calculus (a
subreduction of $\beta$). For CbV, instead, it is not possible to have an
operational characterization of meaningfulness internally to Plotkin’s
original CbV $\lambda$-calculus, as already remarked by Paolini and Ronchi
Della Rocca (Paolini and Ronchi Della Rocca, 1999; Rocca and Paolini, 2004).
This weakness of Plotkin’s CbV is widely accepted in the literature on CbV,
which provides many alternative proposals to extend CbV (Grégoire and Leroy,
2002; Accattoli and Paolini, 2012; Carraro and Guerrieri, 2014; Accattoli and
Guerrieri, 2016; Herbelin and Zimmermann, 2009) in such a way that an internal
characterization of scrutability becomes possible. Among them we chose the
formalism in (Accattoli and Paolini, 2012), called here dCBV, as it has good
rewriting properties. For uniformity, we also took its CbN version (Accattoli
and Kesner, 2012).

#### Outline

Section 2 presents the dCBV-Calculus and a first result of (qualitative)
surface genericity. A general methodology to prove quantitative full
genericity is introduced in Section 3, and we instantiate it to the dCBV-
Calculus in Section 4. Call-by-name genericity is developed in Section 5,
still using the methodology proposed in Section 3. Section 6 presents the
results of consistency and sensibility for the associated theories. Section 7
discusses related works and concludes. Omitted proofs are in the Appendix.

##  2\. The dCBV-Calculus

This section introduces the syntax and operational semantics of the dCBV-
calculus, including the new notion of _stratified reduction_ (a key ingredient
of our approach). We also recall the $\mathcal{V}$ type system (Bucciarelli et
al., 2020), another key tool in this work. Adequacy of the dCBV-calculus
versus non-adequacy of Plotkin’s CbV is also discussed, to justify the use of
dCBV. At the end of the section, a first qualitative surface genericity result
(Section 2) is obtained thanks to the type system.

#### Syntax

We present the syntax of the dCBV Calculus, a call-by-value $\lambda$-calculus
with explicit substitutions originally introduced in (Accattoli and Paolini,
2012), where it is called the _Value Substitution Calculus_. Given a countably
infinite set $\mathcal{X}$ of variables $x,y,z,\dots$, the sets of terms
($\Lambda$) and values ($\Upsilon$) are given by the following inductive
definitions:

$\begin{array}[]{r rcl}\textbf{(Terms)}&{\tt
t},u&\;\Coloneqq&v\;|\;tu\;|\;t[x\backslash u]\\\
\textbf{(Values)}&v&\;\Coloneqq&x\in\mathcal{X}\;|\;\lambda x.t\end{array}$

The set $\Lambda$ includes variables $x$, abstractions $\lambda x.t$,
applications $tu$ and closures $t[x\backslash u]$, the latter representing a
pending explicit substitution (ES) $[x\backslash u]$ on $t$. Terms without ES
are called ES-free. Abstractions $\lambda x.t$ and closures $t[x\backslash u]$
bind the variable $x$ in $t$.

The set of free variables ${\tt fv}(t)$ of a term $t$ is defined as expected,
in particular ${\tt fv}(\lambda x.t)={\tt fv}(t)\backslash\\{x\\}$ and ${\tt
fv}(t[x\backslash u])={\tt fv}(u)\cup({\tt fv}(t)\backslash\\{x\\})$. The
usual notion of $\alpha$-conversion (Barendregt, 1984) is extended to the
whole set $\Lambda$, and terms are identified up to $\alpha$-conversion. For
example $x[x\backslash\lambda y.y]=z[z\backslash\lambda x.x]$. We denote by
$t\\{x\backslash u\\}$ the term obtained by the usual (capture-avoiding) meta-
level substitution of the term $u$ for all free occurrences of the variable
$x$ in the term $t$.

###### Notation 0.

We set $\mathtt{I}\coloneqq\lambda x.x$ and $\Delta\coloneqq\lambda x.xx$ and
$\Omega\coloneqq\Delta\Delta$.

#### (Stratified) Contexts and Equality

The operational semantics of dCBV is often specified by means of a _weak_
reduction relation (Accattoli and Paolini, 2012) that forbids evaluation under
abstractions, called here _surface_ reduction. In this work however, we equip
dCBV with a much finer _stratified_ operational semantics which generalizes
surface reduction to different _levels_. For example, given a term $t=\lambda
x.(u_{1}(\lambda y.u_{2}))$, reduction at level $1$ allows to evaluate inside
one binder $\lambda$, but not inside two or more, so that $u_{1}$ can be
evaluated while $u_{2}$ cannot. This extended semantics sheds a light on the
layering intrinsically standing out in the study of meaningfulness. From now
on, we denote by $\mathbb{N}^{\omega}$ the set $\mathbb{N}\cup\\{\omega\\}$
(with $i<\omega$ for all $i\in\mathbb{N}$), which will be used to index all
the forthcoming notions with respect to a level.

To define such stratified operational semantics, we need a fine-grained notion
of context (a terms containing exactly one hole $\diamond$). The set of list
contexts $(\mathtt{L})$ and stratified contexts $(\mathtt{V}_{k})$ for
$k\in\mathbb{N}^{\omega}$ are inductively defined as follows (where
$i\in\mathbb{N}$):

$\begin{array}[]{c}\begin{array}[]{rcl}\mathtt{L}&\;\Coloneqq&\diamond\;|\;\mathtt{L}[x\backslash
t]\\\\[5.69046pt]
\mathtt{V}_{0}&\;\Coloneqq&\diamond\;|\;\mathtt{V}_{0}\,t\;|\;t\,\mathtt{V}_{0}\;|\;\mathtt{V}_{0}[x\backslash
t]\;|\;t[x\backslash\mathtt{V}_{0}]\\\
\mathtt{V}_{i+1}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathtt{V}_{i}\;|\;\mathtt{V}_{i+1}\,t\;|\;t\,\mathtt{V}_{i+1}\;|\;\mathtt{V}_{i+1}[x\backslash
t]\;|\;t[x\backslash\mathtt{V}_{i+1}]\\\
\mathtt{V}_{\omega},\mathtt{C}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathtt{V}_{\omega}\;|\;\mathtt{V}_{\omega}\,t\;|\;t\,\mathtt{V}_{\omega}\;|\;\mathtt{V}_{\omega}[x\backslash
t]\;|\;t[x\backslash\mathtt{V}_{\omega}]\end{array}\end{array}$

A stratified context is _ES-free_ if it is without ES. Special cases of
stratified contexts are surface contexts (whose hole is not in the scope of
any $\lambda$) and full contexts (the restriction-free one-hole contexts, also
denoted by $\mathtt{C}$): the former (resp. the latter) are stratified
contexts for the minimal (resp. transfinite) level, i.e. $\mathtt{V}_{0}$
(resp. $\mathtt{V}_{\omega}$). In a stratified context $\mathtt{V}_{k}$, the
hole can occur everywhere as long as its depth is at most $k$, so that in
$\mathtt{V}_{\omega}$ the hole can occur everywhere and in $\mathtt{V}_{0}$ it
cannot occur under any abstraction. Thus for example $y\,(\lambda x.\diamond)$
is in $\mathtt{V}_{1}$, and thus in every $\mathtt{V}_{k}$ with $k\geq 1$,
including $\mathtt{V}_{\omega}$, but it is not in $\mathtt{V}_{0}$. For all
$k\in\mathbb{N}^{\omega}$, we write $\mathtt{V}_{k}\\!\left<t\right>$ for the
term obtained by replacing the hole in $\mathtt{V}_{k}$ with the term $t$, and
similarly for $\mathtt{L}$.

We define the stratified equality comparing terms up to a given depth by the
following inductive rules (where $k\in\mathbb{N}^{\omega}$ and
$i\in\mathbb{N})$:

$\begin{array}[]{c}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
2.16647pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
var})$}}}\hbox{\hbox{\hbox{}\hbox{$\phantom{\overset{\scriptscriptstyle
i}{\approx}}\hfil\lx@intercol$}}\hbox{$x\overset{\scriptscriptstyle
k}{\approx}x$}}\par}\par}}}$}\hskip
11.38092pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\\!\scriptsize$({\tt app})$}}}\hbox{\hskip
1.8633pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t_{1}\overset{\scriptscriptstyle
k}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle
k}{\approx}u_{2}$}}}}\hbox{$t_{1}t_{2}\overset{\scriptscriptstyle
k}{\approx}u_{1}u_{2}$}}}\par}\par}}}$}\hskip
11.38092pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
14.78416pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
es})$}}}\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t_{1}\overset{\scriptscriptstyle
k}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle
k}{\approx}u_{2}$}}}}\hbox{$t_{1}[x\backslash
t_{2}]\overset{\scriptscriptstyle k}{\approx}u_{1}[x\backslash
u_{2}]$}}\par}\par}}}$}\\\\[11.38092pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
9.5289pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\scriptsize$({\tt
abs})$}}}\hbox{\hbox{\hbox{}\hbox{$\phantom{t\overset{\scriptscriptstyle
k}{\approx}u}\hfil\lx@intercol$}}\hbox{$\lambda x.t\overset{\scriptscriptstyle
0}{\approx}\lambda y.u$}}\par}\par}}}$}\hskip
22.76228pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
17.82805pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
abs})$}}}\hbox{\hbox{\hbox{}\hbox{$t\overset{\scriptscriptstyle
i}{\approx}u$}}\hbox{$\lambda x.t\overset{\scriptscriptstyle
i+1}{\approx}\lambda x.u$}}\par}\par}}}$}\hskip
22.76228pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
12.41142pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
abs})$}}}\hbox{\hbox{\hbox{}\hbox{$t\overset{\scriptscriptstyle\omega}{\approx}u$}}\hbox{$\lambda
x.t\overset{\scriptscriptstyle\omega}{\approx}\lambda
x.u$}}\par}\par}}}$}\end{array}$

Notice that $t\overset{\scriptscriptstyle\omega}{\approx}u$ if and only if
$t=u$.

###### Example 2.1.

Let $t_{0}:=(\lambda x.x(\lambda y.x))z$ and $t_{1}:=(\lambda x.x(\lambda
z.z))z$. We have $t_{0}\overset{\scriptscriptstyle 0}{\approx}t_{1}$ and
$t_{0}\overset{\scriptscriptstyle 1}{\approx}t_{1}$ but not
$t_{0}\overset{\scriptscriptstyle k}{\approx}t_{1}$ for any $k\geq 2$.

#### (Stratified) Operational Semantics.

The notions of contexts already established, we can now equip dCBV with an
operational semantics. The following rewriting rules are the base components
of such operational semantics. Any term having the shape of the left-hand side
of one of these three rules is called a redex.

$\begin{array}[]{c c c}\mathtt{L}\\!\left<\lambda x.s\right>t\;\mapsto_{{\tt
dB}}\;\mathtt{L}\\!\left<s[x\backslash
t]\right>&&t[x\backslash\mathtt{L}\\!\left<v\right>]\;\mapsto_{{\tt
sV}}\;\mathtt{L}\\!\left<t\\{x\backslash v\\}\right>\end{array}$

Rules ${\tt dB}$ and ${\tt sV}$ are assumed to be _capture free_ , so no free
variable of $t$ is captured by the context $\mathtt{L}$. The ${\tt dB}$-rule
fires a $\beta$-redex (with no restriction on the argument $t$) and generates
an ES. The ${\tt sV}$-rule encapsulates the call-by-value behavior: it fires
an ES provided that its argument is a _value_ $v$, possibly wrapped in a list
context $\mathtt{L}$. In both rewrite rules, reduction acts _at a distance_
(Accattoli and Kesner, 2010): the main constructors involved in the rule can
be separated by a finite—possibly empty—list $\mathtt{L}$ of ES. This
mechanism unblocks redexes that otherwise would be stuck, e.g. $(\lambda
x.x)[y\backslash zz]v\mapsto_{{\tt dB}}x[x\backslash v][y\backslash zz]$ fires
a $\beta$-redex by taking $\mathtt{L}=\diamond[y\backslash zz]$ as the list
context in between the function $\lambda x.x$ and the argument $v$. Another
example is $(xx)[x\backslash\mathtt{I}[y\backslash zz]]\mapsto_{{\tt
sV}}(\mathtt{I}\mathtt{I})[y\backslash zz]$ which substitutes the value
$\mathtt{I}$ for the variable $x$ by pushing out the list context
$\mathtt{L}=\diamond[y\backslash zz]$.

The $\mathrm{v}_{k}$-stratified reduction $\rightarrow_{\mathrm{v}_{k}}$ is
the $\mathtt{V}_{k}$-closure of the two rewriting rules $\mapsto_{{\tt dB}}$
and $\mapsto_{{\tt sV}}$. In particular, $\rightarrow_{\mathrm{v}_{0}}$ (resp.
$\rightarrow_{\mathrm{v}_{\omega}}$) is called surface (resp. full) reduction.
We write $\rightarrow^{*}_{\mathrm{v}_{k}}$ for the reflexive and transitive
_closure_ of the reduction $\rightarrow_{\mathrm{v}_{k}}$, and
$\rightarrow^{i}_{\mathrm{v}_{k}}$ (with $i\in\mathbb{N}$) for the
_composition_ $i$ times of $\rightarrow_{\mathrm{v}_{k}}$. As an example,
consider

$\begin{array}[]{l}\lambda x.\big{(}\lambda y.xw\big{)}[w\backslash\lambda
z.\Omega]\;\rightarrow_{\mathrm{v}_{2}}\;\lambda x.\lambda y.\big{(}x\,\lambda
z.\Omega\big{)}\\\ \hskip 14.22636pt\;\rightarrow_{\mathrm{v}_{3}}\;\lambda
x.\lambda y.\big{(}x\,\lambda
z.((ww)[w\backslash\Delta])\big{)}\;\rightarrow_{\mathrm{v}_{3}}\;\lambda
x.\lambda y.\big{(}x\,\lambda z.\Omega\big{)}\end{array}$

The first and third reduction steps are ${\tt sV}$-steps while the second is a
${\tt dB}$-step. Moreover, the first step is indeed a
$\rightarrow_{\mathrm{v}_{k}}$-step for any $k\geq 2$. However, the second and
third steps are not $\rightarrow_{\mathrm{v}_{k}}$-steps for $0\leq k\leq 2$.
In general,
$\rightarrow_{\mathrm{v}_{i}}\,\subsetneq\,\rightarrow_{\mathrm{v}_{i+1}}\,\subsetneq\,\rightarrow_{\mathrm{v}_{\omega}}$
for all $i\in\mathbb{N}$. For $k\notin\\{0,\omega\\}$,
$\mathrm{v}_{k}$-stratified reduction is not confluent.

###### Lemma 2.2 ((Accattoli and Paolini, 2012)).

The dCBV surface and full reductions are confluent.

#### Normal Forms.

A term $t$ is $\mathrm{v}_{k}$-normal (or a $\mathrm{v}_{k}$-normal form),
noted ${\tt NF}_{\mathrm{v}_{k}}(t)$, if there is no $u$ such that
$t\rightarrow_{\mathrm{v}_{k}}u$. Note that ${\tt NF}_{\mathrm{v}_{i+1}}(t)$
implies ${\tt NF}_{\mathrm{v}_{i}}(t)$. A term $t$ is a surface (resp. full)
normal form if it is $\mathrm{v}_{0}$-normal (resp.
$\mathrm{v}_{\omega}$-normal). A term $t$ is $\mathrm{v}_{k}$-normalizing if
$t\rightarrow^{*}_{\mathrm{v}_{k}}u$ for some $\mathrm{v}_{k}$-normal form
$u$. In particular, a term $t$ is surface (resp. full) normalizing if it is
$\mathrm{v}_{0}$-normalizing (resp. $\mathrm{v}_{\omega}$-normalizing). Since
$\rightarrow_{\mathrm{v}_{i}}\subsetneq\rightarrow_{\mathrm{v}_{i+1}}$, then
some terms may be $\rightarrow^{*}_{\mathrm{v}_{i}}$-normalizing but not
$\rightarrow^{*}_{\mathrm{v}_{i+1}}$-normalizing, e.g. $\lambda x.((\lambda
z.xy)[y\backslash\lambda w.\Omega])$ is $\mathrm{v}_{0}$, $\mathrm{v}_{1}$ and
$\mathrm{v}_{2}$-normalizing but not $\mathrm{v}_{3}$-normalizing. As a
consequence, there are terms that are surface but not full normalizing.

Normal forms can be _syntactically_ characterized by the following grammar
${\tt no}_{\mathrm{v}_{k}}$ ($k\in\mathbb{N}^{\omega}$), where the subgrammar
${\tt ne}_{\mathrm{v}_{k}}\ (k\in\mathbb{N}^{\omega})$ generates special
normal forms called _neutral_ , which never create a redex when applied to an
argument.

$\begin{array}[]{rcl}{\tt vr}_{\mathrm{v}_{k}}&\coloneqq&x\;|\;{\tt
vr}_{\mathrm{v}_{k}}[x\backslash{\tt ne}_{\mathrm{v}_{k}}]\\\\[5.69046pt] {\tt
ne}_{\mathrm{v}_{k}}&\coloneqq&{\tt vr}_{\mathrm{v}_{k}}\,{\tt
no}_{\mathrm{v}_{k}}\;|\;{\tt ne}_{\mathrm{v}_{k}}\,{\tt
no}_{\mathrm{v}_{k}}\;|\;{\tt ne}_{\mathrm{v}_{k}}[x\backslash{\tt
ne}_{\mathrm{v}_{k}}]\\\\[5.69046pt] {\tt
no}_{\mathrm{v}_{0}}&\coloneqq&\lambda x.t\;|\;{\tt
vr}_{\mathrm{v}_{0}}\;|\;{\tt ne}_{\mathrm{v}_{0}}\;|\;{\tt
no}_{\mathrm{v}_{0}}[x\backslash{\tt ne}_{\mathrm{v}_{0}}]\\\ {\tt
no}_{\mathrm{v}_{i+1}}&\coloneqq&\lambda x.{\tt no}_{\mathrm{v}_{i}}\;|\;{\tt
vr}_{\mathrm{v}_{i+1}}\;|\;{\tt ne}_{\mathrm{v}_{i+1}}\;|\;{\tt
no}_{\mathrm{v}_{i+1}}[x\backslash{\tt
ne}_{\mathrm{v}_{i+1}}]\;(i\in\mathbb{N})\\\ {\tt
no}_{\mathrm{v}_{\omega}}&\coloneqq&\lambda x.{\tt
no}_{\mathrm{v}_{\omega}}\;|\;{\tt vr}_{\mathrm{v}_{\omega}}\;|\;{\tt
ne}_{\mathrm{v}_{\omega}}\;|\;{\tt no}_{\mathrm{v}_{\omega}}[x\backslash{\tt
ne}_{\mathrm{v}_{\omega}}]\end{array}$

lemmaCbvNoSnCharacterization Let $k\in\mathbb{N}^{\omega}$. Then $t\in\Lambda$
is $\mathrm{v}_{k}$-normal iff $t\in{\tt no}_{\mathrm{v}_{k}}$.

#### Quantitative Types.

We now present the quantitative typing system $\mathcal{V}$, originally
introduced in (Ehrhard, 2012) for the $\lambda$-calculus and extended to dCBV
in (Bucciarelli et al., 2020). It contains functional and intersection types.
Intersection is considered to be associative, commutative but not idempotent,
thus an intersection type is represented by a (possibly empty) finite multiset
$\left[\sigma_{i}\right]_{i\in I}$. Formally, given a countably infinite set
$\mathcal{TV}$ of type variables $\alpha,\beta,\gamma,\dots$, we inductively
define:

$\begin{array}[]{rcl}\sigma,\tau,\rho&\Coloneqq&\alpha\in\mathcal{TV}\;|\;\mathcal{M}\;|\;\mathcal{M}\Rightarrow\sigma\\\
\mathcal{M}&\Coloneqq&\left[\sigma_{i}\right]_{i\in I}\ (I\mbox{
finite})\end{array}$

The typing rule of system $\mathcal{V}$ are defined as follows:

$\begin{array}[]{ccc}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
29.04854pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\scriptsize$({\tt
var})$}}}\hbox{\hbox{\hbox{}\hbox{}}\hbox{$x:\mathcal{M}\vdash
x:\mathcal{M}\hfil\lx@intercol$}}\par}\par}}}$}\hskip
14.22636pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
7.0024pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\scriptsize$({\tt abs})$}}}\hbox{\hbox{\hbox{}\hbox{\lower
1.94444pt\hbox{\hbox{$\left(\vrule
height=8.88889pt,depth=0.0pt,width=0.0pt\right.$}$\left.\hbox{$\vbox{\hbox{\hbox{}\hbox{\hbox{$\Pi_{i}\triangleright_{\mathcal{V}}\mathrel{}$}$\mathrel{}\Gamma_{i};x:\mathcal{M}_{i}\vdash
t:\sigma_{i}$}}}$}\right)_{i\in I}$}}}\hbox{\hbox{$\;\;+_{i\in
I}\Gamma_{i}\mathrel{}$}$\mathrel{}\vdash\lambda
x.t:\left[\mathcal{M}_{i}\Rightarrow\sigma_{i}\right]_{i\in
I}\;\;$}}\par}\par}}}$}\\\\[14.22636pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\scriptsize$({\tt app})$}}}\hbox{\hskip
6.2569pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1}\vdash
t:\left[\mathcal{M}\Rightarrow\sigma\right]\hfil\lx@intercol$}}\hbox{$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash
u:\mathcal{M}$}}}}\hbox{$\Gamma_{1}+\Gamma_{2}\vdash
tu:\sigma$}}}\par}\par}}}$}\\\\[14.22636pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
4.10071pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\scriptsize$({\tt
es})$}}}\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1};x:\mathcal{M}\vdash
t:\sigma\hfil\lx@intercol$}}\hbox{$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash
u:\mathcal{M}$}}}}\hbox{$\Gamma_{1}+\Gamma_{2}\vdash t[x\backslash
u]:\sigma$}}\par}\par}}}$}\end{array}$

with $I$ finite in rule $({\tt abs})$. A (type) derivation is a tree obtained
by applying the (inductive) typing rules of system $\mathcal{V}$. The notation
$\Pi\triangleright_{\mathcal{V}}\Gamma\vdash t:\sigma$ means there is a
derivation of the judgment $\Gamma\vdash t:\sigma$ in system $\mathcal{V}$. We
say that $t$ is $\mathcal{V}$-typable if
$\Pi\triangleright_{\mathcal{V}}\Gamma\vdash t:\sigma$ holds for some
$\Gamma,\sigma$. For example, the term $\lambda x.yz$ is typable with the
context$\Gamma=y:\left[\left[\,\right]\Rightarrow\alpha\right],z:\left[\,\right]$
and type $\alpha$, as illustrated below.

(1) $({\tt abs})$ $({\tt app})$ $({\tt abs})$ $({\tt var})$
$y:\left[\left[\,\right]\Rightarrow\alpha\right]\vdash
y:\left[\left[\,\right]\Rightarrow\alpha\right]$ $\vdash\lambda
z.\Omega:\left[\,\right]$
$y:\left[\left[\,\right]\Rightarrow\alpha\right]\vdash y(\lambda
z.\Omega):\alpha$
$y:\left[\left[\,\right]\Rightarrow\alpha\right]\vdash\lambda x.y(\lambda
z.\Omega):\left[\left[\,\right]\Rightarrow\alpha\right]$

System $\mathcal{V}$ _characterizes_ surface normalization (see Lemma 2.4).

#### Meaningfulness.

Meaningfulness is about the possibility to differentiate operationally
relevant terms from those that are irrelevant. Operational relevance can be
understood as the ability, under appropriate circumstances, to produce some
element that is _observable_ within the corresponding language. Scrutability
in dCBV (Accattoli and Guerrieri, 2022) aligns precisely with this principle.
Throughout this paper, call-by-value scrutability is called _meaningfulness_.
Formally,

###### Definition 2.3.

A term $t\in\Lambda$ is said dCBV-meaningful if there exists a testing context
$\mathtt{T}$ and a value $v\in\Upsilon$ such that
$\mathtt{T}\\!\left<t\right>\rightarrow^{*}_{\mathrm{v}_{0}}v$, where testing
contexts are defined by
$\mathtt{T}\;\Coloneqq\;\diamond\;|\;\mathtt{T}\,u\;|\;(\lambda
x.\mathtt{T})\,u$.

The intuition behind meaningfulness is that values are the observable elements
in call-by-value, while testing contexts $\mathtt{T}$ supply arguments to
their plugged term, possibly binding them to variables. For example
$t=x(\lambda y.z)$ is meaningful as
$\mathtt{T}\\!\left<t\right>\rightarrow^{*}_{\mathrm{v}_{0}}\lambda y.z$ for
$\mathtt{T}=(\lambda x.\diamond)(\lambda z.z)$, while $\Omega$ and $x\Omega$
are meaningless as for whatever testing context $\Omega$ and $x\Omega$ are
plugged into, $\Omega$ will not be erased.

Meaningfulness can be characterized _operationally_ , through the notion of
surface-normalization, and _logically_ , through typability in type system
$\mathcal{V}$. The logical characterization of meaningfulness plays a central
role in this work as it yields the initial genericity result (Section 2) upon
which all the other results are founded.

###### Lemma 2.4 (dCBV Meaningful Characterizations (Accattoli and Paolini,
2012; Accattoli and Guerrieri, 2022; Bucciarelli et al., 2020)).

Let $t\in\Lambda$. Then the following characterizations hold:

  * (Operational)

$t$ is dCBV-meaningful iff $t$ is dCBV surface-normalizing.

  * (Logical)

$t$ is dCBV-meaningful iff $t$ is $\mathcal{V}$-typable.

####  Adequacy of the dCBV-Calculus.

Plotkin’s seminal work (Plotkin, 1975) established the foundations and key
concepts about the _call-by-value_ $\lambda$-calculus (_CbV_). The syntax of
Plotkin’s CbV is based on ES-free terms. Using the notations introduced above,
the reduction relations $\rightarrow_{\mathrm{pv}_{0}}$ and
$\rightarrow_{\mathrm{pv}_{\omega}}$ in Plotkin’s CbV are the closures under
ES-free surface and full contexts, of the _${\tt\beta_{v}}$ -rule_ below:

$(\lambda x.t)\,v\;\mapsto_{{\tt\beta_{v}}}\;t\\{x\backslash
v\\}\quad\text{where $v$ is a ES-free\ value}$

For example, $(\lambda x.x)\lambda y.z\rightarrow_{\mathrm{pv}_{0}}\lambda
y.z$ and $\lambda x.((\lambda y.z)x)\rightarrow_{\mathrm{pv}_{\omega}}\lambda
x.z$. As expected, $\rightarrow^{*}_{\mathrm{pv}_{\omega}}$ denotes the
reflexive-transitive closure of $\rightarrow_{\mathrm{pv}_{\omega}}$. It is
straightforward to see that reduction in Plotkin’s CbV can be easily simulated
by reductions in dCBV. The converse fails (hence dCBV reduces _more_ that
Plotkin’s CbV), even when considering ES-free terms: take $t\coloneqq(\lambda
x.\Delta)(yy)\Delta$, where $\delta\coloneqq\lambda z.zz$. Note that $\lambda
x.\Delta$ is applied to $yy$ —which is not a value and cannot reduce to a
value— so $t$ is normal in Plotkin’s CbV, but it diverges in dCBV:

$\displaystyle t\rightarrow_{\mathrm{v}_{0}}{\Delta}[x\backslash
yy]\Delta\rightarrow_{\mathrm{v}_{0}}(zz)[z\backslash\Delta][x\backslash
yy]\rightarrow_{\mathrm{v}_{0}}\Delta\Delta[x\backslash
yy]\rightarrow_{\mathrm{v}_{0}}\dots$

Concerning the notion of meaningfulness, it can be adapted to Plotkin’s CbV: a
ES-free term is Plotkin-meaningful if there is a testing context $\mathtt{T}$
and a ES-free value $v$ such that
$\mathtt{T}\\!\left<t\right>\rightarrow^{*}_{\mathrm{pv}_{0}}v$.

Plotkin (Plotkin, 1975) also introduced the notion of _observational
equivalence_ to identify ES-free terms having the same behavior. Two ES-free
terms $t,u$ are observationally equivalent in Plotkin’s CbV, noted
$t\cong^{p}u$, if for every ES-free full context $\mathtt{C}$ such that
$\mathtt{C}\\!\left<t\right>$ and $\mathtt{C}\\!\left<u\right>$ are _closed_ ,
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{pv}_{\omega}}v_{1}$ iff
$\mathtt{C}\\!\left<u\right>\rightarrow^{*}_{\mathrm{pv}_{\omega}}v_{2}$ for
some ES-free values $v_{1},v_{2}$. This notion can be naturally extended to
ES: two terms $t,u\in\Lambda$ are observationally equivalent in dCBV, noted
$t\cong u$, if for every full context $\mathtt{C}$ such that
$\mathtt{C}\\!\left<t\right>$ and $\mathtt{C}\\!\left<u\right>$ are _closed_ ,
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{v}_{\omega}}v_{1}$ iff
$\mathtt{C}\\!\left<u\right>\rightarrow^{*}_{\mathrm{v}_{\omega}}v_{2}$ for
some values $v_{1},v_{2}$. Accattoli and Guerrieri (Accattoli and Guerrieri,
2022) proved that the notions of meaningfulness and observational equivalence
coincide in Plotkin’s CbV and dCBV.

###### Lemma 2.5 ((Accattoli and Guerrieri, 2022)).

Let $t,u$ be two ES-free terms.

  * •

Observational equivalence in Plotkin and dCBV coincide.

  * •

$t$ is Plotkin-meaningful if and only if $t$ is dCBV-meaningful.

Thus, the semantic notions of meaningfulness and observational equivalence are
_robust_ in CbV, they do not depend on the syntactic formulation of the
calculus (Plotkin’s or dCBV). Said differently, dCBV is _conservative_ with
respect to Plotkin’s CbV: it does not change its semantics. However, there is
a crucial difference between Plotkin’s CbV and dCBV. As Paolini and Ronchi
Della Rocca (Paolini and Ronchi Della Rocca, 1999) first observed (see also
(Rocca and Paolini, 2004; Accattoli and Paolini, 2012; Carraro and Guerrieri,
2014; Accattoli and Guerrieri, 2016, 2022)), Plotkin’s CbV is not _adequate_ :

  1. (1)

observational equivalence may equate terms having different operational
behaviors in Plotkin’s CbV, normal form and a diverging term, e.g.
$t\coloneqq(\lambda x.\Delta)(yy)\Delta$ seen above is normal, but
$t\cong\Delta\Delta$ and $\Delta\Delta$ is diverging;

  2. (2)

meaningfulness cannot be characterized operationally inside Plotkin’s CbV, for
instance again the term $t\coloneqq(\lambda x.\Delta)(yy)\Delta$ seen above is
normal for Plotkin, but meaningless.

The inadequacy of Plotkin’s CbV is due to _open_ terms, that is, terms
containing free variables (such as $t$ above). Indeed, Plotkin’s CbV works
well only when reduction is _weak_ (it does not go under abstractions) and
restricted to _closed_ terms (without free variables): this is enough to
properly model evaluation of functional programs. But Plotkin’s does not model
adequately proof-assistants (Grégoire and Leroy, 2002), where evaluation
proceeds under abstraction, and hence on possibly (locally) open terms. On the
contrary, dCBV is adequate because meaningfulness can be characterized
operationally inside the calculus (Lemma 2.4) and observational equivalence
does not equate terms with a different operational behavior (Section 6).

#### Surface Genericity.

Genericity can be stated in various ways, according to the previous different
characterizations of meaningfulness (Lemma 2.4). As we shall see, an
operational presentation of genericity is more informative than a logical one,
it particularly allows for the extraction of quantitative information of the
reduction sequences to normal form, as well as observational information about
these normal forms. Nonetheless, proving logical genericity, called here
_typed genericity_ , is a more straightforward endeavor (just an induction on
full contexts), so that we start with it.

[dCBV Typed Genericity]lemmaCbvSurfaceTypedGenericity Let $t\in\Lambda$ be
dCBV-meaningless. If
$\Pi\triangleright_{\mathcal{V}}\Gamma\vdash\mathtt{C}\\!\left<t\right>:\sigma$,
then there is
$\Pi^{\prime}\triangleright_{\mathcal{V}}\Gamma\vdash\mathtt{C}\\!\left<u\right>:\sigma$
for all $u\in\Lambda$.

For instance, in the derivation (1), we can replace $\Omega$, which is dCBV-
meaningless, with any $u\in\Lambda$ without changing any type.

The logical characterization of meaningfulness (Lemma 2.4) together with the
previous dCBV Typed Genericity result suffice to derive the following first
(weak) surface genericity theorem.

[dCBV Qualitative Surface Genericity]theoremRecCbvQualitativeSurfaceGenericity
Let $t\in\Lambda$ be dCBV-meaningless. If $\mathtt{C}\\!\left<t\right>$ is
dCBV-meaningful then $\mathtt{C}\\!\left<u\right>$ is also dCBV-meaningful for
all $u\in\Lambda$.

###### Proof.

Let $t$ be dCBV-meaningless and $\mathtt{C}\\!\left<t\right>$ be dCBV-
meaningful. By LABEL:{lem:cbvBKRV_characterizes_meaningfulness},
$\mathtt{C}\\!\left<t\right>$ is $\mathcal{V}$-typable. By Section 2,
$\mathtt{C}\\!\left<u\right>$ is also $\mathcal{V}$-typable, hence
$\mathtt{C}\\!\left<u\right>$ is dCBV-meaningful by
LABEL:{lem:cbvBKRV_characterizes_meaningfulness}. ∎

These preliminary outcomes will be further bolstered and refined in the
subsequent sections of the paper: on one hand we will prove full genericity,
as explained in Section 1, on the other hand, we will enrich the genericity
property quantitatively.

##  3\. Towards Full Genericity: Key Tools

In this paper, we prove genericity results for dCBV and dCBN, starting from
_qualitative surface genericity_ up to _quantitative stratified genericity_ ,
thus including full genericity as a particular case, an important result for
the theory of call-by-value that has never been proved before. All these
results stand upon a first _typed genericity_ result (Section 2) that we
swiftly proved using the existing logical characterization of meaningfulness
in (Accattoli and Guerrieri, 2022) (Lemma 2.4). For the rest of our results,
we use a technique based on some additional key ingredients that we discuss in
what follows. We use a _generic_ vocabulary “calculus”, “stratified context”,
“stratified reduction”, etc, the intention being that the same methodology
will be applied to call-by-value (Section 4) and to call-by-name (Section 5).

####  Specifying Unknown Subterms: Meaningful Approximants.

The set of terms $\Lambda$ of the calculus is extended with a new constant
$\bot$ representing an _unknown piece of term_. The resulting set of _partial
terms_ is noted ${\bf\Lambda}$, using bold font. All the previous notions are
lifted consequently: partial stratified contexts, partial stratified
reduction, partial normalization, etc. They are all defined as conservative
extensions to partial elements of their underlying original ones.

Partial terms are endowed with a _partial order_ $\leq$, defined as the
partial full context closure of the relation $\bot\leq\mathbf{t}$, for all
$\mathbf{t}\in{\bf\Lambda}$. Intuitively, $\mathbf{t}\leq\mathbf{u}$ means
that $\mathbf{u}$ carries more information than $\mathbf{t}$.

We use the partial calculus to abstract from meaningless subterms. For that
purpose, for each term $t$ we construct its _meaningful approximant_
$\mathcal{MA}(t)$, a partial term obtained by replacing all meaningless
subterms of $t$ with $\bot$. As expected, $\mathcal{MA}(t)$
(under-)approximates $t$, in that $\mathcal{MA}(t)\leq t$. Meaningful
approximants are the cornerstone of our approach: they will be used as
intermediary stakeholders to transfer a reduction sequence between two terms
into another reduction sequence between two other related terms.

####  Axioms.

The method used to derive quantitative stratified genericity from the
preliminary typed genericity result incorporates all the previously mentioned
elements, in addition to some general statements on the partial calculus and
meaningful approximants. These statements, called _axioms_ , _uniformly_
outline the prerequisites that are necessary for achieving quantitative and
full genericity from qualitative and surface genericity. Nonetheless, they
require validation for each individual calculus, given that their suitability
is closely tied to their respective concept of stratified reduction.

We now detail the four axioms. Our approach strongly relies on the operational
characterization of meaningfulness. Thus, all the axioms are related to
reduction sequences and normal forms.

Numerous natural approaches exist to extend a given calculus into some
corresponding partial calculus (Sections 4.1 and 5.2). However, not all of
these methods consistently allow for an accurate approximation of the
calculus’s dynamic behavior. What we mean by this is the capacity to relate
reductions in the calculus to those occurring in its partial counterpart, and
vice versa.

We assume that $k$-reduction sequences on terms can be approximated by means
of $k$-reduction sequences on meaningful approximants. Ideally, this means
that $t\rightarrow_{k}u$ implies
$\mathcal{MA}(t)\rightarrow_{k}\mathcal{MA}(u)$. However, this is not always
true in our frameworks, and it is sufficient to approximate reduction
sequences in the following weaker way. We denote by $\rightarrow^{=}_{k}$ the
reflexive closure of $\rightarrow_{k}$.

###### Axiom A (Dynamic Approximation).

Let $k\in\mathbb{N}^{\omega}$ and $t,u\in\Lambda$. If $t\rightarrow_{k}u$ then
there is $\mathbf{u}\in{\bf\Lambda}$ such that
$\mathcal{MA}(t)\rightarrow_{k}^{=}\mathbf{u}\geq\mathcal{MA}(u)$.

We also assume that the partial order gives a natural lifting of partial
$k$-reduction sequences into other reduction sequence (on terms or partial
terms) of same length.

###### Axiom B (Dynamic Partial Lifting).

Let $k\in\mathbb{N}^{\omega}$ and
$\mathbf{t},\mathbf{u},\mathbf{t}^{\prime}\in{\bf\Lambda}$. If
$\mathbf{t}\rightarrow_{k}\mathbf{u}$ and $\mathbf{t}\leq\mathbf{t}^{\prime}$,
then $\mathbf{t}^{\prime}\rightarrow_{k}\mathbf{u}^{\prime}\geq\mathbf{u}$ for
some $\mathbf{u}^{\prime}\in{\bf\Lambda}$.

Stratified normal forms are exactly the meaningful and observable outcomes
behind the notion of stratified computation. Let ${\tt no}_{k}$ be the set of
$k$-normal forms. Partial $k$-normal forms without any occurrence of $\bot$ at
depth $k$, noted ${\tt\textbf{bno}}_{k}$, provide perfect approximations of
$k$-normal forms by keeping all their meaningful content. Our next axiom
asserts that the meaningful approximant of an $k$-normal form does not loose
any meaningful information.

###### Axiom C (Observability of Normal Form Approximants).

Let $k\in\mathbb{N}^{\omega}$ and $\mathbf{t}\in{\tt no}_{k}$, then
$\mathcal{MA}(t)\in{\tt\textbf{bno}}_{k}$.

Finally, partial terms in ${\tt\textbf{bno}}_{k}$ are supposed to provide
perfect approximants for $k$-normal forms. The last axiom asserts that they
are stable by increasing information.

###### Axiom D (Stability of Meaningful Observables).

Let $k\in\mathbb{N}^{\omega}$ and $\mathbf{t}\in{\tt\textbf{bno}}_{k}$. If
$\mathbf{u}\in{\bf\Lambda}$ and $\mathbf{t}\leq\mathbf{u}$, then
$\mathbf{u}\in{\tt\textbf{bno}}_{k}$ and
$\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$.

##  4\. Call-by-Value Stratified Genericity

In this section we first introduce the _partial missing_ dCBV-calculus
(Section 4.1), an extension of dCBV enabling the simplification of some
(meaningless) subterms. Then, we prove that the axioms presented in Section 3
hold in the partial dCBV (Sections 4.2, 4.2, 4.2 and 4.4). We use these
properties to strengthen our first dCBV qualitative surface genericity result
into a quantitative stratified one (Theorem 4.5).

###  4.1. The Partial dCBV-Calculus

#### Syntax.

Terms of the partial dCBV-calculus share the same structure as those of dCBV,
with the additional constant $\bot$. Formally, the sets
$\mathbf{\Lambda}\supsetneq\Lambda$ of partial terms and
$\mathbf{\Upsilon}\supsetneq\Upsilon$ of partial values for the partial dCBV-
calculus, denoted by the same symbols for terms but distinguished by a bold
font, are defined inductively as follows:

$\begin{array}[]{r rcl}\textbf{(Partial
terms)}&\mathbf{t},\mathbf{u}&\Coloneqq&\mathbf{v}\;|\;\mathbf{t}\,\mathbf{u}\;|\;\mathbf{t}[x\backslash\mathbf{u}]\;|\;\bot\\\
\textbf{(Partial values)}&\mathbf{v}&\Coloneqq&x\in\mathcal{X}\;|\;\lambda
x.\mathbf{t}\end{array}$

#### Contexts.

As in dCBV, there is a stratified operational semantics, but now defined by
means of partial contexts. The sets of partial list contexts $(\mathbf{L})$
and partial stratified contexts $(\mathbf{V}_{k})$, for
$k\in\mathbb{N}^{\omega}$, are inductively defined as follows (where
$i\in\mathbb{N}$):

$\begin{array}[]{c}\begin{array}[]{rcl}\mathbf{L}&\Coloneqq&\diamond\;|\;\mathbf{L}[x\backslash\mathbf{t}]\\\\[5.69046pt]
\mathbf{V}_{0}&\;\Coloneqq&\diamond\;|\;\mathbf{V}_{0}\,\mathbf{t}\;|\;\mathbf{t}\,\mathbf{V}_{0}\;|\;\mathbf{V}_{0}[x\backslash\mathbf{t}]\;|\;\mathbf{t}[x\backslash\mathbf{V}_{0}]\\\
\mathbf{V}_{i+1}&\Coloneqq&\diamond\;|\;\lambda
x.\mathbf{V}_{i}\;|\;\mathbf{V}_{i+1}\,\mathbf{t}\;|\;\mathbf{t}\,\mathbf{V}_{i+1}\;|\;\mathbf{V}_{i+1}[x\backslash\mathbf{t}]\;|\;\mathbf{t}[x\backslash\mathbf{V}_{i+1}]\\\
\mathbf{V}_{\omega}&\Coloneqq&\diamond\;|\;\lambda
x.\mathbf{V}_{\omega}\;|\;\mathbf{V}_{\omega}\,\mathbf{t}\;|\;\mathbf{t}\,\mathbf{V}_{\omega}\;|\;\mathbf{V}_{\omega}[x\backslash\mathbf{t}]\;|\;\mathbf{t}[x\backslash\mathbf{V}_{\omega}]\end{array}\end{array}$

In particular, we call partial surface (resp. full) context the base (resp.
transfinite) level $\mathbf{V}_{0}$ (resp. $\mathbf{V}_{\omega}$).

#### (Stratified) Operational Semantics.

The following rewriting rules are the base components of our reduction
relations. Any partial term having the shape of the left-hand side of one of
these three rules is called a redex.

$\begin{array}[]{c c c}\mathbf{L}\\!\left<\lambda
x.\mathbf{t}\right>\mathbf{u}\;\mapsto_{{\tt\textbf{dB}}}\;\mathbf{L}\\!\left<\mathbf{t}[x\backslash\mathbf{u}]\right>&&\mathbf{t}[x\backslash\mathbf{L}\\!\left<\mathbf{v}\right>]\;\mapsto_{{\tt\textbf{sV}}}\;\mathbf{L}\\!\left<\mathbf{t}\\{x\backslash\mathbf{v}\\}\right>\end{array}$

Building upon the established pattern used for terms, the stratified partial
reduction (or $\textbf{v}_{k}$-reduction in bold)
$\rightarrow_{\textbf{v}_{k}}$ is the partial $k$-stratified closure
($\mathbf{V}_{k}$-closure) of the two rewriting rules
$\mapsto_{{\tt\textbf{dB}}}$ and $\mapsto_{{\tt\textbf{sV}}}$. In particular,
the reduction $\rightarrow_{\textbf{v}_{0}}$ (resp.
$\rightarrow_{\textbf{v}_{\omega}}$) is called partial surface (resp. full)
reduction. Its reflexive and transitive closure is again denoted by
$\rightarrow^{*}_{\textbf{v}_{k}}$. A partial term $\mathbf{t}$ is a
$\textbf{v}_{k}$-normal form (or $\textbf{v}_{k}$-normal) if there is no
$\mathbf{u}\in\mathbf{\Lambda}$ such that
$\mathbf{t}\rightarrow_{\textbf{v}_{k}}\mathbf{u}$. A partial term is
$\textbf{v}_{k}$-normalizing if
$\mathbf{t}\rightarrow^{*}_{\textbf{v}_{k}}\mathbf{u}$ for some
$\textbf{v}_{k}$-normal form $\mathbf{u}$, and similarly for the partial
surface and full reductions.

###### Example 4.1.

$\mathbf{t}_{0}=\big{(}\lambda y.\bot w\big{)}[w\backslash\lambda
z.\bot]\rightarrow_{\textbf{v}_{k}}\lambda y.\bot\,\big{(}\lambda
z.\bot\big{)}=\mathbf{t}_{1}$ for any $k\in\mathbb{N}^{\omega}$. In
particular, $\mathbf{t}_{1}$ is partial surface normal.

###  4.2. Quantitative Stratified Genericity

#### Meaningful Approximation.

As explained before, our approach is based on abstracting meaningless subterms
by means of partial terms. This is implemented through the tool of _meaningful
approximation_ , which associates with each term a partial term obtained by
replacing all its meaningless subterms with $\bot$. Formally, the dCBV-
meaningful approximant $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)$ of a term
$t\in\Lambda$ is defined as $\bot$ if $t$ is dCBV-meaningless, and inductively
on $t$ as follows otherwise:

$\displaystyle\mathcal{M\\!A}_{{\tt V}}\\!\left(x\right)$
$\displaystyle\coloneqq x$ $\displaystyle\mathcal{M\\!A}_{{\tt
V}}\\!\left(t[x\backslash u]\right)$
$\displaystyle\coloneqq\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)]$
$\displaystyle\mathcal{M\\!A}_{{\tt V}}\\!\left(\lambda x.t\right)$
$\displaystyle\coloneqq\lambda x.\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)$
$\displaystyle\mathcal{M\\!A}_{{\tt V}}\\!\left(tu\right)$
$\displaystyle\coloneqq\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$

###### Example 4.2.

$\mathcal{M\\!A}_{{\tt V}}\\!\left((\lambda x.x\Omega)(\lambda
y.\Omega)\right)=(\lambda x.\bot)(\lambda y.\bot)$.

Another partial calculus already exists in a CbV setting (Kerinec et al.,
2020, 2021; ManzonettoPR2019), which only approximates values. Their approach
seems incompatible with our definition of meaningful approximant: it cannot be
used to approximate meaningless terms such as $\Omega$.

We equip the set of partial terms ${\bf\Lambda}$ with a partial order $\leq$
defined as the partial full context closure of $\bot\leq\mathbf{t}$ for any
partial term $\mathbf{t}\in{\bf\Lambda}$. This definition does not only allow
us to approximate values, as done in (Kerinec et al., 2020), but any kind of
term. As expected, the meaningful approximation of a term approximates
it.lemmaCbvMeaningfulApproximationLeqTerm Let $t\in\Lambda$, then
$\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\leq t$.

Using qualitative surface genericity (Section 2), we obtain a genericity
result for meaningful approximants which states that replacing a meaningless
subterm by any other kind of term can only refine its meaningful approximant.

[dCBV Approximant Genericity]lemmaCbvApproximantGenericity Let $\mathtt{C}$ be
a full context. If $t\in\Lambda$ is dCBV-meaningless, then
$\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<u\right>\right)$ for all $u\in\Lambda$.

###### Example 4.3.

One has $\mathcal{M\\!A}_{{\tt V}}\\!\left((\lambda x.x\Omega)(\lambda
y.\Omega)\right)=(\lambda x.\bot)(\lambda y.\bot)\leq(\lambda
x.x\mathtt{I})(\lambda y.\bot)=\mathcal{M\\!A}_{{\tt V}}\\!\left((\lambda
x.x\mathtt{I})(\lambda y.\Omega)\right)$ since $\mathtt{I}$ is dCBV-
meaningful.

The previous property constitutes the core of our quantitative stratified
genericity result. It will be used in particular to construct a common partial
term approximating two distinct terms $\mathtt{C}\\!\left<t\right>$ and
$\mathtt{C}\\!\left<u\right>$, where $t$ is necessarily a meaningless subterm.
This common partial term will then be used to transform a reduction sequence
from $\mathtt{C}\\!\left<t\right>$ into a reduction sequence from
$\mathtt{C}\\!\left<u\right>$.

#### Dynamic Approximation and Lifting.

We now seek to transfer reduction sequences between two terms by using a
common partial term approximating both of them. First, we show that term
reduction steps are simulated by the corresponding meaningful approximants.
This corresponds to Axiom A for dCBV.

[dCBV Dynamic Approximation]lemmaCbvDynamicApproximation Let
$k\in\mathbb{N}^{\omega}$ and $t,u\\!\in\\!\Lambda$. If
$t\rightarrow_{\mathrm{v}_{k}}\\!u$ then $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\rightarrow^{=}_{\textbf{v}_{k}}\\!\mathbf{u}\geq\mathcal{M\\!A}_{{\tt
V}}\\!\left(u\right)$ for some $\mathbf{u}\\!\in\\!\mathbf{\Lambda}$.

Thus, the meaningful approximant $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)$
replicates the _essence_ of the reduction sequence from $t$. Still, there are
two important differences. First, some steps may be equated by their
meaningful approximants, e.g.
$t_{0}\coloneqq\Omega\rightarrow_{\mathrm{v}_{0}}(xx)[x\backslash\Delta]\eqqcolon
t_{1}$ while $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{0}\right)=\bot=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)$.
Secondly, some reduction steps do not yield the meaningful approximation but
an over-approximation of it, e.g. consider $t_{2}\coloneqq(x(\lambda
y.z\Delta))[z\backslash\Delta]\rightarrow_{\mathrm{v}_{0}}x(\lambda
y.\Omega)\eqqcolon t_{3}$, then $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{1}\right)=(x(\lambda
y.z\Delta))[z\backslash\Delta]\rightarrow_{\textbf{v}_{0}}x(\lambda y.\Omega)$
while $x(\lambda y.\Omega)\geq x\bot=\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{3}\right)$.

Partial reduction sequences can also be lifted to greater partial terms, and
in particular to terms. This is Axiom B for dCBV.

[dCBV Dynamic Partial Lift]lemmaCbvDynamicLift Let $k\in\mathbb{N}^{\omega}$
and $\mathbf{t},\mathbf{u},\mathbf{t}^{\prime}\\!\in\\!\mathbf{\Lambda}$. If
$\mathbf{t}\rightarrow_{\textbf{v}_{k}}\\!\mathbf{u}$ and
$\mathbf{t}\leq\mathbf{t}^{\prime}$, then
$\mathbf{t}^{\prime}\\!\rightarrow_{\textbf{v}_{k}}\\!\mathbf{u}^{\prime}\\!\geq\mathbf{u}$
for some $\mathbf{u}^{\prime}\\!\in\\!\mathbf{\Lambda}$.

Recalling Example 4.1, let $\mathbf{t}^{\prime}_{0}\coloneqq\big{(}\lambda
y.\mathtt{I}w\big{)}[w\backslash\lambda z.\lambda x.\bot]$, so that
$\mathbf{t}_{0}\leq\mathbf{t}^{\prime}_{0}$. Then
$\mathbf{t}^{\prime}_{0}\rightarrow_{\textbf{v}_{k}}\lambda
y.\mathtt{I}\,\big{(}\lambda z.\lambda x.\bot\big{)}=:\mathbf{t}^{\prime}_{1}$
for all $k\in\mathbb{N}^{\omega}$, and
$\mathbf{t}_{1}\leq\mathbf{t}^{\prime}_{1}$.

#### Observability.

Stratified normal forms are precisely the meaningful and observable outcomes
behind the notion of stratified computation. For $k\in\mathbb{N}^{\omega}$,
the set ${\tt bno}_{\textbf{v}_{k}}$ of partial terms introduced below aims to
provide perfect approximation of them, being $\textbf{v}_{k}$-normal forms
without any occurrence of $\bot$ at depth $k$.

$\displaystyle{\tt bvr}_{\textbf{v}_{k}}$ $\displaystyle\coloneqq\,x\;|\;{\tt
bvr}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]$
$\displaystyle{\tt bne}_{\textbf{v}_{k}}$ $\displaystyle\coloneqq\,{\tt
bvr}_{\textbf{v}_{k}}\,{\tt bno}_{\textbf{v}_{k}}\;|\;{\tt
bne}_{\textbf{v}_{k}}\,{\tt bno}_{\textbf{v}_{k}}\;|\;{\tt
bne}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]$
$\displaystyle{\tt bno}_{\textbf{v}_{0}}$ $\displaystyle\coloneqq\,\lambda
x.\mathbf{t}\;|\;{\tt bvr}_{\textbf{v}_{0}}\;|\;{\tt
bne}_{\textbf{v}_{0}}\;|\;{\tt bno}_{\textbf{v}_{0}}[x\backslash{\tt
bne}_{\textbf{v}_{0}}]$ $\displaystyle{\tt bno}_{\textbf{v}_{i+1}}$
$\displaystyle\coloneqq\,\lambda x.{\tt bno}_{\textbf{v}_{i}}\;|\;{\tt
bvr}_{\textbf{v}_{i+1}}\;|\;{\tt bne}_{\textbf{v}_{i+1}}\;|\;{\tt
bno}_{\textbf{v}_{i+1}}[x\backslash{\tt bne}_{\textbf{v}_{i+1}}]\ \
(i\in\mathbb{N})$ $\displaystyle{\tt bno}_{\textbf{v}_{\omega}}$
$\displaystyle\coloneqq\,\lambda x.{\tt bno}_{\textbf{v}_{\omega}}\;|\;{\tt
bvr}_{\textbf{v}_{\omega}}\;|\;{\tt bne}_{\textbf{v}_{\omega}}\;|\;{\tt
bno}_{\textbf{v}_{\omega}}[x\backslash{\tt bne}_{\textbf{v}_{\omega}}]$

Remarkably, our meaningful approximants are precise enough to perfectly
observe the important level of these meaningful results. We thus obtain the
dCBV instance of Axiom C.

[dCBV Observability of Normal Form
Approximants]lemmaCbvObservabilityNormalFormApproximant Let
$k\in\mathbb{N}^{\omega}$ and $\mathbf{t}\in{\tt no}_{\mathrm{v}_{k}}$, then
$\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\in{\tt bno}_{\textbf{v}_{k}}$.

###### Example 4.4.

$t_{0}\coloneqq\lambda x.(x(\lambda y.\mathtt{I}\mathtt{I})(\lambda
z.\mathtt{I}\Omega))$ is $\mathrm{v}_{1}$-normal and its meaningful
approximant is $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{0}\right)=\lambda
x.(x(\lambda y.\mathtt{I}\mathtt{I})(\lambda z.\bot))\in{\tt
bno}_{\textbf{v}_{1}}$.

Finally, we show that partial terms in ${\tt bno}_{\textbf{v}_{k}}$ entirely
determinate the first $k$ levels of the $k$-normal forms they approximate.
Consequently, any greater approximant aligns with its first $k$ levels. This
is the dCBV precisely the instance of Axiom D.

[dCBV Stability of Meaningful
Observables]lemmaCbvStabilityMeaningfulObservables Let
$k\in\mathbb{N}^{\omega}$. If $\mathbf{t}\in{\tt bno}_{\textbf{v}_{k}}$ and
$\mathbf{t}\leq\mathbf{u}\in\mathbf{\Lambda}$, then $\mathbf{u}\in{\tt
bno}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle
k}{\approx}\mathbf{u}$.

Note that $\mathbf{u}$ can be a term. Taking $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{0}\right)$ from Example 4.4, where $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{0}\right)\leq t_{0}$ as expected, one verifies that both
partial terms $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{0}\right)$ and $t_{0}$
share the same structure on the first $2$-levels. And similarly for any other
partial term greater than $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{0}\right)$.

#### Quantitative Stratified Genericity.

We now have all the material to enhance our first _qualitative_ surface
genericity (Section 2) into a stronger _quantitative_ stratified genericity
result.

###### Theorem 4.5 (dCBV Quantitative Stratified Genericity).

Let $k\in\mathbb{N}^{\omega}$. If $t\in\Lambda$ is dCBV-meaningless and
$\mathtt{C}\\!\left<t\right>$ is $\mathrm{v}_{k}$-normalizing, then there is
$i\in\mathbb{N}$ such that, for every $u\in\Lambda$, there are
$t^{\prime},u^{\prime}\in{\tt no}_{\mathrm{v}_{k}}$ such that
$\mathtt{C}\\!\left<t\right>\rightarrow^{i}_{\mathrm{v}_{k}}t^{\prime}\;\overset{\scriptscriptstyle
k}{\approx}\;u^{\prime}\;\sideset{{}^{i}_{\mathrm{v}_{k}\\!\\!\\!\\!}}{}{\operatorname{\leftarrow}}\;\mathtt{C}\\!\left<u\right>$.

###### Proof.

By definition, there is $s\in{\tt no}_{\mathrm{v}_{k}}$ such that
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{v}_{k}}s$. By iterating
Sections 4.2 and 4.2, there are $\mathbf{s}\in\mathbf{\Lambda}$ and
$i\in\mathbb{N}$ such that $\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\rightarrow^{i}_{\textbf{v}_{k}}\mathbf{s}\geq\mathcal{M\\!A}_{{\tt
V}}\\!\left(s\right)$. Since $s\in{\tt no}_{\mathrm{v}_{k}}$, then
$\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\in{\tt bno}_{\textbf{v}_{k}}$
using Section 4.2, thus $\mathbf{s}\in{\tt bno}_{\textbf{v}_{k}}$ using
Example 4.4. On one hand, $\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathtt{C}\\!\left<t\right>$
by Example 4.2, thus by iterating Section 4.2, one has
$\mathtt{C}\\!\left<t\right>\rightarrow^{i}_{\mathrm{v}_{k}}t^{\prime}$ for
some $t^{\prime}\in\Lambda$ such that $\mathbf{s}\leq t^{\prime}$. By Example
4.4, $t^{\prime}\in{\tt no}_{\mathrm{v}_{k}}$ and
$t^{\prime}\overset{\scriptscriptstyle k}{\approx}\mathbf{s}$. On the other
hand, $\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<u\right>\right)$ according to Example 4.2, thus
$\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathtt{C}\\!\left<u\right>$
by Example 4.2 and transitivity. By iterating Section 4.2 again, one has that
$\mathtt{C}\\!\left<u\right>\rightarrow^{i}_{\mathrm{v}_{k}}u^{\prime}$ for
some $u^{\prime}\in\Lambda$ such that $\mathbf{s}\leq u^{\prime}$. By Example
4.4, $u^{\prime}\in{\tt no}_{\mathrm{v}_{k}}$ and
$u^{\prime}\overset{\scriptscriptstyle k}{\approx}\mathbf{s}$. Finally,
$t^{\prime}\overset{\scriptscriptstyle k}{\approx}u^{\prime}$ by transitivity
of $\overset{\scriptscriptstyle k}{\approx}$. ∎

Graphically, these are the main steps in the proof of Theorem 4.5:

$\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)$$\mathbf{s}\\!$$\mathtt{C}\\!\left<t\right>$$t^{\prime}\\!$$\ni$${\tt
no}_{\mathrm{v}_{k}}$$\mathtt{C}\\!\left<u\right>$$u^{\prime}\\!$$\in$${\tt
no}_{\mathrm{v}_{k}}$$\scriptscriptstyle
n$$\scriptscriptstyle\textbf{v}_{k}$$\scriptscriptstyle
n$$\scriptscriptstyle\mathrm{v}_{k}$$\scriptscriptstyle
n$$\scriptscriptstyle\mathrm{v}_{k}$$\leftsquigarrow$$\scriptscriptstyle{\tt
Lem}.\ref{lem:cbvAGK_Aprx_Simulation_MultiStep}$$\rightsquigarrow$$\scriptscriptstyle{\tt
Lem}.\ref{lem:cbvAGK_Aprx_Simulation_MultiStep}$$\geq$$\scriptscriptstyle{\tt
Lem.}\ref{lem:Cbv_MA(t)_<=_t}$$\geq$$\leq$$\scriptscriptstyle{\tt
Lem.}\ref{lem:Cbv_t_meaningless_=>_MA(F<t>)_<=_MA(F<u>)}\;\&\;{\tt
Lem.}\ref{lem:Cbv_MA(t)_<=_t}$$\leq$$\overset{\scriptscriptstyle
k}{\scalebox{4.0}[1.0]{$\approx$}}$$\scriptscriptstyle{\tt
Lem.}\ref{lem:Cbv_|t_in_bnoSn_and_t_<=_u_==>_u_in_BnoSn}$

A particular case is given by the following statement since $k$-equality for
$k=\omega$ is just the equality between terms.

###### Corollary 4.6 (dCBV Quantitative Full Genericity).

If $t\in\Lambda$ is dCBV-meaningless and
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{v}_{\omega}}s$ where $s$
is $\mathrm{v}_{\omega}$-normal, then there is $i\in\mathbb{N}$ such that, for
every $u\in\Lambda$,
$\mathtt{C}\\!\left<t\right>\rightarrow^{i}_{\mathrm{v}_{\omega}}s\;\sideset{{}^{i}_{\mathrm{v}_{\omega}\\!\\!\\!\\!}}{}{\operatorname{\leftarrow}}\;\mathtt{C}\\!\left<u\right>$.

For instance, $(\lambda y.\mathtt{I})\lambda
z.\Omega\rightarrow^{2}_{\mathrm{v}_{\omega}}\mathtt{I}\;\sideset{{}^{2}_{\mathrm{v}_{\omega}\\!\\!\\!\\!}}{}{\operatorname{\leftarrow}}\;(\lambda
y.\mathtt{I})\lambda z.u$ for any $u\in\Lambda$.

Theorem 4.5, Corollary 4.6 and the general methodology used to prove such
results are among the main contributions of this paper.

##  5\. Call-by-Name Stratified Genericity

Section 5.1 introduces the syntax and operational semantics of the dCBN-
calculus (Accattoli and Kesner, 2010, 2012), including the new notion of
_stratified reduction_. We also recall the $\mathcal{N}$ type system (Kesner
and Ventura, 2014). The qualitative and quantitative stratified genericity
results follow in Section 5.2.

###  5.1. Syntax and Stratified Operational Semantics

#### Syntax.

The term syntax of the dCBN-calculus is exactly the same as in dCBV. We keep
the same notations for terms ($s,t,u,\dots$) and the set of terms ($\Lambda$).
In the operational semantics of dCBN (see below), values do not play any role,
so we do not distinguish them. Free variables, $\alpha$-conversion and
substitution are defined as in dCBV.

#### Contexts.

The operational semantics of the dCBN-calculus is often specified by means of
a _head_ reduction that forbids evaluation inside arguments, called here
_surface_ reduction. Here again, we equip the dCBN-calculus with a new
_stratified_ operational semantics which generalizes surface reduction to
different _levels_.

The set of list contexts $(\mathtt{L})$ and stratified contexts
$(\mathtt{N}_{k})$ for $k\in\mathbb{N}^{\omega}$, that can be seen as terms
containing exactly one hole $\diamond$, are inductively defined as follows
(where $i\in\mathbb{N}$):

$\begin{array}[]{rcl}\mathtt{L}&\;\Coloneqq&\diamond\;|\;\mathtt{L}[x\backslash
t]\\\\[5.69046pt] \mathtt{N}_{0}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathtt{N}_{0}\;|\;\mathtt{N}_{0}\,t\;|\;\mathtt{N}_{0}[x\backslash t]\\\
\mathtt{N}_{i+1}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathtt{N}_{i+1}\;|\;\mathtt{N}_{i+1}\,t\;|\;t\,\mathtt{N}_{i}\;|\;\mathtt{N}_{i+1}[x\backslash
t]\;|\;t[x\backslash\mathtt{N}_{i}]\\\
\mathtt{N}_{\omega},\mathtt{C}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathtt{N}_{\omega}\;|\;\mathtt{N}_{\omega}\,t\;|\;t\,\mathtt{N}_{\omega}\;|\;\mathtt{N}_{\omega}[x\backslash
t]\;|\;t[x\backslash\mathtt{N}_{\omega}]\end{array}$

In particular, surface contexts (whose hole is not in an argument) and full
contexts (the restriction-free one-hole contexts, also denoted by
$\mathtt{C}$) are special cases of stratified context: surface contexts are
base level $\mathtt{N}_{0}$ and full contexts the transfinite level
$\mathtt{N}_{\omega}$. In stratified contexts $\mathtt{N}_{k}$, the hole can
occur everywhere as long as its depth is at most $k$, while in
$\mathtt{N}_{\omega}$ it can occur everywhere and in $\mathtt{N}_{0}$ it
cannot occur in a top level argument. Thus for example $y\,(\lambda
x.\diamond)$ is in $\mathtt{N}_{1}$, and thus in every $\mathtt{N}_{k}$ with
$k\geq 1$, including $\mathtt{N}_{\omega}$, but it is not in $\mathtt{N}_{0}$.
For all $k\in\mathbb{N}^{\omega}$, we write $\mathtt{N}_{k}\\!\left<t\right>$
for the term obtained by replacing the hole in $\mathtt{N}_{k}$ with the term
$t$, and similarly for $\mathtt{L}$.

We define the stratified equality comparing terms up to a given depth. It is
defined by the following inductive rules (with $i\in\mathbb{N})$:

$({\tt var})$ $x\overset{\scriptscriptstyle i}{\approx}x$

$({\tt abs})$ $t\overset{\scriptscriptstyle i}{\approx}u$$\lambda
x.t\overset{\scriptscriptstyle i}{\approx}\lambda x.u$

$({\tt app})$ $t_{1}\overset{\scriptscriptstyle
0}{\approx}u_{1}$$t_{1}t_{2}\overset{\scriptscriptstyle 0}{\approx}u_{1}u_{2}$

$({\tt app})$ $t_{1}\overset{\scriptscriptstyle
i+1}{\approx}u_{1}$$t_{2}\overset{\scriptscriptstyle
i}{\approx}u_{2}$$t_{1}t_{2}\overset{\scriptscriptstyle
i+1}{\approx}u_{1}u_{2}$

$({\tt app})$
$t_{1}\overset{\scriptscriptstyle\omega}{\approx}u_{1}$$t_{2}\overset{\scriptscriptstyle\omega}{\approx}u_{2}$$t_{1}t_{2}\overset{\scriptscriptstyle\omega}{\approx}u_{1}u_{2}$

$({\tt es})$ $t\overset{\scriptscriptstyle 0}{\approx}u$$t[x\backslash
t^{\prime}]\overset{\scriptscriptstyle 0}{\approx}u[x\backslash u^{\prime}]$
$({\tt es})$ $t\overset{\scriptscriptstyle
i+1}{\approx}u$$t^{\prime}\overset{\scriptscriptstyle
i}{\approx}u^{\prime}$$t[x\backslash t^{\prime}]\overset{\scriptscriptstyle
i+1}{\approx}u[x\backslash u^{\prime}]$ $({\tt es})$
$t\overset{\scriptscriptstyle\omega}{\approx}u$$t^{\prime}\overset{\scriptscriptstyle\omega}{\approx}u^{\prime}$$t[x\backslash
t^{\prime}]\overset{\scriptscriptstyle\omega}{\approx}u[x\backslash
u^{\prime}]$

###### Example 5.1.

Let $t_{0}:=x\mathtt{I}[x\backslash y\Omega]$ and
$t_{1}:=x\mathtt{I}[x\backslash y\mathtt{I}]$. We have
$t_{0}\overset{\scriptscriptstyle 0}{\approx}t_{1}$ and
$t_{0}\overset{\scriptscriptstyle 1}{\approx}t_{1}$ but not
$t_{0}\overset{\scriptscriptstyle k}{\approx}t_{1}$ for any $k\geq 2$.

While the same intuition behind stratification is shared between dCBV and
dCBN, their respective implementations turn out to be quite different,
depending on the underlying notion of reduction.

#### (Stratified) Operational Semantics.

The notions of contexts already established, we can now equip the dCBN with an
operational semantics acting _at a distance_ (Accattoli and Kesner, 2010,
2012). The following rewriting rules are the base components of such
operational semantics.

$\begin{array}[]{c c c}\mathtt{L}\\!\left<\lambda x.s\right>t\;\mapsto_{{\tt
dB}}\;\mathtt{L}\\!\left<s[x\backslash t]\right>&&t[x\backslash
u]\;\mapsto_{{\tt s}}\;t\\{x\backslash u\\}\end{array}$

Rule ${\tt dB}$ assumed to be _capture free_ , so no free variable of $t$ is
captured by the context $\mathtt{L}$. The main difference between dCBN and
dCBV is that rule ${\tt sV}$ of the latter is replaced by rule ${\tt s}$ in
the former.

The stratified reduction (or $\mathrm{n}_{k}$-reduction)
$\rightarrow_{\mathrm{n}_{k}}$ is the $\mathtt{N}_{k}$-closure of the two
rewriting rules $\mapsto_{{\tt dB}}$ and $\mapsto_{{\tt s}}$. In particular,
$\rightarrow_{\mathrm{n}_{0}}$ (resp. $\rightarrow_{\mathrm{n}_{\omega}}$) is
called surface (resp. full) reduction. We write
$\rightarrow^{*}_{\mathrm{n}_{k}}$ for the reflexive and transitive closure of
reduction $\rightarrow_{\mathrm{n}_{k}}$.

###### Lemma 5.2 ((Accattoli and Kesner, 2012)).

The dCBN surface and full reductions are confluent.

As in dCBV, For $k\notin\\{0,\omega\\}$, $\mathrm{n}_{k}$-reduction is not
confluent. In general,
$\rightarrow_{\mathrm{n}_{i}}\,\subsetneq\,\rightarrow_{\mathrm{n}_{i+1}}\,\subsetneq\,\rightarrow_{\mathrm{n}_{\omega}}$
for all $i\in\mathbb{N}$.

#### Normal Forms.

Similar to ${\tt dCBV}$, each level of the stratified reduction
$\rightarrow_{\mathrm{n}_{k}}$ yields a corresponding notion of
$\mathrm{n}_{k}$-normal form and $\mathrm{n}_{k}$-normalizability. Normal
forms can be _syntactically_ characterized by the following grammar ${\tt
no}_{\mathrm{n}_{\omega}}$, where the subgrammar ${\tt
ne}_{\mathrm{n}_{\omega}}$ generates special normal forms called _neutral_ ,
which never create a redex when applied to an argument.

$\begin{array}[]{c}\begin{array}[]{rcl}{\tt
ne}_{\mathrm{n}_{0}}&\coloneqq&x\;|\;{\tt ne}_{\mathrm{n}_{0}}t\\\ {\tt
ne}_{\mathrm{n}_{i+1}}&\coloneqq&x\;|\;{\tt ne}_{\mathrm{n}_{i+1}}{\tt
no}_{\mathrm{n}_{i}}\qquad(i\in\mathbb{N})\\\ {\tt
ne}_{\mathrm{n}_{\omega}}&\coloneqq&x\;|\;{\tt ne}_{\mathrm{n}_{\omega}}{\tt
no}_{\mathrm{n}_{\omega}}\\\\[5.69046pt] {\tt
no}_{\mathrm{n}_{k}}&\coloneqq&\lambda x.{\tt no}_{\mathrm{n}_{k}}\;|\;{\tt
ne}_{\mathrm{n}_{k}}\qquad(k\in\mathbb{N}^{\omega})\end{array}\end{array}$

lemmaCbnNoSnCharacterization Let $k\in\mathbb{N}^{\omega}$. Then $t\in\Lambda$
is $\mathrm{n}_{k}$-normal iff $t\in{\tt no}_{\mathrm{n}_{k}}$.

#### Quantitative Typing.

We now present the quantitative typing system $\mathcal{N}$ based on
intersection types which was introduced in (Kesner and Ventura, 2014). The
typing rule of system $\mathcal{N}$ are defined as follows:

$\begin{array}[]{ccc}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
29.76262pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\scriptsize$({\tt
var})$}}}\hbox{\hbox{\hbox{}\hbox{}}\hbox{$x:\left[\sigma\right]\vdash
x:\sigma\hfil\lx@intercol$}}\par}\par}}}$}\hskip
28.45274pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
2.06671pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\scriptsize$({\tt
abs})$}}}\hbox{\hbox{\hbox{}\hbox{$\Pi\triangleright_{\mathcal{N}}\Gamma;x:\mathcal{M}\vdash
t:\sigma$}}\hbox{$\Gamma\vdash\lambda
x.t:\mathcal{M}\Rightarrow\sigma\quad$}}\par}\par}}}$}\\\\[14.22636pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\scriptsize$({\tt app})$}}}\hbox{\hskip
5.29054pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{}\hbox{\lower 2.5pt\hbox{\hbox{$\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$}$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1}\vdash
t:\left[\tau_{i}\right]_{i\in
I}\Rightarrow\sigma\hfil\lx@intercol$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash
u:\tau_{i}$}}}$}\right)_{i\in I}$}}}}}\hbox{\hbox{$\Gamma_{1}+_{i\in
I}\Gamma_{2}^{i}\mathrel{}$}$\mathrel{}\vdash tu:\sigma\hskip
79.6678pt$}}}\par}\par}}}$}\\\\[14.22636pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\scriptsize$({\tt es})$}}}\hbox{\hskip
5.29054pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{}\hbox{\lower 2.5pt\hbox{\hbox{$\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$}$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1},x:\left[\tau_{i}\right]_{i\in
I}\vdash
t:\sigma\hfil\lx@intercol$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash
u:\tau_{i}$}}}$}\right)_{i\in I}$}}}}}\hbox{\hbox{$\Gamma_{1}+_{i\in
I}\Gamma_{2}^{i}\mathrel{}$}$\mathrel{}\vdash t[x\backslash u]:\sigma\hskip
71.13188pt$}}}\par}\par}}}$}\end{array}$

with $I$ finite in rules $({\tt app})$ and $({\tt es})$. As with system
$\mathcal{V}$, a (type) derivation is a tree obtained by applying the
(inductive) typing rules of system $\mathcal{N}$. Similarly, the notation
$\Pi\triangleright_{\mathcal{N}}\Gamma\vdash t:\sigma$ means there is a
derivation of the judgment $\Gamma\vdash t:\sigma$ in system $\mathcal{N}$ and
we say that $t$ is $\mathcal{N}$-typable if
$\Pi\triangleright_{\mathcal{N}}\Gamma\vdash t:\sigma$ holds for some
$\Gamma,\sigma$.

System $\mathcal{N}$ _characterizes_ surface normalization (see Lemma 5.4).

#### Meaningfulness.

We start by defining dCBN-meaningfulness.

###### Definition 5.3.

A term $t\in\Lambda$ is dCBN meaningful if there is a testing context
$\mathtt{T}$ such that
$\mathtt{T}\\!\left<t\right>\rightarrow^{*}_{\mathrm{n}_{0}}\mathtt{I}$ (with
$\mathtt{T}\Coloneqq\diamond\;|\;\mathtt{T}\,u\;|\;(\lambda
x.\mathtt{T})\,u$).111Usually, dCBN-meaningfulness (aka _solvability_) is
defined using contexts of the form $(\lambda x_{1}\dots
x_{m}.\diamond)N_{1}\dots N_{n}$ ($m,n\geq 0$) (Barendregt, 1977, 1984; Rocca
and Paolini, 2004), instead of testing contexts. It is easy to check that the
two definitions are equivalent in dCBN. The benefit of our definition is that
the same testing contexts are also used to define dCBV-meaningfulness (Section
2).

As for the dCBV-case, dCBN-meaningfulness can be characterized _operationally_
, through the notion of surface-normalization, and _logically_ , through
typability in type system $\mathcal{N}$.

###### Lemma 5.4 (dCBN Meaningful Characterizations (Bucciarelli et al., 2021,
2020)).

Let $t\in\Lambda$. Then, the following characterizations hold:

  * (Operational)

$t$ is dCBN-meaningful iff $t$ is dCBN surface-normalizing.

  * (Logical)

$t$ is dCBN-meaningful iff $t$ is $\mathcal{N}$-typable.

#### Surface Genericity.

As in ${\tt dCBV}$, since the typing system characterizes meaningfulness, we
can prove a typed genericity result.

[dCBN Typed Genericity]lemmaCbnTypedSurfaceGenericity Let $t\in\Lambda$ be
dCBN-meaningless. If
$\Pi\triangleright_{\mathcal{N}}\Gamma\vdash\mathtt{C}\\!\left<t\right>:\sigma$,
then there is
$\Pi^{\prime}\triangleright_{\mathcal{N}}\Gamma\vdash\mathtt{C}\\!\left<u\right>:\sigma$
for all $u\in\Lambda$.

Likewise, it can be transformed into a qualitative surface genericity using
the logical characterization (Lemma 5.4).

[dCBN Qualitative Surface Genericity]theoremCbnQualitativeSurfaceGenericity
Let $t\in\Lambda$ be dCBN-meaningless. If $\mathtt{C}\\!\left<t\right>$ is
dCBN-meaningful then $\mathtt{C}\\!\left<u\right>$ is also dCBN-meaningful for
all $u\in\Lambda$.

###  5.2. Call-by-Name Genericity

####  Partial dCBN-Calculus

The set $\mathbf{\Lambda}$ of partial terms of the partial dCBN-calculus,
denoted by the same symbols used for terms but in a bold font, is given by the
following inductive definition:

$\begin{array}[]{r rcl}\textbf{(Partial
terms)}&\mathbf{t},\mathbf{u}&\Coloneqq&x\in\mathcal{X}\;|\;\lambda
x.\mathbf{t}\;|\;\mathbf{t}\mathbf{u}\;|\;\mathbf{t}[x\backslash\mathbf{u}]\;|\;\bot\end{array}$

As in the dCBN-calculus, there is a stratified operational, but now defined by
means of partial contexts. The set of partial list contexts $(\mathbf{L})$ and
partial stratified contexts $(\mathbf{N}_{k})$ for some
$k\in\mathbb{N}^{\omega}$ are inductively defined as follows (where
$i\in\mathbb{N}$):

$\begin{array}[]{rcl}\mathbf{L}&\;\Coloneqq&\diamond\;|\;\mathbf{L}[x\backslash
t]\\\\[5.69046pt] \mathbf{N}_{0}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathbf{N}_{0}\;|\;\mathbf{N}_{0}\,t\;|\;\mathbf{N}_{0}[x\backslash t]\\\
\mathbf{N}_{i+1}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathbf{N}_{i+1}\;|\;\mathbf{N}_{i+1}\,t\;|\;t\,\mathbf{N}_{i}\;|\;\mathbf{N}_{i+1}[x\backslash
t]\;|\;t[x\backslash\mathbf{N}_{i}]\\\
\mathbf{N}_{\omega}&\;\Coloneqq&\diamond\;|\;\lambda
x.\mathbf{N}_{\omega}\;|\;\mathbf{N}_{\omega}\,t\;|\;t\,\mathbf{N}_{\omega}\;|\;\mathbf{N}_{\omega}[x\backslash
t]\;|\;t[x\backslash\mathbf{N}_{\omega}]\end{array}$

The following rewriting rules are the base components of our reduction
relations. Any partial term having the shape of the left-hand side of one of
these three rules is called a redex.

$\begin{array}[]{c c c}\mathbf{L}\\!\left<\lambda
x.\mathbf{t}\right>\mathbf{u}\;\mapsto_{{\tt\textbf{dB}}}\;\mathbf{L}\\!\left<\mathbf{t}[x\backslash\mathbf{u}]\right>&&\mathbf{t}[x\backslash\mathbf{u}]\;\mapsto_{{\tt\textbf{s}}}\;\mathbf{t}\\{x\backslash\mathbf{u}\\}\end{array}$

Building upon the established pattern used for terms, the stratified partial
reduction (or $\mathrm{n}_{k}$-reduction) $\rightarrow_{\mathbf{n}_{k}}$ is
defined as the partial $k$-stratified closure ($\mathbf{N}_{k}$-closure) of
the two rewriting rules $\mapsto_{{\tt\textbf{dB}}}$ and
$\mapsto_{{\tt\textbf{s}}}$. Its reflexive-transitive closure is denoted by
$\rightarrow^{*}_{\mathbf{n}_{k}}$.

###### Example 5.5.

$\mathbf{t}_{0}=\big{(}\lambda y.\bot w\big{)}[w\backslash\lambda
z.\bot]\rightarrow_{\mathbf{n}_{k}}\lambda y.\big{(}\bot\,\lambda
z.\bot\big{)}$ $=\mathbf{t}_{1}$ for any $k\in\mathbb{N}^{\omega}$. In
particular, $\mathbf{t}_{1}$ is $\mathbf{n}_{0}$-normal form.

#### Meaningful Approximation.

The definition is the same as in dCBV, just adapting the notion of
meaningfulness to dCBN. Indeed, the dCBN-meaningful approximant
$\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)$ of $t\in\Lambda$ is $\bot$ if $t$
is dCBN-meaningless, and is defined inductively on $t$ otherwise:

$\displaystyle\mathcal{M\\!A}_{{\tt N}}\\!\left(x\right)$
$\displaystyle\coloneqq x$ $\displaystyle\mathcal{M\\!A}_{{\tt
N}}\\!\left(tu\right)$ $\displaystyle\coloneqq\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)$
$\displaystyle\mathcal{M\\!A}_{{\tt N}}\\!\left(\lambda x.t\right)$
$\displaystyle\coloneqq\lambda x.\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)$
$\displaystyle\mathcal{M\\!A}_{{\tt N}}\\!\left(t[x\backslash u]\right)$
$\displaystyle\coloneqq\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)]$

The meaningful approximation of a term $t$ approximates
$t$:lemmaCbnMeaningfulApproximationLeqTerm Let $t\in\Lambda$, then
$\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\leq t$.

[dCBN Approximant Genericity]lemmaCbnApproximantGenericity Let $\mathtt{C}$ be
a full context. If $t\in\Lambda$ is dCBN-meaningless, then
$\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<u\right>\right)$ for all $u\in\Lambda$.

#### Dynamic Approximation and Lifting.

To replicate the proof of quantitative stratified genericity on the dCBN-
calculus, we now need to be able to approximate term reductions and lift
partial reductions. Fortunately, both instances of Axioms B and A for dCBN
hold. Consequently, the partial dCBN-calculus can effectively be used to
approximate reductions of the dCBN-calculus.

#### Observability.

We now check that the partial dCBN-calculus correctly captures the meaningful
and observable outcomes.

For $k\in\mathbb{N}^{\omega}$, the set ${\tt bno}_{\mathbf{n}_{k}}$ of partial
terms introduced below aims to provide perfect approximation of them, being
$\mathbf{n}_{k}$-normal forms without any occurrence of $\bot$ at depth $k$.

$\begin{array}[]{rcl}{\tt bne}_{\mathbf{n}_{0}}&\coloneqq&x\;|\;{\tt
bne}_{\mathbf{n}_{0}}\mathbf{t}\\\ {\tt
bne}_{\mathbf{n}_{i+1}}&\coloneqq&x\;|\;{\tt bne}_{\mathbf{n}_{i+1}}{\tt
bno}_{\mathbf{n}_{i}}\qquad(i\in\mathbb{N})\\\ {\tt
bne}_{\mathbf{n}_{\omega}}&\coloneqq&x\;|\;{\tt bne}_{\mathbf{n}_{\omega}}{\tt
bno}_{\mathbf{n}_{\omega}}\\\\[5.69046pt] {\tt
bno}_{\mathbf{n}_{k}}&\coloneqq&\lambda x.{\tt bno}_{\mathbf{n}_{k}}\;|\;{\tt
bne}_{\mathbf{n}_{k}}\qquad(k\in\mathbb{N}^{\omega})\end{array}$

Remarkably, the partial terms in ${\tt bno}_{\mathbf{n}_{k}}$ are precise
enough to perfectly observe the $\mathrm{n}_{k}$-normal forms and entirely
determine them up to depth $k$, so that the dCBN instances of Axioms C and D
hold.

#### Quantitative Stratified Genericity.

We now have all the material to enhance our dCBN qualitative surface
genericity (Section 5.1) into a stronger quantitative stratified genericity
result.

[dCBN Quantitative Stratified
Genericity]theoremCbnQuantitativeStratifiedGenericity Let
$k\in\mathbb{N}^{\omega}$. If $t\in\Lambda$ is dCBN-meaningless and
$\mathtt{C}\\!\left<t\right>$ is $\mathrm{n}_{k}$-normalizing, then there is
$i\in\mathbb{N}$ such that, for every $u\in\Lambda$, there are
$t^{\prime},u^{\prime}\in{\tt no}_{\mathrm{n}_{k}}$ such that
$\mathtt{C}\\!\left<t\right>\rightarrow^{i}_{\mathrm{n}_{k}}t^{\prime}\;\overset{\scriptscriptstyle
k}{\approx}\;u^{\prime}\;\sideset{{}^{i}_{\mathrm{n}_{k}\\!\\!\\!\\!}}{}{\operatorname{\leftarrow}}\;\mathtt{C}\\!\left<u\right>$.

The proof of this theorem follows the exact same schematic as Theorem 4.5. A
particular case is given by the following statement since $k$-equality for
$k=\omega$ is just the equality between terms.

###### Corollary 5.6 (dCBN Quantitative Full Genericity).

If $t\in\Lambda$ is dCBN-meaningless and
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{n}_{\omega}}s$ where $s$
is $\mathrm{n}_{\omega}$-normal, then there is $i\in\mathbb{N}$ such that, for
every $u\in\Lambda$,
$\mathtt{C}\\!\left<t\right>\rightarrow^{i}_{\mathrm{n}_{\omega}}s\;\sideset{{}^{i}_{\mathrm{n}_{\omega}\\!\\!\\!\\!}}{}{\operatorname{\leftarrow}}\;\mathtt{C}\\!\left<u\right>$.

##  6\. Theories

In this section, we prove that the meaningful (resp. observational) theory
$\bm{\mathcal{H}}$ (resp. $\bm{\mathcal{H}}^{*}$) generated by dCBV and dCBN
is _consistent_ (resp. _consistent_ and _sensible_). This is when genericity
comes into play. To streamline the presentation of our approach and avoid
unnecessary repetitions, we employ a _unified reasoning_ methodology for both
frameworks. To achieve this, we begin by presenting the proofs of consistency
and sensibility for a _generic_ calculus (Section 6.1), for which we assume a
set of axioms, mirroring our approach when describing the methodology used to
obtain genericity (Section 3). Then, we instantiate the generic calculus with
dCBV (Section 6.2) and dCBN (Section 6.3), showing that each of these
instantiations enjoys the axioms stated before for the generic calculus.

###  6.1. Generic Theories

We introduce here a generic calculus and three associated theories: the
computational theory $\bm{\mathcal{R}}$, the meaningful theory
$\bm{\mathcal{H}}$ and the observational theory $\bm{\mathcal{H}}^{*}$. We
provide an axiomatized proof of the consistency of $\bm{\mathcal{H}}$, and of
the consistency and sensibility of $\bm{\mathcal{H}}^{*}$.

Let us consider a generic calculus, based on the set of terms $\Lambda$
equipped with a notion of stratified contexts for all
$k\in\mathbb{N}^{\omega}$. In particular, _full contexts_ ($k=\omega$) are
denoted by $\mathtt{C}$. We also assume the generic calculus to be equipped
with a set $\mathsf{R}$ of rewrite rules. The following definitions should be
subscripted by $\mathsf{R}$ but we omit it for better readability. As in
Section 3, we also assume the generic calculus to be equipped with a notion of
_stratified reduction_ $\rightarrow_{k}$ generated by the closure of the rules
in $\mathsf{R}$ by stratified contexts of level $k\in\mathbb{N}^{\omega}$.
This gives rise to corresponding notions of $k$-normal form and
$k$-normalization. In particular the generic calculus is equipped with a
notion of surface reduction (level $k=0$) as well as a notion of full
reduction (level $k=\omega$). We also assume that the generic calculus is
equipped with an appropriate notion of  _meaningfulness_.

A theory is a set of equations of the form $t\doteq u$ with $t,u\in\Lambda$. A
congruence $\mathcal{C}_{\mathsf{B}}$ is the smallest theory containing a set
$\mathsf{B}$ of _base equations_ , and closed by reflexivity, symmetry,
transitivity and full contexts. Alternatively, $\mathcal{C}_{\mathsf{B}}$ can
be specified by the rules below:

$\begin{array}[]{c}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\\!\\!\scriptsize$({\tt ref})$}}}\hbox{\hskip
5.2234pt\hbox{\hbox{\hbox{}\hbox{$\phantom{t\doteq
u}\hfil\lx@intercol$}}\hbox{$t\doteq t$}}}\par}\par}}}$}\hskip
14.22636pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\\!\\!\scriptsize$({\tt
sym})$}}}\hbox{\hbox{\hbox{}\hbox{$t\doteq u$}}\hbox{$u\doteq
t$}}\par}\par}}}$}\hskip
14.22636pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\\!\\!\scriptsize$({\tt tra})$}}}\hbox{\hskip
5.53821pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
10.00002pt\hbox{\hbox{\hbox{}\hbox{$t\doteq s$}}\hbox{$s\doteq
u$}}}}\hbox{$t\doteq u$}}}\par}\par}}}$}\\\\[8.5359pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
14.16682pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\\!\scriptsize$({\tt
ctx})$}}}\hbox{\hbox{\hbox{}\hbox{$t\doteq
u\hfil\lx@intercol$}}\hbox{$\mathtt{C}\\!\left<t\right>\doteq\mathtt{C}\\!\left<u\right>$}}\par}\par}}}$}\hskip
14.22636pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\\!\\!\scriptsize$({\tt
base})$}}}\hbox{\hskip
7.5695pt\hbox{\hbox{\hbox{}\hbox{$(t,u)\\!\in\\!\mathsf{B}$}}\hbox{$t\doteq
u$}}}\par}\par}}}$}\end{array}$

Given a theory $\mathsf{B}$, we write $\mathsf{B}\vdash t\doteq u$ if $t\doteq
u\in\mathcal{C}_{\mathsf{B}}$, and $\mathsf{B}\not\vdash t\doteq u$ if
$t\doteq u\notin\mathcal{C}_{\mathsf{B}}$. A congruence
$\mathcal{C}_{\mathsf{B}}$ is consistent, if it does not equate all terms
(i.e. there are $t,u\in\Lambda$ such that $\mathsf{B}\not\vdash t\doteq u$).

The computational theory $\bm{\mathcal{R}}$ is the congruence
$\mathcal{C}_{\mathsf{R}}$ (recall that $\mathsf{R}$ is the set of rewrite
rules of the generic calculus). We write
$t\mathbin{={{}_{\\!\\!\mathsf{R}}}}u$ for the reflexive, symmetric,
transitive closure of the reduction $\rightarrow_{\omega}$. As expected, the
congruence $\bm{\mathcal{R}}$ axiomatizes the equivalence
$\mathbin{={{}_{\\!\\!\mathsf{R}}}}$:

lemmaGenThTCharacterization Let $t,u\in\Lambda$, then $\mathsf{R}\vdash
t\doteq u$ if and only if $t\mathbin{={{}_{\\!\\!\mathsf{R}}}}u$.

A $\lambda$-theory $\bm{\mathcal{E}}$ is any congruence containing the
computational theory $\bm{\mathcal{R}}$, that is,
$\bm{\mathcal{E}}=\mathcal{C}_{\mathsf{B}}$ for some
$\mathsf{B}\supseteq\mathsf{R}$. A $\lambda$-theory $\mathcal{C}_{\mathsf{B}}$
is sensible if it equates all meaningless terms, that is, $\mathsf{B}\vdash
t\doteq u$ if $t$ and $u$ are meaningless. The meaningful theory
$\bm{\mathcal{H}}$ is the smallest sensible $\lambda$-theory (i.e.
$\bm{\mathcal{H}}\coloneqq\mathcal{C}_{\mathsf{H}}$ where
$\mathsf{H}\coloneqq\mathsf{R}\cup\\{(t,u)\;|\;t,u\text{ meaningless}\\}$).

Working directly on $\bm{\mathcal{H}}$ is not easy, but it is possible to
refine its specification following (Barendregt, 1984) (see Appendix D for
details).

In order to abstractly prove consistency of the $\lambda$-theory
$\bm{\mathcal{H}}$, we first assume consistency of the $\lambda$-theory
$\bm{\mathcal{R}}$ as an _axiom_.

###### Axiom E (Consistency).

The $\lambda$-theory $\bm{\mathcal{R}}$ is consistent.

Why this assumption is reasonable? The $\lambda$-theory $\bm{\mathcal{H}}$ is
built as an extension of $\bm{\mathcal{R}}$ to ensure its invariance under
reduction. If $\bm{\mathcal{R}}$ is inconsistent then all its extensions
(including $\bm{\mathcal{H}}$) are inconsistent as well, regardless of the
definition of meaningfulness. Taking $\bm{\mathcal{R}}$ to be consistent as an
axiom is therefore reasonable in our framework.

We abstractly prove that consistency of $\bm{\mathcal{H}}$ can be reduced to
that of $\bm{\mathcal{R}}$, following the same ideas in (Barendregt, 1984).
For that, we start by showing in particular that $\bm{\mathcal{H}}$ and
$\bm{\mathcal{R}}$ both agree on $\omega$-normal forms, a forthcoming property
(Axiom F) which uses the fact that the generic calculus satisfies the
following Axioms E and F.

[Confluence and Normal Form]assumptionAssumptionTheoryFullConfluence Reduction
$\rightarrow_{\omega}$ is confluent and there exists an $\omega$-normal form.

Indeed, normal forms represent the results of computations, thus being without
$\omega$-normal forms would mean that the calculus never yields a result
(also, variables are $\omega$-normal in any reasonable rewriting system).
Moreover, confluence of $\rightarrow_{\omega}$ implies that two evaluations
from the same term cannot yield different outcomes. Hence, Axiom E is a
perfectly reasonable assumption.

###### Axiom F (Full Genericity).

If $t\in\Lambda$ is meaningless and
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\omega}s$ where $s$ is
$\omega$-normal, then for every $u\in\Lambda$,
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\omega}s\;\sideset{{}^{*}_{\omega}}{}{\operatorname{\leftarrow}}\;\mathtt{C}\\!\left<u\right>$.

Since $\bm{\mathcal{H}}$ is the smallest sensible $\lambda$-theory, proving
$\mathtt{C}\\!\left<t\right>\doteq\mathtt{C}\\!\left<u\right>$ in
$\bm{\mathcal{H}}$ can be done either by using the rules for
$\bm{\mathcal{R}}$ or –thanks to sensibility– by replacing $t$ with $u$ when
they are both meaningless. Full genericity (Axiom F) allows one to do that
directly in $\bm{\mathcal{R}}$, in the special case where
$\mathtt{C}\\!\left<t\right>$ or $\mathtt{C}\\!\left<u\right>$ is
$\omega$-normalizing. Therefore,

lemmaGenTheoryHAndLambdaAgreeFNF If $u\in\Lambda$ has a $\omega$-normal form,
then for any $t\in\Lambda$, if $\mathsf{H}\vdash t\doteq u$ then
$\mathsf{R}\vdash t\doteq u$.

###### Theorem 6.1.

The $\lambda$-theory $\bm{\mathcal{H}}$ is consistent.

###### Proof.

By Axiom E, there exist two terms $t_{1},t_{2}\in\Lambda$ such that
$t_{1}\doteq t_{2}$ is not provable in $\bm{\mathcal{R}}$. Moreover, using
Axiom E, there exists an $\omega$-normal form $u\in\Lambda$. Suppose by absurd
that $\bm{\mathcal{H}}$ is inconsistent, then $\mathsf{H}\vdash t_{1}\doteq u$
and $\mathsf{H}\vdash u\doteq t_{2}$. Thus $\mathsf{R}\vdash t_{1}\doteq u$
and $\mathsf{R}\vdash u\doteq t_{2}$ using Axiom F, hence $\mathsf{R}\vdash
t_{1}\doteq t_{2}$ by transitivity which contradicts Axiom E. One then
concludes that $\bm{\mathcal{H}}$ is consistent. ∎

Now we study the observational theory $\bm{\mathcal{H}}^{*}$ associated with a
generic calculus, which is defined by the following set:

$\bm{\mathcal{H}}^{*}\coloneqq\\{t\doteq
u\;|\;\forall\;\mathtt{C},\;\mathtt{C}\\!\left<t\right>\text{ meaningful
}\Leftrightarrow\mathtt{C}\\!\left<u\right>\text{ meaningful}\\}$

To prove that the theory $\bm{\mathcal{H}}^{*}$ is a consistent and sensible
$\lambda$-theory, we use the following complementary axioms, which are natural
and self-explained, as well as consistency of $\bm{\mathcal{H}}$ (Theorem
6.1).

###### Axiom G (Meaningfulness Stability).

Let $t,u\in\Lambda$ such that $t\rightarrow_{\omega}u$, then $t$ is meaningful
if and only if $u$ is meaningful.

###### Axiom H (Surface Genericity).

If $t\in\Lambda$ is meaningless and $\mathtt{C}\\!\left<t\right>$ is
meaningful, then for any $u\in\Lambda$, $\mathtt{C}\\!\left<u\right>$ is
meaningful.

###### Axiom I (Meaningful Existence).

There is a meaningless term in the generic calculus.

theoremGenTheoryHStarConsistent $\bm{\mathcal{H}}^{*}$ is a sensible and
consistent $\lambda$-theory.

###### Proof.

($\lambda$-theory) It suffices to show
$\bm{\mathcal{H}}^{*}=\mathcal{C}_{\bm{\mathcal{H}}^{*}}$ and
$\mathsf{R}\subseteq\bm{\mathcal{H}}^{*}$. If $(t,u)\in\mathsf{R}$ then, for
every full context $\mathtt{C}$, we have
$\mathtt{C}\\!\left<t\right>\rightarrow_{\omega}\mathtt{C}\\!\left<u\right>$
and so $t\doteq u\in\bm{\mathcal{H}}^{*}$ by Axiom G. By definition of
$\bm{\mathcal{H}}^{*}$, it is easy to check that
$t\\!\doteq\\!u\in\bm{\mathcal{H}}^{*}$ iff
$t\\!\doteq\\!u\in\mathcal{C}_{\bm{\mathcal{H}}^{*}}$.

(Sensibility) As $\bm{\mathcal{H}}^{*}$ is a $\lambda$-theory, it suffices to
show that $\bm{\mathcal{H}}^{*}$ equates all meaningless terms. Let
$t,u\in\Lambda$ be meaningless. By surface genericity (Axiom H),
$\mathtt{C}\\!\left<t\right>$ is meaningful iff so is
$\mathtt{C}\\!\left<u\right>$, thus $t\doteq u\in\bm{\mathcal{H}}^{*}$.

(Consistency) As $\bm{\mathcal{H}}$ is consistent (Theorem 6.1),
$\mathsf{H}\not\vdash t\doteq u$ for some $t,u\in\Lambda$. This means that $t$
or $u$ –say $t$– is meaningful (otherwise $\mathsf{H}\vdash t\doteq u$). By
Axiom I, there is a meaningless $s\in\Lambda$. For $\mathtt{C}=\diamond$,
$\mathtt{C}\\!\left<t\right>=t$ is meaningful and
$\mathtt{C}\\!\left<s\right>=s$ is meaningless, then $t\doteq
s\notin\bm{\mathcal{H}}^{*}=\mathcal{C}_{\bm{\mathcal{H}}^{*}}$ thus
$\bm{\mathcal{H}}^{*}\not\vdash t\doteq s$, that is, $\bm{\mathcal{H}}^{*}$ is
consistent. ∎

###  6.2. dCBV Theories

We now instantiate the generic theories above to the dCBV-calculus: let
$\bm{\mathcal{H}}_{{\tt dCBV}}$ (resp. $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$) be
the instantiation of $\bm{\mathcal{H}}$ (resp. $\bm{\mathcal{H}}^{*}$)
obtained by replacing “meaningful” with “dCBV-meaningful” (see Definition 2.3)
in its definiton. Thus, we prove consistency (resp. and sensibility) of
$\bm{\mathcal{H}}_{{\tt dCBV}}$ (resp. $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$).
We also prove that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ is the _unique_
_maximal_ consistent $\lambda_{{\tt dCBV}}$-theory extending
$\bm{\mathcal{H}}_{{\tt dCBV}}$.

###### Theorem 6.2.

The dCBV-calculus verifies Axioms E, F, E, G, H and I.

###### Proof.

For Axiom E see (Accattoli and Paolini, 2012). Axiom F is a special case of
Corollary 4.6. Axiom G is proved using Full Subject Reduction and Expansion in
system $\mathcal{V}$ (Bucciarelli et al., 2020) and Lemma 2.4. For Axiom H we
use Section 2. For Axiom I: the term $\Omega$ is
$\rightarrow_{\mathrm{v}_{0}}$ divergent thus by Lemma 2.4, one concludes that
it is dCBV-meaningless. ∎

###### Corollary 6.3.

  1. (1)

The $\lambda_{{\tt dCBV}}$-theory $\bm{\mathcal{H}}_{{\tt dCBV}}$ is
consistent.

  2. (2)

The theory $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ is a sensible and consistent
$\lambda_{{\tt dCBV}}$-theory.

Sensibility means that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ is an extension of
$\bm{\mathcal{H}}_{{\tt dCBV}}$. We prove that $\bm{\mathcal{H}}^{*}_{{\tt
dCBV}}$ is actually the unique consistent maximal $\lambda_{{\tt
dCBV}}$-theory extending $\bm{\mathcal{H}}_{{\tt dCBV}}$, where maximal means
that, for every $t,u\in\Lambda$, either $\bm{\mathcal{H}}^{*}_{{\tt
dCBV}}\vdash t\doteq u$ or $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ extended with
the base equation $t\doteq u$ is inconsistent. For that we need the following
property.

lemmaCbvTheoryHExtended Let $t,u\in\Lambda$. If $\bm{\mathcal{H}}_{{\tt
dCBV}}$ is extended with the base equation $t\doteq u$ is consistent, then for
all full context $\mathtt{C}$, one has that $\mathtt{C}\\!\left<t\right>$ is
dCBV-meaningful iff $\mathtt{C}\\!\left<u\right>$ is dCBV-meaningful.

By Corollary 6.3 and sensibility of $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ (Axiom
I), we have:

corollaryCbvTheoryHStarHPComplete The theory $\bm{\mathcal{H}}^{*}_{{\tt
dCBV}}$ is the unique maximal consistent and sensible $\lambda_{{\tt
dCBV}}$-theory.

The $\lambda_{{\tt dCBV}}$-theory $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ equates
_more_ then $\bm{\mathcal{H}}_{{\tt dCBV}}$. For example,
$\mathtt{I}\doteq\lambda x.\lambda y.xy$ is provable in
$\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ but not in $\bm{\mathcal{H}}_{{\tt
dCBV}}$.

Finally, we can now prove our last contribution: the $\lambda_{{\tt
dCBV}}$-theory $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ coincides with the
observational equivalence $\cong$ defined in Section 2. To prove this, we
define the auxiliary notion of open-observational equivalence $\cong^{o}$ in
dCBV: given $t,u\in\Lambda$, $t\cong^{o}u$ if for _every_ full context
$\mathtt{C}$,
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{v}_{\omega}}v_{1}$ iff
$\mathtt{C}\\!\left<u\right>\rightarrow^{*}_{\mathrm{v}_{\omega}}v_{2}$ for
some values $v_{1},v_{2}\in\Upsilon$. Note that, differently from $\cong$,
$\cong^{o}$ quantifies over all full contexts and not only on _closing_ full
contexts, hence $\cong^{o}\,\subseteq\,\cong$.

###### Corollary 6.4.

Let $t,u\in\Lambda$, then $t\cong u$ iff $\bm{\mathcal{H}}^{*}_{{\tt
dCBV}}\vdash t\doteq u$.

###### Proof.

$\bm{\mathcal{H}}^{*}_{{\tt dCBV}}\vdash t\doteq u$ means that for every full
context $\mathtt{C}$, $\mathtt{C}\\!\left<t\right>$ is meaningless iff
$\mathtt{C}\\!\left<u\right>$ is. By quantitative stratified genericity with
$k=0$ (Theorem 4.5), this is equivalent to say that, for every full context
$\mathtt{C}$, $\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{v}_{0}}v$
for some value $v$ iff
$\mathtt{C}\\!\left<u\right>\rightarrow^{*}_{\mathrm{v}_{0}}v^{\prime}$ for
some value $v^{\prime}$, that is, $t\cong^{o}u$. Thus,
$\bm{\mathcal{H}}^{*}_{{\tt dCBV}}\vdash t\doteq u$ if and only if
$t\cong^{o}u$.

Therefore, as $\cong^{o}\,\subseteq\,\cong$, if $\bm{\mathcal{H}}^{*}_{{\tt
dCBV}}\vdash t\doteq u$ then $t\cong u$, in particular $\cong$ is sensible
(since so is $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$, Corollary 6.3). As $\cong$
is a consistent (clearly, $\mathtt{I}\not\cong\Omega$) $\lambda$-theory
(trivial), one has that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}\vdash t\doteq u$ if
and only if $t\cong u$, by maximality of $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$
(Corollary 6.3). ∎

Corollaries 6.3, 6.3 and 6.4 are among our main contributions. In particular,
the fact that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}=\ \cong$ means that two
different approaches to define a semantics in dCBV actually coincide. This
further backs up the idea that what we call dCBV-meaningfulness approppriately
represents meaningfuness in dCBV.

###  6.3. dCBN Theories

We now instantiate the generic theories of Section 6.1 to the dCBN-calculus:
let $\bm{\mathcal{H}}_{{\tt dCBN}}$ (resp. $\bm{\mathcal{H}}^{*}_{{\tt
dCBN}}$) be the instantiation of $\bm{\mathcal{H}}$ (resp.
$\bm{\mathcal{H}}^{*}$) obtained by replacing “meaningful” with dCBN-
meaningful (see Definition 5.3) Thus, we prove that $\bm{\mathcal{H}}_{{\tt
dCBN}}$ (resp. $\bm{\mathcal{H}}^{*}_{{\tt dCBN}}$) is consistent (resp.
consistent and sensible).

###### Theorem 6.5.

The dCBN-calculus verifies Axioms E, F, E, G, H and I.

###### Proof.

For Axiom E see (Bucciarelli et al., 2023). For Axiom F, it is a special case
of Section 5.2. For Axiom G is proved using Full Subject Reduction and
Expansion in system $\mathcal{N}$ (Bucciarelli et al., 2020) and Lemma 5.4.
For Axiom H we use Section 5.1. For Axiom I: the term $\Omega$ is
$\rightarrow_{\mathrm{n}_{0}}$ divergent thus by Lemma 5.4, one concludes that
it is dCBN-meaningless. ∎

###### Corollary 6.6.

  1. (1)

The $\lambda_{{\tt dCBN}}$-theory $\bm{\mathcal{H}}_{{\tt dCBN}}$ is
consistent.

  2. (2)

The theory $\bm{\mathcal{H}}^{*}_{{\tt dCBN}}$ is a sensible and consistent
$\lambda_{{\tt dCBN}}$-theory.

Using arguments similar to dCBV, we can establish that the theory
$\bm{\mathcal{H}}^{*}_{{\tt dCBN}}$ is the unique maximal consistent
$\lambda_{{\tt dCBN}}$-theory extending $\bm{\mathcal{H}}_{{\tt dCBN}}$ and
coincides with the observational equivalence where the observable is being
$\mathrm{n}_{0}$-normalizing, analogously to what is well-known for the pure
$\lambda$-calculus (Hyland, 1975; Wadsworth, 1976; Barendregt, 1984).

##  7\. Related Works and Conclusion

#### Related Works

There are at least six different methods to prove (full) _genericity_ in CbN.

  * •

Barendregt (Barendregt, 1984, Ch. 14.3) uses a tree-topology on terms based on
Böhm trees, and continuity of term application with respect to it.

  * •

Takahashi’s (Takahashi, 1994) operational proof exploits the fact that the
solvable terms are precisely the ones having a head normal form.

  * •

Kuper’s (Kuper, 1995) operational proof is based on leftmost reduction and can
also be extended to other calculi (e.g. with types, PCF).

  * •

Kennaway  _et al._ (Kennaway et al., 1999) abstractly provide three axioms in
order for a set of $\lambda$-terms to be coherently equated and satisfy
genericity.

  * •

Ghilezan (Ghilezan01) exploits a topology induced by an intersection type
system and, as in (Barendregt, 1984), continuity of application with respect
to it.

  * •

Barbarossa and Manzonetto (Barbarossa and Manzonetto, 2020) prove that
genericity follows from the commutation of normalization and Taylor expansion.

Let us see why the existing methods to prove CbN genericity cannot be easily
adapted to CbV. Barendregt’s method does not easily lift to CbV because CbV
_Böhm trees_ and their properties are still to be explored; a first attempt is
in (Kerinec et al., 2020, 2021). Takahashi’s method is based on _lifting_
genericity with respect to substitutions to genericity with respect to _full
contexts_ : such a method breaks in CbV, because it relies on adding
abstractions, which in CbV (and not in CbN) can turn a meaningless term into a
meaningful one. Kuper’s approach relies on _leftmost_ reduction, which is a
normalizing strategy for CbN; the equivalent normalizing strategy for CbV
(Accattoli et al., 2021, 2023) is involuted and not really leftmost in a
syntactic sense, so this method would not be handy. Kennaway et al.’s
_axiomatics_ targets first-order term rewriting systems and CbN
$\lambda$-calculus, but it is unclear how to adapt the technique to _higher-
order_ reduction, in particular to reduction at a distance. Ghilezan’s
approach can only work with _idempotent_ intersection types, and this makes
impossible to extract any quantitative information as we do. Finally, it is
tedious to adapt Barbarossa and Manzonetto’s method to _CbV Taylor expansion_
, whose underlying properties are still not well explored: some preliminary
attempts appear in (Ehrhard, 2012; Carraro and Guerrieri, 2014; Kerinec et
al., 2020, 2021). Moreover the Taylor expansion exploits some kind of non-
determinism that in fact is not needed to prove genericity. Indeed, our
approach still uses some kind of approximations of $\lambda$-terms, but
contrary to the Taylor expansion, its reduction rules are not non-
deterministic.

Genericity and $\lambda$-theories of CbV was scarcely approached in the
literature on CbV. The non-adequacy problem mentioned in Section 2 for
Plotkin’s CbV was already noticed by Paolini, Ronchi Della Rocca _et al._
(Paolini and Ronchi Della Rocca, 1999; Rocca and Paolini, 2004; Accattoli and
Paolini, 2012; Carraro and Guerrieri, 2014; Guerrieri et al., 2017), who
studied different properties of CbV solvability. As mentioned before, this
notion does not yield a consistent associated theory.

Garcia-Perez and Nogueira (García-Pérez and Nogueira, 2016) proposed a
_different_ notion of solvability for Plotkin’s CbV that takes into account
the _order_ of a term (number of arguments it can take), for which they prove
genericity. The $\lambda$-theory generated by their notion of solvability is
different from $\bm{\mathcal{H}}_{{\tt dCBV}}$ and it can also be proved to be
consistent. However, the original calculus still suffers from _non-adequacy_.

Independently, Accattoli and Lancelot (Accattoli and Lancelot, 2024) have
recently developed an alternative study of what we call _surface_ genericity
in this paper, for both CbV and CbN, via different tools (e.g. bisimulations).
As far as we know, the challenging proof of _full_ genericity for dCBV-
meaningless terms has never been proved before.

The consistency of the theory $\bm{\mathcal{H}}_{{\tt dCBV}}$ is already
proved in the literature —or can be easily derived— from the consistency of
some related $\lambda_{v}$-theories (Egidi et al., 1992; Paolini and Ronchi
Della Rocca, 1999; Carraro and Guerrieri, 2014; Accattoli and Guerrieri, 2022;
Accattoli and Lancelot, 2024). However, this paper provides the first proof of
consistency of the theory $\bm{\mathcal{H}}_{{\tt dCBV}}$ that is _direct_
—not based on consistency of some related theories— and _operational_ —not
based on semantical methods.

It would also be reasonable to study $\lambda$-theories that are consistent
but non sensible, as it is done for CbN, see e.g. (Barendregt92a).

#### Conclusion

We introduce a novel technique to prove _stratified_ genericity, yielding both
_surface_ and _full_ genericity as special cases. Remarkably, this technique
is specified by an _axiomatic_ approach which applies to both _call-by-value_
and _call-by-name_. Moreover, our genericity theorems are not only
_qualitative_ (as usual in the literature) but also _quantitative_ , capturing
the fact that replacing a meaningless subterm in a normalizing term $t$ does
not affect the number of steps to reach the normal form of $t$.

Furthermore, we establish the _first direct_ and _operational_ proof that the
smallest congruence relation resulting from equating all meaningless
$\lambda$-terms is _consistent_. We substantiate this proof by introducing an
_axiomatic_ approach, which applies to both _call-by-value_ and _call-by-name_
paradigms. Moreover, we show that these two theories admit a unique _maximal_
consistent extension which coincides with well-known _observational
equivalences_.

Alternatively, our methodology based on meaningful approximants can be
replaced by a non-idempotent intersection type system characterizing full
normalization, as (Bucciarelli et al., 2017; Kesner and Ventura, 2014) for
dCBN and (Accattoli et al., 2023) for dCBV. The obtained result would however
be weaker, since such typing systems only characterize normalizability of
terms, but do not provide any information about the form of the resulting
normal forms. Some ideas coming from (Bernadet and Lengrand, 2011) will be
studied in this direction.

Through the tools developed in this paper, we aim to extend our approach to
establish genericity within a more encompassing unifying framework, such as
call-by-push-value (Levy, 1999) or the bang calculus (Ehrhard, 2016; Ehrhard
and Guerrieri, 2016; Guerrieri and Manzonetto, 2018; Bucciarelli et al., 2020,
2023; ArrialGuerrieriKesner23). These frameworks, by explicitly distinguishing
between values and computations, have the capability to subsume both call-by-
value and call-by-name at the same time.

An equally challenging model of computation, still unexplored in terms of
meaningfulness and genericity, is call-by-need (Ariola and Felleisen, 1997;
Ariola et al., 1995) We believe that by stratifying the notion of call-by-need
contexts and reduction, we can construct a well-defined notion of
meaningfulness and then achieve a corresponding genericity result.

We are also interested in understanding the relation between the notion of CbV
meaningless studied here and the one of _unsolvability of order $0$_
introduced by (García-Pérez and Nogueira, 2016) for Plotkin’s CbV.

The notion of meaningfulness in CbN (solvability) is strictly related to the
one of Böhm tree, which represents a term as a possible infinite tree that is
the sup of its approximations. Our notion of meaningful approximation yields a
notion of Böhm tree in CbV, which slightly differs from the one introduced in
(Kerinec et al., 2020, 2021) (because of their different notion of
approximation). It would be interesting to compare the two notions of CbV Böhm
trees and characterize the $\lambda$-theories they generate in a denotational
or operational way.

We believe that our approach to approximation and stratification are powerful
tools that can be used not only to prove genericity but also other important
results in $\lambda$-calculus such as Scott’s continuity, Berry’s stability or
Kahn and Plotkin’s sequentiality theory, simplifing the proofs provided in
(Barbarossa and Manzonetto, 2020) via the notion of Taylor expansion.

An open question in CbV was the existence of an appropriate notion of
meaningfulness and its associated $\lambda$-theory fulfilling _all_ the basic
properties and criteria we discussed in Section 1, which are well-known for
the theory $\bm{\mathcal{H}}$ in CbN. This paper fills the gap by answering
positively to this fundamental question, through a new approach that is robust
as it works uniformly for CbN and CbV.

## References

  * (1)
  * Accattoli et al. (2021) Beniamino Accattoli, Andrea Condoluci, and Claudio Sacerdoti Coen. 2021.  Strong Call-by-Value is Reasonable, Implosively. In _36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021_ (June 29 - July 2, 2021). IEEE, Rome, Italy, 1–14.  https://doi.org/10.1109/LICS52264.2021.9470630
  * Accattoli et al. (2020) Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. 2020.  Tight typings and split bounds, fully developed.  _Journal of Functional Programming_ 30 (2020), e14.  https://doi.org/10.1017/S095679682000012X
  * Accattoli and Guerrieri (2016) Beniamino Accattoli and Giulio Guerrieri. 2016.  Open Call-by-Value. In _Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings_ _(Lecture Notes in Computer Science, Vol. 10017)_ , Atsushi Igarashi (Ed.). 206–226.  https://doi.org/10.1007/978-3-319-47958-3_12
  * Accattoli and Guerrieri (2022) Beniamino Accattoli and Giulio Guerrieri. 2022.  The theory of call-by-value solvability.  _Proceedings of the ACM on Programming Languages_ 6, ICFP (2022), 855–885.  https://doi.org/10.1145/3547652
  * Accattoli et al. (2023) Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. 2023\.  Strong Call-by-Value and Multi Types. In _Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Proceedings_ (December 4-8, 2023) _(Lecture Notes in Computer Science, Vol. 14446)_ , Erika Ábrahám, Clemens Dubslaff, and Silvia Lizeth Tapia Tarifa (Eds.). Springer, Lima, Peru, 196–215.  https://doi.org/10.1007/978-3-031-47963-2_13
  * Accattoli and Kesner (2010) Beniamino Accattoli and Delia Kesner. 2010.  The structural lambda-calculus. In _Proceedings of 24th EACSL Conference on Computer Science Logic_ _(LNCS, Vol. 6247)_ , Anuj Dawar and Helmut Veith (Eds.). Springer, Brno, Czech Republic, 381–395.
  * Accattoli and Kesner (2012) Beniamino Accattoli and Delia Kesner. 2012.  The Permutative $\lambda$-Calculus. In _Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings_ _(Lecture Notes in Computer Science, Vol. 7180)_ , Nikolaj S. Bjørner and Andrei Voronkov (Eds.). Springer, 23–36.  https://doi.org/10.1007/978-3-642-28717-6_5
  * Accattoli and Lancelot (2024) Beniamino Accattoli and Adrienne Lancelot. 2024.  Light Genericity. In _Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings_ _(Lecture Notes in Computer Science)_ , Naoki Kobayashi and James Worrell (Eds.). Springer.  To appear.
  * Accattoli and Paolini (2012) Beniamino Accattoli and Luca Paolini. 2012.  Call-by-Value Solvability, Revisited. In _FLOPS_ (May 23-25, 2012) _(LNCS, Vol. 7294)_ , Tom Schrijvers and Peter Thiemann (Eds.). Springer, Kobe, Japan, 4–16.
  * Ariola and Felleisen (1997) Zena M. Ariola and Matthias Felleisen. 1997.  The Call-By-Need lambda Calculus.  _Journal of Functional Programming_ 7, 3 (1997), 265–301.  https://doi.org/10.1017/S0956796897002724
  * Ariola et al. (1995) Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. 1995.  The Call-by-Need Lambda Calculus. In _Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (January 23-25, 1995), Ron K. Cytron and Peter Lee (Eds.). ACM Press, San Francisco, California, USA, 233–246.  https://doi.org/10.1145/199448.199507
  * Barbarossa and Manzonetto (2020) Davide Barbarossa and Giulio Manzonetto. 2020.  Taylor subsumes Scott, Berry, Kahn and Plotkin.  _Proceedings of the ACM on Programming Languages_ 4, POPL (2020), 1–23.  https://doi.org/10.1145/3371069
  * Barendregt (1971) Henk Barendregt. 1971\.  _Some extensional term models for combinatory logics and $\lambda$-calculi_.  Ph. D. Dissertation. Univ. Utrecht.
  * Barendregt (1973) Henk Barendregt. 1973\.  A Characterization of Terms of the lambda I-Calculus Having a Normal Form.  _Journal Symbolic Logic_ 38, 3 (1973), 441–445.  https://doi.org/10.2307/2273041
  * Barendregt (1977) Henk Barendregt. 1977\.  Solvability in lambda-calculi. In _Colloque international de logique : Clermont-Ferrand, 18-25 juillet 1975_ , M. Guillaume (Ed.). Éditions du C.N.R.S., Paris, 209–219.
  * Barendregt (1984) Henk Barendregt. 1984\.  _The Lambda Calculus: Its Syntax and Semantics_ (revised ed.). Studies in logic and the foundation of mathematics, Vol. 103.  North-Holland, Amsterdam.
  * Barendregt and Manzonetto (2022) Henk Barendregt and Giulio Manzonetto. 2022.  _A Lambda Calculus Satellite_.  College Publications.  https://www.collegepublications.co.uk/logic/mlf/?00035
  * Berline (2000) Chantal Berline. 2000\.  From computation to foundations via functions and application: The -calculus and its webbed models.  _Theoretical Computer Science_ 249, 1 (2000), 81–161.  https://doi.org/10.1016/S0304-3975(00)00057-8
  * Berline et al. (2007) Chantal Berline, Giulio Manzonetto, and Antonino Salibra. 2007\.  Lambda Theories of Effective Lambda Models. In _Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Proceedings_ (September 11-15, 2007) _(Lecture Notes in Computer Science, Vol. 4646)_ , Jacques Duparc and Thomas A. Henzinger (Eds.). Springer, Lausanne, Switzerland, 268–282.  https://doi.org/10.1007/978-3-540-74915-8_22
  * Berline et al. (2009) Chantal Berline, Giulio Manzonetto, and Antonino Salibra. 2009\.  Effective lambda-models versus recursively enumerable lambda-theories.  _Mathematical Structures in Computer Science_ 19, 5 (2009), 897–942.  https://doi.org/10.1017/S0960129509990053
  * Bernadet and Lengrand (2011) Alexis Bernadet and Stéphane Lengrand. 2011.  Complexity of Strongly Normalising -Terms via Non-idempotent Intersection Types. In _FOSSACS_ _(LNCS, Vol. 6604)_ , Martin Hofmann (Ed.). Springer, 88–107.
  * Breuvart (2014) Flavien Breuvart. 2014\.  On the characterization of models of _H_. In _Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14_ (July 14 - 18, 2014), Thomas A. Henzinger and Dale Miller (Eds.). ACM, Vienna, Austria, 24:1–24:10.  https://doi.org/10.1145/2603088.2603111
  * Breuvart et al. (2016) Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. 2016.  New Results on Morris’s Observational Theory: The Benefits of Separating the Inseparable. In _1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016_ (June 22-26, 2016) _(LIPIcs, Vol. 52)_ , Delia Kesner and Brigitte Pientka (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Porto, Portugal, 15:1–15:18.  https://doi.org/10.4230/LIPICS.FSCD.2016.15
  * Bucciarelli et al. (2020) Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. 2020.  The Bang Calculus Revisited. In _Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Proceedings_ (September 14-16, 2020) _(Lecture Notes in Computer Science, Vol. 12073)_ , Keisuke Nakano and Konstantinos Sagonas (Eds.). Springer, Akita, Japan, 13–32.  https://doi.org/10.1007/978-3-030-59025-3
  * Bucciarelli et al. (2021) Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. 2021\.  Solvability = Typability + Inhabitation.  _Logical Methods in Computer Science_ 17, 1 (2021).  https://lmcs.episciences.org/7141
  * Bucciarelli et al. (2023) Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. 2023.  The bang calculus revisited.  _Information and Computation_ 293 (Aug. 2023), 105047\.  https://doi.org/10.1016/j.ic.2023.105047
  * Bucciarelli et al. (2017) Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017\.  Non-idempotent intersection types for the Lambda-Calculus.  _Logic Journal of the IGPL_ 25, 4 (07 2017), 431–464.  https://doi.org/10.1093/jigpal/jzx018 arXiv:https://academic.oup.com/jigpal/article-pdf/25/4/431/19368065/jzx018.pdf
  * Carraro and Guerrieri (2014) Alberto Carraro and Giulio Guerrieri. 2014.  A Semantical and Operational Account of Call-by-Value Solvability. In _Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings_ (April 5-13, 2014) _(Lecture Notes in Computer Science, Vol. 8412)_ , Anca Muscholl (Ed.). Springer, Grenoble, France, 103–118.  https://doi.org/10.1007/978-3-642-54830-7_7
  * CHURCH (1941) ALONZO CHURCH. 1941\.  _The Calculi of Lambda Conversion. (AM-6)_.  Princeton University Press.  http://www.jstor.org/stable/j.ctt1b9x12d
  * Coppo and Dezani-Ciancaglini (1978) Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978\.  A new type assignment for $\lambda$-terms.  _Archiv für mathematische Logik und Grundlagenforschung_ 19, 1 (1978), 139–156.  https://doi.org/10.1007/BF02011875
  * Coppo and Dezani-Ciancaglini (1980) Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980\.  An extension of the basic functionality theory for the $\lambda$-calculus.  _Notre Dame Journal of Formal Logic_ 21, 4 (1980), 685–693.  https://doi.org/10.1305/ndjfl/1093883253
  * Egidi et al. (1992) Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. 1992\.  Operational, denotational and logical descriptions: a case study.  _Fundamenta Informaticae_ 16, 1 (1992), 149–169.
  * Ehrhard (2012) Thomas Ehrhard. 2012\.  Collapsing non-idempotent intersection types. In _Computer Science Logic (CSL’12)_ _(LIPIcs, Vol. 16)_ , Patrick Cégielski and Arnaud Durand (Eds.). Schloss Dagstuhl \- Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, Fontainebleau, France, 259–273.