theorem

# Normal Form Bisimulations by Value

Beniamino Accattoli  Inria & LIX, École Polytechnique, UMR 7161France
<EMAIL_ADDRESS>,  Adrienne Lancelot  Inria & LIX, École
Polytechnique, UMR 7161France<EMAIL_ADDRESS>and  Claudia Faggian
IRIF, CNRS, Université Paris Cité, F-75013 ParisFrance<EMAIL_ADDRESS>
(2018)

###### Abstract.

Normal form bisimilarities are a natural form of program equivalence resting
on open terms, first introduced by Sangiorgi in call-by-name. The literature
contains a normal form bisimilarity for Plotkin’s call-by-value
$\lambda$-calculus, Lassen’s _enf bisimilarity_ , which validates all of
Moggi’s monadic laws and can be extended to validate $\eta$. It does not
validate, however, other relevant principles, such as the identification of
meaningless terms—validated instead by Sangiorgi’s bisimilarity—or the
commutation of $\sf{let}$s. These shortcomings are due to issues with open
terms of Plotkin’s calculus. We introduce a new call-by-value normal form
bisimilarity, deemed _net bisimilarity_ , closer in spirit to Sangiorgi’s and
satisfying the additional principles. We develop it on top of an existing
formalism designed for dealing with open terms in call-by-value. It turns out
that enf and net bisimilarities are _incomparable_ , as net bisimilarity does
not validate Moggi’s laws nor $\eta$. Moreover, there is no easy way to merge
them. To better understand the situation, we provide an analysis of the rich
range of possible call-by-value normal form bisimilarities, relating them to
Ehrhard’s relational model.

Lambda calculus, program equivalence, bisimulations, call-by-value

††copyright: acmcopyright††journalyear: 2018††doi: XXXXXXX.XXXXXXX††journal:
JACM††journalvolume: 37††journalnumber: 4††article: 111††publicationmonth: 8

##  1\. Introduction

The study of program equivalences for $\lambda$-calculi is an important topic
where semantical and operational techniques meet. Properties of program
equivalences are notoriously difficult to prove. Even the equivalence of two
terms might be challenging to establish, if the notion of equivalence is
Morris’ contextual equivalence (1968), or some variant still involving a
universal quantification, such as Abramsky’s applicative bisimilarity (1990).
Another difficulty is the fact that properties of program equivalences are
brittle, as they are not preserved by extensions of the calculus under study,
nor by restrictions, and not even by changing the evaluation strategy within
the same calculus.

It is well-known that applicative bisimilarity is fully abstract for
contextual equivalence in the untyped call-by-name weak $\lambda$-calculus
(where _weak_ stands for reduction only out of abstractions, which is standard
in functional languages) (Abramsky, 1990), as well as in Plotkin’s call-by-
value weak $\lambda$-calculus (Egidi et al., 1992; Pitts, 2012). Therefore,
one might be led to think that the call-by-name/call-by-value switch is quite
robust in the weak setting, even if it is known that its robustness breaks in
a probabilistic setting, as shown by Dal Lago et al. (2014).

This paper stems from the observation that another natural program
equivalence, Sangiorgi’s _normal form bisimilarity_ (1994) (shortened to nf-
bisimilarity), behaves differently in call-by-name (shortened to CbN) and
call-by-value (CbV), already in the untyped effect-free weak case.

##### Normal Form Bisimilarity

Normal form bisimulations are program equivalences that, instead of comparing
terms _externally_ , depending on how they behave _in contexts_ , compare them
_internally_ , by looking at the structure of their (infinitary) _normal
forms_. A distinctive feature of nf-bisimulations is that they directly
manipulate _open terms_ , to the point that Sangiorgi rather used to call them
_open bisimulations_ in his seminal paper (1994).

Sangiorgi’s CbN nf-bisimilarity is not fully abstract for contextual
equivalence, being sound but not complete. The failure of full abstraction is
compensated by the fact that CbN nf-bisimilarity is easier to establish than
applicative similarity, because of the absence of quantification over
arguments. Typically, it is easy to show that different fix-points
combinators—which are the paradigmatic terms with infinitary normal forms—are
nf-bisimilar, while it is hard to show that they are applicative bisimilar.

There exists a CbV nf-bisimilarity, Lassen’s _enf bisimilarity_
$\simeq_{\mathit{enf}}$ (2005a), which is considered the CbV nf-bisimilarity
of reference. Like Sangiorgi’s, it is sound but not complete for CbV
contextual equivalence $\simeq_{C}^{v}$. It is not an off-the-shelf adaptation
of Sangiorgi’s to CbV, as it has an _extra clause_ about evaluation contexts,
exploiting the well-known issues of Plotkin’s CbV $\lambda$-calculus with open
terms; issues that are discussed at length by Accattoli and Guerrieri (2016,
2018, 2022).

The incompleteness of both CbN and CbV nf-bisimulations for the weak
$\lambda$-calculus at first sight suggests that they are robust with respect
to the CbN/CbV switch. In fact, they are _not_. The two bisimilarities are
indeed incomplete for very different reasons.

##### Incompleteness of Enf.

Here are four important reasons why enf bisimilarity is incomplete.

  1. (1)

_Eta_ : enf bisimilarity does not validate $\eta_{v}$, the CbV variant of
$\eta$-equivalence, even if Lassen himself shows how to refine enf to correct
this aspect.

  2. (2)

_CbN duplication_ : enf bisimilarity does not equate duplications of terms
that are not _by value_ : terms such as $(\lambda x.yxx)t$ and $ytt$, are
contextually equivalent for any $t$, also for terms $t$ that are _not_ values,
while in general they are not enf bisimilar. In richer CbV settings with state
or probability, contexts discriminate more, and those terms are not
contextually equivalent, but in the pure case they are. This aspect, referred
here to as _cost-sensitiveness_ , is not necessarily a drawback, as it keeps
the program equivalence closer to CbV intuition.

  3. (3)

_Commutation of (independent) $\sf{let}$s_: in the pure case—or in the
presence of commutative effects—contextual equivalence validates the following
commutation $\equiv_{com}$ (presented with $\sf{let}$s for readability, but
easily presentable without them, expanding $\sf{let}$s as $\beta$-redexes):

${\sf let}\ x=u\ {\sf in}\ {\sf let}\ y=s\ {\sf in}\ t\ \ \equiv_{com}\ \ {\sf
let}\ y=s\ {\sf in}\ {\sf let}\ x=u\ {\sf in}\ t$ if $x\notin{\tt fv}(s)$ and
$y\notin{\tt fv}(u)$.

Enf bisimulations do not equate these terms.

  4. (4)

_$\Omega$ -terms/meaningless terms_: enf bisimilarity does not equate terms
contextually equivalent to the paradigmatic looping/meaningless $\lambda$-term
$\Omega$, referred here to as _$\Omega$ -terms_. This is connected to the
mentioned issues of Plotkin’s calculus with open terms, as they cause _false
normal forms_ , that is, $\Omega$-terms that are normal. In CbN, instead, all
$\Omega$-terms diverge.

Point 2 is acceptable, because a bisimilarity validating CbN duplication in
CbV needs to go beyond comparing the structure of normal forms, as the example
shows, thus necessarily departing from the format of nf-bisimilarities. Thus,
we shall consider cost-sensitivity as _inherent_ to CbV nf-bisimilarities,
which need not be corrected. Point 3 is specific to CbV, because in CbN
$\sf{let}$s disappear during evaluation, while in CbV with open terms they
might end up in normal forms. It is thus disappointing that commuting
$\sf{let}$s are not captured. More precisely, it would be desirable to have a
notion of nf-bisimilarity where the validation of commuting $\sf{let}$s can be
added/removed modularly, as to adapt to different CbV settings
(pure/(non-)commutative-effects). Point 4 is a stark difference between CbV
and CbN, because Sangiorgi’s bisimilarity _does equate_ the $\Omega$-terms of
weak CbN.

#####  $\Omega$-terms

The failure of enf bisimilarity with respect to $\Omega$-terms is relevant, as
all natural denotational models and program equivalences identify
$\Omega$-terms (of the modelled notion of evaluation). Roughly, different
semantics are built by distinguishing various partitions of
non-$\Omega$-terms, but they put all terms contextually equivalent to the idle
loop $\Omega$ in the same class—indeed, what would be the advantage of
partitioning them in classes? For strong CbN evaluation, in particular, the
equational identification of $\Omega$-terms is the concept around which
Barendregt’s classic book (1984) is built (therein $\Omega$-terms are called
_unsolvable terms_ , see Sect. 2).

##### Two Possible Approaches.

To overcome some of the mentioned incompleteness via a nf-bisimilarity, one
can act on two different levels: _changing the underlying calculus_ , which
provides the normal forms to compare, or _changing the nf-bisimilarity_ , that
is, the notion of comparison. For instance, Biernacki et al. (2019a) address
the problem of $\Omega$-terms (called therein _deferred diverging terms_) by
providing an alternative definition of enf bisimilarity. Commuting
$\sf{let}$s, however, do not seem to be capturable by a similar tweak of enf-
bisimilarity, as the commutation does not behave well in Plotkin’s CbV
calculus. At first sight, changing the underlying calculus is less viable, as
in general it changes the notion of contextual equivalence.

##### The Value Substitution Calculus.

The starting point of this paper is the _value substitution calculus_
(shortened to VSC), a CbV $\lambda$-calculus due to Accattoli and Paolini
(2012) and related to linear logic proof nets (Accattoli, 2015). The VSC
solves the issues of Plotkin’s calculus with open terms via an extension of
the rewriting rules, while–crucially–retaining the same notion of contextual
equivalence (Accattoli and Guerrieri, 2022). Moreover, the proof nets
inception of the calculus makes it easy to deal with the commutation of
$\sf{let}$s, which can be modularly added via a notion of _structural
equivalence_ , compatible with the rewriting rules by design. Therefore, the
VSC is a natural candidate for designing a CbV nf-bisimilarity improving on
some of the incompleteness of Lassen’s by changing the underlying calculus.

##### Net Bisimilarity.

Using the VSC, we introduce a CbV nf-bisimilarity validating the commutation
of $\sf{let}$s and identifying $\Omega$-terms. The obtained _net bisimilarity_
$\simeq_{\mathit{net}}$ and the proof of its _compatibility_ (that is, its
stability by context closure)—the challenging property to prove for
bisimilarities—are the main contributions of this paper. Compatibility implies
soundness with respect to contextual equivalence, and it is proved adapting
Lassen’s variant (1999) for nf-bisimilarities of Howe’s method. As it is often
the case for nf-bisimilarities, ours is sound but not complete. In
particular—as for enf bisimilarity—it is _cost-sensitive_.

The crafting of net bisimilarity rests on a sophisticated analysis of CbV and
the VSC. We start with the off-the-shelf adaptation of Sangiorgi’s nf-
bisimilarity to the VSC, _without Lassen’s extra clause_ , as it is unclear
how to adapt the clause to the VSC. We then refine the adaptation by comparing
normal forms modulo the (proof nets) structural equivalence of the VSC—which
includes commuting $\sf{let}$s—whence the name _net_ bisimilarity. We actually
go further, introducing a _parametric_ nf-bisimilarity, where parts of the
structural equivalences can be turned off and on at will—because some (such as
commuting $\sf{let}$s) fail in extensions of CbV with non-commutative
effects—thus defining a _family_ of CbV nf-bisimilarities, all proved
compatible via a _single abstract proof_.

Our result is however more a new beginning than the end of the story: net
bisimilarity, indeed, is _not_ a refinement of Lassen’s
$\simeq_{\mathit{enf}}$. In fact, the two are _incomparable_ , because net
bisimilarity is incomplete in yet some other ways, which are instead validated
by Lassen’s.

##### Moggi’s Laws

It is well-known that Plotkin’s CbV $\lambda$-calculus is defective, and not
just because of open terms. Plotkin himself showed the incompleteness of his
continuation-passing translation (Plotkin, 1975). To both solve the issue and
modeling extensions with effects, Moggi extended Plotkin’s calculus with
equations corresponding to laws for monads (Moggi, 1988, 1989), that are sound
for contextual equivalence. Lassen’s enf bisimulations verify these laws,
showing that it is possible to capture the laws in the notion of nf-
bisimulation rather than by changing the underlying calculus. In particular,
it is Lassen’s extra clause that allows enf to capture Moggi’s laws.

Moggi’s laws, however, are not rules of the VSC, and are not captured by net
bisimilarity. Additionally, it is unclear how to extend net bisimulations as
to satisfy Moggi’s laws. Once more, there are two options: extending the
underlying calculus (the VSC) or the nf-bisimilarity
($\simeq_{\mathit{net}}$). Both options however break properties that are
crucial for the proof that net bisimilarity is compatible. Another
disappointing fact is that the addition of $\eta_{v}$ to net bisimilarity
requires one of Moggi’s laws, so it is also unclear how to add $\eta_{v}$ to
net bisimulations.

##### Impasse and Beyond

Summing up, it seems that one cannot have the cake (a framework for nf-
bisimilarity satisfying either commuting $\sf{let}$s and $\Omega$-terms, or
Moggi’s laws and $\eta_{v}$) and eat it too (extend the framework as to
capture the missing half), or at least it is far from evident how to do it.
The exploration of such an _impasse_ is the other main contribution of the
paper. We study two further program equivalences, a naive bisimilarity
$\simeq_{nai}$ and the program equivalence $\simeq_{type}$ induced by a model,
which are sort of the intersection and the union of enf and net
bisimilarities.

##### Naive Bisimilarity $\simeq_{nai}$ = No Cake and No Eating

We consider the off-the-shelf adaptation of Sangiorgi’s CbN nf-bisimulations
to Plotkin’s CbV, obtaining _naive nf-bisimulations_ , which are strictly
weaker than both enf and net bisimulations, as they do not identify commuting
$\sf{let}$s, $\Omega$-terms, Moggi’s laws, nor $\eta_{v}$. The experiment is
instructive because we show that naive bisimulations, despite their weakness,
are enough to provide easy proofs of bisimilarity for fix-point
combinators—Lassen’s extra clause plays no role in that. Naive bisimilarity
also gives us the opportunity to gently introduce the proof technique that we
use for net bisimilarity.

##### Type Equivalence $\simeq_{type}$ = Cake and Eating, Universally

At the other end of the spectrum, we investigate the program equivalence given
by the equational theory of Ehrhard’s CbV relational model (Ehrhard, 2012). We
call it _type equivalence_ because the model is presented as a multi type
system (a variant of intersection types). Such a model was already extensively
studied in connection with the VSC by Accattoli and Guerrieri (2018, 2022).
Its equational theory does not have a presentation via nf-bisimulations, nor
any other characterization, but it is nonetheless possible to study it via the
multi type system. It turns out that type equivalence, similarly to nf-
bisimilarities, is compatible and sound, but not complete for contextual
equivalence, because it is cost-sensitive. It is not an easily usable
equivalence, as it is based on a _universal_ quantification over the typings
for a term, but it provides interesting insights.

Our results are that both enf and net bisimilarities are _included_ in type
equivalence. Therefore, the two bisimilarities are joinable. Since both are
sound, they are obviously joinable in a cost-insensitive setting, as they are
both included in contextual equivalence. Our results show that they are also
joinable in a _cost-sensitive_ program equivalence, thus suggesting that a nf-
bisimilarity joining the two might be possible. Crafting it, and especially
proving that it is compatible, is left to future work.

The following table sums up the situation.

| $\simeq_{nai}$ | $\simeq_{\mathit{enf}}$ | $\simeq_{\mathit{net}}$ | $\simeq_{type}$ | $\simeq_{C}^{v}$
---|---|---|---|---|---
Moggi’s left identity law $\mathtt{I}t\equiv_{lid}t$ ? | ✗ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$ | ✗ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$
Identification of $\Omega$-terms and commuting $\sf{let}$s? | ✗ | ✗ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$
Universal quantification in the definition? | ✗ | ✗ | ✗ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$
CbN duplication $(\lambda x.yxx)t\equiv_{dup}ytt$ ? | ✗ | ✗ | ✗ | ✗ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\checkmark}}$

##### Related Work

Beyond the already cited papers, nf-bisimilarity is studied in variants and
extensions of the $\lambda$-calculus by Lassen (1999, 2005b, 2006), Lassen and
Levy (2007, 2008), Biernacki and Lenglet (2012) and Jagadeesan et al. (2009),
and in relationship to game semantics by Levy and Staton (2014), Jaber and
Murawski (2021), and Jaber and Sangiorgi (2022). The presence of state in
(Støvring and Lassen, 2009; Biernacki et al., 2019a) makes enf-like
bisimilarities fully abstract (as it makes contextual equivalence cost-
sensitive and commutation of $\sf{let}$s invalid). Lassen’s enf bisimilarity
is studied with respect to $\eta$-equivalence by Biernacki et al. (2019b),
extensions with effects by Dal Lago and Gavazzo (2019), and the $\pi$-calculus
by Durier et al. (2022).

CbV multi types are also used by Kesner and co-authors (Bucciarelli et al.,
2020; Kesner and Peyrot, 2022; Kesner and Viso, 2022; Arrial et al., 2023) and
Díaz-Caro et al. (2013).

A notion of CbV Böhm tree, inducing a program equivalence similar to nf-
bisimilarity is proposed by Kerinec et al. (2020). Their equivalence is in
between our naive and net bisimilarities. They conjecture that it
characterizes type equivalence. Our results _refute_ such a conjecture: with
respect to the benchmarks of Sect. 5, their equivalence equates all
$\Omega$-terms but not commuting $\sf{let}$s—which are validated by net
bisimilarity—nor Moggi’s left identity law $\equiv_{lid}$.

Very recently, Koutavas et al. (2023) introduced a _complete_ CbV
bisimilarity, presented as a _nf-bisimilarity_. It is however different from
Sangiorgi’s and Lassen’s, as Koutaval et al.’s bisimilarity considers more
than the structure of normal forms, which—as already pointed out—is mandatory
to validate CbN duplication and be complete in CbV. Their definition, indeed,
is rather based on game semantics tools and environmental bisimulations.
Moreover, it addresses the different setting of CbV PCF, which is typed, and
it is not clear whether the result smoothly adapts to the untyped pure CbV
$\lambda$-calculus.

##### Proofs

Omitted proofs are in the additional material associated with this submission
on HotCRP. In case of acceptance, a version of this paper with all proofs will
be put on arXiv.org.

##  2\. Preliminaries

##### Contexts

All along the paper we use (many notions of) _contexts_ , i.e. terms with
exactly one hole, noted $\langle\cdot\rangle$. Plugging a term $t$ in a
context $C$, noted $C\langle t\rangle$, possibly captures free variables of
$t$. For instance $(\lambda x.\langle\cdot\rangle)\langle x\rangle=\lambda
x.x$, while $(\lambda x.y)\\{y{\shortleftarrow}x\\}=\lambda z.x$.

##### Preorders

We shall mostly deal with simulations, rather than bisimulations, since the
result for equivalences shall always follow by simply considering the
symmetric notions. Given a preorder/similarity $\precsim_{X}$ for some $X$, we
denote with $\simeq_{X}$ the corresponding equivalence/bisimilarity.

##### (In)Equational Theories and Compatibility

Good program preorder/equivalences are _(in)equational theories_ , that is,
they contain the reduction of the calculus and they are _compatible_ , defined
as: if $t\precsim t^{\prime}$ then $C\langle t\rangle\precsim C\langle
t^{\prime}\rangle$ for all contexts $C$, that is, that they are stable by
context closure. Reduction is usually trivially included in similarities while
compatibility is usually non-trivial to prove.

##### Contextual Equivalence

The standard of reference for program equivalences is contextual equivalence,
that can be defined abstractly as follows.

###### Definition 2.1 (Contextual Preorder and Equivalence).

Given a language of terms $\mathcal{T}$ with its associated notion of contexts
$C$ and predicate stating the termination of evaluation $\Downarrow_{e}$, we
define the associated _contextual preorder_ $\precsim_{\mathcal{C}}^{e}$ and
_contextual equivalence_ $\simeq_{\mathcal{C}}^{e}$ as follows:

  * •

$t\precsim_{\mathcal{C}}^{e}t^{\prime}$ if $C\langle
t\rangle~{}{\Downarrow_{e}}$ implies $C\langle
t^{\prime}\rangle~{}{\Downarrow_{e}}$ for all contexts $C$ such that $C\langle
t\rangle$ and $C\langle t^{\prime}\rangle$ are closed terms.

  * •

$t\simeq_{\mathcal{C}}^{e}t^{\prime}$ is the equivalence relation induced by
$\precsim_{C}$, that is, $t\simeq_{\mathcal{C}}^{e}t^{\prime}\iff
t\precsim_{\mathcal{C}}^{e}t^{\prime}$ and
$t^{\prime}\precsim_{\mathcal{C}}^{e}t$.

A relation ${\mathcal{R}}$ is sound for the contextual preorder
$\precsim_{\mathcal{C}}^{e}$ when
${\mathcal{R}}\subseteq\precsim_{\mathcal{C}}^{e}$. Soundness follows from
compatibility and _adequacy for $\Downarrow_{e}$_, defined as: if
$t~{}{\mathcal{R}}~{}t^{\prime}$ then $t\Downarrow_{e}$ implies
$t^{\prime}\Downarrow_{e}$.

###### Proposition 2.2.

Let $\precsim$ be a compatible and adequate preorder. Then
$\precsim\subseteq\precsim_{\mathcal{C}}^{e}$.

###### Proof.

Suppose $u\precsim u^{\prime}$. Let $C$ any closing context for $u$ and
$u^{\prime}$. By compatibility, $C\langle u\rangle\precsim C\langle
u^{\prime}\rangle$. By adequacy, $C\langle u\rangle\Downarrow_{e}$ implies
$C\langle u^{\prime}\rangle\Downarrow_{e}$, that is,
$u\precsim_{\mathcal{C}}^{e}u^{\prime}$. ∎

We shall see that normal form simulations are defined in such a way that they
are adequate, so that soundness follows directly from compatibility. Note that
soundness without compatibility is useless: the relation
${\mathcal{R}}\coloneqq\\{(xy,xy)\\}$ is sound but not compatible.

##### Diamond

A rewriting notion that shall play a role is the _diamond property_ , which is
the following one-step strengthening of confluence for a reduction $\to$: if
$t\to u_{1}$, $t\to u_{2}$, and $u_{1}\neq u_{2}$ then exists $s$ such that
$u_{1}\to s$ and $u_{2}\to s$. Some well-known facts: the diamond property
implies confluence but not vice-versa; if $\to$ is diamond and there is a
terminating reduction from $t$ then there are no diverging reductions from
$t$; all reductions to normal form, if any, have the same length. Roughly, the
diamond property is a relaxed form of determinism, where non-deterministic
choices have no impact on the result nor on the length of the evaluation
leading to it.

#####  $\Omega$-terms, Solvability, and Scrutability

A cornerstone of the theory of the (CbN) $\lambda$-calculus is the study of
what here we call _$\Omega$ -terms_, that is, terms that are contextually
equivalent to $\Omega$, the paradigmatic looping term. Such a notion has been
extensively studied for _head_ (CbN) contextual equivalence, for which
$\Omega$-terms are better known as _unsolvable terms_ , and often labeled as
_meaningless terms_. Actually, the definition of unsolvable term (here
omitted) is different, as it does not mention $\Omega$ nor contextual
equivalence, but equivalent to the one of $\Omega$-term. Equational theories
that identify all unsolvable terms were first studied by Wadsworth (1971,
1976) and Barendregt (1971, 1977), and it is the leading theme of Barendregt’s
book (1984). Unsolvable terms can be characterized as those terms that diverge
with respect to head reduction, as proved by Wadsworth.

Adopting _weak_ head (CbN) contextually equivalence gives a different set of
$\Omega$-terms. As for the head case, these $\Omega$-terms coincide with a
natural set of terms defined without mentioning $\Omega$, namely _(CbN)
inscrutable terms_ (for the definition see Appendix C (p. C)), first studied
by Ronchi Della Rocca and Paolini (2004) (under the name _not potentially
valuable terms_), who provide the following useful characterization, akin to
Wadsworth’s for unsolvable terms.

###### Theorem 2.3 (Diverging characterization of CbN scrutability).

A term $t$ is CbN inscrutable (thus a weak CbN $\Omega$-term) if and only if
the weak head reduction of $t$ diverges.

For instance, $\Omega$ is inscrutable but $\lambda x.\Omega$ and $x\Omega$ are
not (while $\lambda x.\Omega$ is unsolvable). From the characterization, it
follows that every inscrutable term is unsolvable, but not vice-versa.

In CbV, there are analogous notions of unsolvable and inscrutable terms, but
they lack analogous _diverging characterizations_ in Plotkin’s CbV
$\lambda$-calculus. They have been thoroughly studied by Accattoli and
Guerrieri (2022) in the VSC, where instead they admit diverging
characterizations. Surprisingly, an equational theory identifying CbV
unsolvable terms is necessarily inconsistent. The right notion of meaningless
term in CbV is actually given by CbV inscrutable terms. In Appendix C (p. C),
one can find the technical definition of CbV inscrutable terms as well as the
proof that they coincide with CbV $\Omega$-terms (relying on the VSC
introduced in Sect. 9).

In this paper, we shall not consider unsolvable terms, as we only consider
_weak_ reductions. Thus, CbN/CbV _$\Omega$ -terms_ shall always be relative to
weak CbN/CbV contextually equivalence, and coinciding with CbN/CbV inscrutable
terms.

##  3\. Background About Normal Form Bisimulations

Normal form bisimulations are program equivalences that, instead of comparing
terms _externally_ , depending on how they behave _in contexts_ , they compare
them _internally_ , by looking at the structure of their (infinitary) _normal
forms_. Let us give the simplest possible example.

Let $\rightarrow_{wh}$ be weak head reduction, also known as CbN evaluation,
which is a deterministic reduction and it is defined as $(\lambda
x.t)us_{1}\ldots s_{k}\rightarrow_{wh}t\\{x{\shortleftarrow}u\\}s_{1}\ldots
s_{k}$ with $k\geq 0$. Normal form simulations are usually based on a big-step
presentation of $\rightarrow_{wh}$: we write $t\Downarrow_{wh}\,u$ if the
$\rightarrow_{wh}$-evaluation of $t$ terminates on $u$, and
$t\not\Downarrow_{wh}\,$ otherwise. The following notion of simulation was
first considered by Sangiorgi (1994). Our presentation is slightly different
but equivalent.

###### Definition 3.1 (CbN normal form simulations, (Sangiorgi, 1994)).

A relation ${\mathcal{R}}$ is a CbN normal form simulation if
${\mathcal{R}}\subseteq\langle{\mathcal{R}}\rangle_{cbn}$, where
$t\langle{\mathcal{R}}\rangle_{cbn}t^{\prime}$ holds whenever $t,t^{\prime}$
satisfy one of the following clauses:

$\begin{array}[]{r@{\hspace{.3cm}}r@{\hspace{.3cm}}l@{\hspace{.3cm}}l@{\hspace{.3cm}}lll}\textup{(cbn
1)}\hskip 8.5359pt&\hskip 8.5359pt&\hfil\hskip
8.5359pt&t\not\Downarrow_{wh}\hfil\hskip 8.5359pt&\textit{i.e.}~{}\text{has
no}\rightarrow_{wh}\text{-normal form.}\\\ \textup{(cbn 2)}\hskip
8.5359pt&t\Downarrow_{wh}\,x\hskip 8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{wh}\,x\hfil\hskip 8.5359pt&\\\ \textup{(cbn
3)}\hskip 8.5359pt&t\Downarrow_{wh}\,\lambda x.t_{1}\hskip
8.5359pt&\text{and}\hfil\hskip 8.5359pt&t^{\prime}\Downarrow_{wh}\,\lambda
x.t^{\prime}_{1}\hfil\hskip
8.5359pt&\text{with}~{}t_{1}~{}{\mathcal{R}}~{}t^{\prime}_{1}\\\ \textup{(cbn
4)}\hskip 8.5359pt&t\Downarrow_{wh}\,n=n_{1}u\hskip
8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{wh}\,n^{\prime}=n_{1}^{\prime}u^{\prime}\hfil\hskip
8.5359pt&\text{with}~{}n_{1}~{}{\mathcal{R}}~{}n_{1}^{\prime}~{}\text{and}~{}u~{}{\mathcal{R}}~{}u^{\prime}\end{array}$

_CbN normal form similarity_ $\precsim_{cbn}$ is the largest CbN normal form
simulation, that is, it is the union of all normal form simulations. We
shorten _normal form_ as _nf_.

Nf-bisimulations and bisimilarity are the symmetric variants of simulations
and similarity, defined as expected. A simple way of proving soundness of
$\precsim_{cbn}$ is to show compatibility via the variant of Howe’s method
developed by Lassen (1999), technique that we shall recall in Sect. 7.

##### Partiality and Divergence.

Nf-simulations rely on a partial notion of evaluation (with respect to full
$\beta$-reduction), such as weak head reduction $\rightarrow_{wh}$. The key
point is that the partial reduction leaves some sub-terms not evaluated
(arguments and abstraction bodies for $\rightarrow_{wh}$). The derived
simulations compare the $\rightarrow_{wh}$-normal forms $\mathsf{nf}_{wh}(t)$
and $\mathsf{nf}_{wh}(u)$ of $t$ and $u$ by:

  * •

Checking that they have the same structure for the partially evaluated part of
the term, and

  * •

Asking that the non-evaluated sub-terms of $\mathsf{nf}_{wh}(t)$ and
$\mathsf{nf}_{wh}(u)$ in the same positions are pairwise nf-similar.

The use of a partial notion of evaluation is crucial, as it allows fine
discriminations related to divergence, which would be blurred if one would
only consider full normal forms. CbN nf-similarity, indeed, discriminates
between the following forms of divergence:

  1. (1)

Looping as $\Omega$;

  2. (2)

Looping only after having received an argument, as for $\lambda x.\Omega$;

  3. (3)

Having a looping argument, as for $x\Omega$;

  4. (4)

The finite iterations of 2 and 3, and of their combination;

  5. (5)

The _infinite_ iteration of 2 or 3, that never actually loop as $\Omega$ as
they keep producing an infinite amount of head variables and/or abstractions.
There exists terms $t$, indeed, the $\rightarrow_{wh}$ normal form of which
is, for instance, $\lambda x.u$ or $xu$ or $x\lambda y.u$, and such that $u$
has the same property. Therefore, they give rise to infinite normal forms such
as $\lambda x.\lambda x.\lambda x.\ldots$ or $x(x(x\ldots$ or $x(\lambda
y.x(\lambda y.\ldots$.

##### Open Terms.

Nf-simulations are different from most other notions of program equivalence in
that they have to deal with open terms, because, even when the terms to
compare are closed, the sub-terms on which the comparison is iterated might be
open.

##### Easier to Use.

With respect to other notions of equivalence such as applicative bisimilarity,
nf-bisimilarity is often simpler to establish, because it removes the
quantification over arguments. A typical example is the proof of the
equivalence of the Curry and Turing fix-point combinators $Y$ and $\Theta$,
which is particularly simple with CbN nf-bisimilarity, as Lassen explained in
his first article relating Böhm tree equivalence and head nf-bisimulations
(Lassen, 1999), a variant of Sangiorgi’s. We can easily adapt his argument on
head nf-bisimulations to weak head nf-bisimulations. Let $Y=\lambda
x.{\Xi\Xi}\text{, where }\Xi=\lambda z.{x({zz})}$ and $\Theta=(\lambda
z.{\lambda x.{x({zzx})}})(\lambda z.{\lambda x.{x({zzx})}})$. It is easy to
check that the following relation ${\mathcal{R}}$ is a CbN nf-(bi)simulation
relating $Y$ and $\Theta$.

$~{}{\mathcal{R}}~{}\coloneqq\\{(Y,\Theta),(\Xi\Xi,x(\Theta
x)),(x(\Xi\Xi),x(\Theta x)),(\Xi\Xi,\Theta x)\mid x\text{ a variable}\\}$

##### Equational Benchmarks

We say that a notion of program equivalence $\simeq_{X}$ _validates_ an
equivalence $\equiv_{Y}$ if $t\equiv_{Y}u$ implies $t\simeq_{X}u$. Program
equivalences in (weak/head/strong) CbN roughly can differ only along two axes:

  1. (1)

_$\eta$ -equivalence_: the amount of $\eta$ equivalence that they validate;

  2. (2)

_$\Omega$ -terms_: the amount of identifications among (variants of)
$\Omega$-terms.

Sangiorgi’s CbN nf-bisimilarity does not validate $\eta$-equivalence, because
his bisimilarity is _rigid_ , it cannot equate different normal forms such as
$x$ and $\lambda y.xy$. Since weak CbN contextual equivalence validates some
cases of $\eta$ equivalence, $\simeq_{cbn}$ is not fully abstract (Sangiorgi,
1994). More generally, nf-bisimilarities tend to not be fully abstract.
Intuitively, $t$ and $t^{\prime}$ might be externally equivalent, that is,
behave the same in all contexts, and yet be internally different, by having
different (potentially infinitary) normal forms.

About $\Omega$-terms, it follows from their diverging characterization (Thm.
2.3) that CbN nf-bisimilarity equates all CbN $\Omega$-terms, that is, it
validates the following equivalence.

  * •

_$\Omega$ -equivalence_: $t\equiv_{\Omega}u$ if $t$ and $u$ are CbN
$\Omega$-terms.

Instead, $\simeq_{cbn}$ does not equate all unsolvable terms, as it
distinguishes $\Omega$ and $\lambda x.\Omega$ (namely
$\Omega\precsim_{cbn}\lambda x.\Omega$ but $\lambda
x.\Omega\not\precsim_{cbn}\Omega$). We shall see that in CbV the reference CbV
nf-bisimulation does not equate all CbV $\Omega$-terms.

##  4\. Plotkin’s Call-by-Value and Open Terms

Here we recall Plotkin’s CbV $\lambda$-calculus, and pay attention to some
aspects that are often neglected, as they shall be relevant in the following
sections.

##### The CbV $\lambda$-Calculus.

A _value_ $v$ is a variable or an abstractions. At the rewriting level, we
consider only weak evaluation, that is, out of abstractions. We define it in
three variants, from left to right, from right to left, and in an unspecified
order, which are discussed next.

<EMAIL_ADDRESS>11.38092pt&t,u,s&\Coloneqq&v\mid tu\\\ \textsc{Values}\hskip 11.38092pt&v&\Coloneqq&x\mid\lambda x.t\par\end{array}$ | $\begin{array}[]{r@{\hspace{.4cm}}rlll}\textsc{(General) Contexts}\hskip 11.38092pt&C&\Coloneqq&\langle\cdot\rangle\mid tC\mid Ct\mid\lambda x.C\\\ \textsc{Weak Contexts}\hskip 11.38092pt&W&\Coloneqq&\langle\cdot\rangle\mid tW\mid Wt\\\ \textsc{Left Contexts}\hskip 11.38092pt&L&\Coloneqq&\langle\cdot\rangle\mid vL\mid Lt\\\ \textsc{Right Contexts}\hskip 11.38092pt&R&\Coloneqq&\langle\cdot\rangle\mid tR\mid Rv\end{array}$
---|---

###### Definition 4.1 (Reductions).

Let root ${\beta_{v}}$ reduction $\mapsto_{{\beta_{v}}}$ defined as $(\lambda
x.t)v\mapsto_{{\beta_{v}}}t\\{x{\shortleftarrow}v\\}$. Then ${\beta_{v}}$,
weak, left (to right), and right (to left) reduction, noted
$\rightarrow_{{\beta_{v}}}$, $\rightarrow_{w}$, $\rightarrow_{l}$, and
$\rightarrow_{r}$, are defined as follows: if $t\mapsto_{{\beta_{v}}}u$ then

$\begin{array}[]{c@{\hspace{1cm}}c@{\hspace{1cm}}c@{\hspace{1cm}}c}C\langle
t\rangle\rightarrow_{{\beta_{v}}}C\langle u\rangle\hfil\hskip
28.45274pt&W\langle t\rangle\rightarrow_{w}W\langle u\rangle\hfil\hskip
28.45274pt&L\langle t\rangle\rightarrow_{l}L\langle u\rangle\hfil\hskip
28.45274pt&R\langle t\rangle\rightarrow_{r}R\langle u\rangle\end{array}$

It is standard that $\rightarrow_{l}$ and $\rightarrow_{r}$ are deterministic
and contained in $\rightarrow_{w}$, which is non-deterministic but diamond,
while $\rightarrow_{{\beta_{v}}}$ is non-deterministic and confluent but not
diamond.

##### Closed Terms.

If terms are closed and evaluation is weak, which are a standard assumption in
the study of functional languages, then call-by-value evaluation has some very
nice properties, summed up by the next proposition.

###### Proposition 4.2.

Let $t$ be a closed term.

  1. (1)

$t$ is a weak/left/right normal form if and only if $t$ is an abstraction.

  2. (2)

On $t$, left and right reduction are full with respect to weak evaluation,
that is, if $t\rightarrow_{w}u$ then there exist $s$ and $r$ such that
$t\rightarrow_{l}s$ and $t\rightarrow_{r}r$.

Intuitively, left and right reduction are two equivalent ways of turning weak
reduction into a deterministic reduction, on closed terms. In CbV, contextual
preorder $\precsim_{C}^{v}$ is defined with respect to evaluation to a value,
which can be equivalently expressed as termination of weak, left, or right
reduction. Importantly, for $\precsim_{C}^{v}$ one considers only the
reduction of closed terms, as the definition of $\precsim_{C}^{v}$ is based on
contexts closing the terms to compare.

##### Open Terms, Stuck Redexes, and The Inequivalence of the Three
Strategies.

As soon as one considers open terms, the good properties of the system break.
The only ones which survive are the diamond property of weak reduction and the
fact that left and right reduction are deterministic. But weak normal forms
now have a complex shape, as there can be _stuck redexes_ such as $(\lambda
x.t)(yy)$ which cannot be reduced because their argument is normal and not a
value.

Stuck redexes unfortunately break the equivalence of left, right, and weak
reduction: left, right, and weak normal forms are all different notions,
because left and right reduction are no longer full with respect to weak
reduction. For instance, $t\coloneqq xx(\mathtt{I}\mathtt{I})$ is a left
normal form which is not a weak/right normal form, because
$t\rightarrow_{w}xx\mathtt{I}$, which is weak/right normal. Similarly,
$\mathtt{I}\mathtt{I}(xx)$ is a right normal form which is not left/weak
normal, and $xx(\mathtt{I}\mathtt{I})(xx)$ is a left/right normal form which
is not weak normal. Perhaps more worrying is the fact that stuck redexes
introduce suspicious distinctions between contextually equivalent terms:
$\Omega$ and $\Omega^{L}\coloneqq(\lambda x.\delta)(yz)\delta$ are
contextually equivalent, but the first one diverges while the second one is
normal, because of the stuck redex.

##  5\. Equational Benchmarks for CbV Program Equivalences

In CbN, there are only two ’equational benchmarks’, or degrees of freedom, for
program equivalences, namely $\eta$-equivalence and the $\Omega$-equivalence
$\equiv_{\Omega}$. In CbV, the situation is richer, there are various
equivalences that can be validated or not. Here we list the most relevant
ones. We start by discussing the CbV variants of $\eta$-equivalence and
$\Omega$-equivalence, and then present the equivalences that are found in
known extensions of Plotkin’s calculus.

For all the equivalences, we simply give the root axioms defining them,
assuming that they are closed by all contexts. All the given equivalences (but
CbN erasure) are validated by CbV contextual equivalence $\simeq_{C}^{v}$. The
meaning of some of the equivalences from extended CbV calculi might seem
obscure. They shall make more sense after the introduction of explicit
substitutions in Sect. 9.

In CbV, $\eta$-equivalence has to be restricted, otherwise it turns non-values
into values. At first sight, the by value version of $\eta$ seems to be
$v\equiv_{\eta_{v}}\lambda x.{vx}$ if $x\notin{\tt fv}(v)$. But since any CbV
program equivalence validates ${\beta_{v}}$-reduction, the case $v=\lambda
y.t$ is actually caught by ${\beta_{v}}$-reduction (because $\lambda
x.(\lambda y.t)x\rightarrow_{{\beta_{v}}}\lambda
x.t\\{y{\shortleftarrow}x\\}=_{\alpha}\lambda y.t$), so that
$\equiv_{\eta_{v}}$ simply amounts to the variable case.

  * •

_$\eta_{v}$ equivalence_: $y\equiv_{\eta_{v}}\lambda x.{yx}$ for every
variable $y$.

##### CbV $\Omega$-terms

$\Omega$-terms adapt to CbV by simply considering CbV contextual equivalence.
The equivalence to be validated here is the following one:

  * •

_$\Omega$ -equivalence by value_: $t\equiv_{\Omega_{v}}u$ if $t$ and $u$ are
CbV $\Omega$-terms.

In Plotkin’s calculus, CbV $\Omega$-terms cannot have a diverging
characterization akin to that of CbN $\Omega$-terms (Thm. 2.3)—they shall have
one in the VSC. For instance, an $\Omega$-term such as
$\Omega^{L}\coloneqq(\lambda x.\delta)(yz)\delta$ is normal for Plotkin, while
it should diverge if a good characterization existed.

The equivalence $\equiv_{\Omega_{v}}$ has a special role among those listed
here because whether a term is an $\Omega$-term is _undecidable_ , so that the
equivalence cannot be seen as computational principle to be tested via a
rewriting rule. It is then all the more relevant that a program equivalence
validates it.

##### Moggi

We now turn to equivalences found in extensions of Plotkin’s calculus. The
equivalences enriching ${\beta_{v}}$-conversion in Moggi’s untyped
computational $\lambda$-calculus are the following ones, here reformulated
without $\sf{let}$-expressions:

  * •

_Left identity_ : $\mathtt{I}t\equiv_{lid}t$, where $\mathtt{I}=\lambda x.x$
is the identity combinator;

  * •

_Associativity of lets_ : $(\lambda x.t)((\lambda y.u)s)\equiv_{ass}(\lambda
y.(\lambda x.t)u)s)$ if $y\not\in{\tt fv}(t)$;

  * •

_Left decomposition of applications_ : $tu\equiv_{lad}(\lambda x.xu)t$ if
$x\not\in{\tt fv}(u)$;

  * •

_Right decomposition of applications_ : $vt\equiv_{rad}(\lambda x.vx)t$ if
$x\not\in{\tt fv}(v)$. This one exists also in an extended form:
$ut\equiv_{exrad}(\lambda x.ux)t$ if $x\not\in{\tt fv}(u)$

Of them, the most interesting one for our study is $\equiv_{lid}$, which in
Plotkin’s calculus holds only for values, as for values it is an instance of
${\beta_{v}}$-conversion, while in Moggi’s it holds for every term $t$.

##### Proof Nets

The CbV translation of $\lambda$-calculus in linear logic proof nets, studied
in detail by Accattoli (2015), equates various pairs of terms. The induced
equivalences are better expressed with explicit subsitution, as we shall see
in Sect. 10, but we anticipate them here anyway. They subsume Moggi’s
$\equiv_{ass}$ rule and other presentations of proof nets equivalences such as
the $\sigma$-rules of the shuffling calculus of Carraro and Guerrieri (2014).
Moreover, they include the following equivalences.

  * •

Left (Applied-$\lambda$) Application: $(\lambda x.t)us\equiv_{@l}(\lambda
x.ts)u$ if $x\not\in{\tt fv}(s)$;

  * •

Right (Applied-$\lambda$) Application: $t((\lambda y.u)s)\equiv_{@r}(\lambda
y.tu)s$ if $y\not\in{\tt fv}(t)$;

  * •

Commutativity: $(\lambda y.(\lambda x.t)u)s\equiv_{com}(\lambda x.(\lambda
y.t)s)u$ if $x\notin{\tt fv}(s)$ and $y\notin{\tt fv}(u)$.

The first two rules correspond to possible commutations between applications
and applied lambdas–which shall correspond to commutations between
applications and $\sf{let}$s in Sect. 10. The second one also can be seen as a
generalization of Moggi’s $\equiv_{ass}$ replacing the value $\lambda x.t$
with whatever term $t$. Commutativity swaps adjacent and unrelated redexes,
and it is the equivalence that in the introduction is formulated with
$\sf{let}$s. It is a special equivalence, for at least two reasons.

  1. (1)

_Effects_ : commutativity holds in the pure CbV setting but it often fails in
extensions of CbV with effects, because many effects are order-dependent
(think of the order of writes on a memory cell). Therefore, it is an
equivalence that one might want to be able to modularly add or remove from a
notion of bisimilarity, rather than always validate it.

  2. (2)

_Unorientable_ : being symmetric, commutativity cannot be oriented as a
rewriting rule. Therefore, any nf-bisimulation validating it needs to be able
to compare normal forms up to some deformation of terms.

The reason why some equivalences at times appear in restricted forms is also
related to effects. With non-commutative effects one has to fix a
deterministic evaluation strategy, typically left-to-right, and this
constrains the shape of equivalences forcing a sub-term to be a value $v$
(resp. $\lambda x.t$), as in $\equiv_{rad}$ (resp. $\equiv_{ass}$). Similarly
for proof nets equivalence, evaluating left-to-right would lead us to a
restricted version of $\equiv_{@r}$ where the sub-term $t$ has to be a value.
Proceeding right-to-left would relax them but force other dual constraints
(such as $t$ being a value in $\equiv_{lad}$), and adopting a non-specified
order induces the extended versions of Moggi’s laws and the unrestricted
version of the proof nets equivalences.

##### CbN Duplication and CbN Erasure

The last equivalences that we consider are CbN duplication and CbN erasure. We
do not actually know how to characterize CbN duplication independently of
erasure with an axiom, or a set of axioms, but we discuss a specific case, to
illustrate the idea.

  * •

_CbN Duplication_ : $(\lambda x.yxx)u\equiv_{dup}yuu$;

  * •

_CbN Erasure_ : $(\lambda x.t)u\equiv_{era}t$ with $x\notin{\tt fv}(t)$.

In CbV, duplication and erasure are included in ${\beta_{v}}$-conversion if
$u$ is a value, but not otherwise. For arbitrary terms, erasure is unsound in
CbV, because erasing a sub-term might turn divergence into termination: for
instance $t\coloneqq(\lambda x.z)(yy)$ is not contextually equivalent to
$u\coloneqq z$ in CbV, because $C\langle t\rangle$ diverges while $C\langle
u\rangle$ terminates with respect to the context $C\coloneqq(\lambda
y.\langle\cdot\rangle)\delta$.

Duplication, instead, is sound for arbitrary terms, the idea being that
terminating (resp. diverging) once, or terminating (resp. diverging) twice
does not affect termination (resp. divergence). It is however a principle
somewhat clashing with the nature of CbV. The cornerstone of CbV is the idea
that one should reduce arguments _before_ substituting them, and CbN
duplication does exactly the opposite. Intuitively, a CbV program equivalence
validating CbN duplication is _qualitative_ or _cost-insensitive_ , as it only
observes termination, while one rejecting it is somehow _cost-sensitive_ , as
it distinguishes between differently efficient ways of realizing the same
qualitative behavior.

##### Summing Up

Of all the discussed equivalences, the most relevant ones for our study are
the $\Omega$-equivalence $\equiv_{\Omega_{v}}$ and left identity
$\equiv_{lid}$. Commutativity $\equiv_{com}$ shall also be a source of
inspiration for the modular _mirror_ approach of Sect. 11. CbN Duplication is
validated by CbV contextual equivalence while none of the program equivalences
studied in this paper validates it. This fact shows that they may be sound but
are _not complete_ with respect to contextual equivalence.

##  6\. Naive CbV Bisimilarity

If one takes Sangiorgi’s CbN nf-similarity $\precsim_{cbn}$ (Definition 3.1)
and simply replaces weak head reduction with one of the weak CbV reductions
(weak, left, or right) then one obtains notions of CbV nf-similarity.

We define the similarity induced by weak reduction. Left or right reductions
induce different similarities but with the same pros and cons that are
discussed below. Let $\Downarrow_{w}\,$ and $\not\Downarrow_{w}\,$ be big-step
termination and divergence with respect to weak CbV reduction
$\rightarrow_{w}$.

###### Definition 6.1 (Naive nf-bisimulation for Call-by-Value).

A relation ${\mathcal{R}}$ is a _naive (CbV) nf-simulation_ if
${\mathcal{R}}\subseteq\langle{\mathcal{R}}\rangle_{nai}$, where
$t\langle{\mathcal{R}}\rangle_{nai}t^{\prime}$ holds whenever $t,t^{\prime}$
satisfy one of the following clauses:

$\begin{array}[]{r@{\hspace{.3cm}}r@{\hspace{.3cm}}l@{\hspace{.3cm}}l@{\hspace{.3cm}}lll}\textup{(nai
1)}\hskip 8.5359pt&\hskip 8.5359pt&\hfil\hskip
8.5359pt&t\not\Downarrow_{w}\hfil\hskip 8.5359pt&\textit{i.e.}~{}\text{has
no}\rightarrow_{w}\text{-normal form.}\\\ \textup{(nai 2)}\hskip
8.5359pt&t\Downarrow_{w}\,x\hskip 8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{w}\,x\hfil\hskip 8.5359pt&\\\ \textup{(nai
3)}\hskip 8.5359pt&t\Downarrow_{w}\,\lambda x.t_{1}\hskip
8.5359pt&\text{and}\hfil\hskip 8.5359pt&t^{\prime}\Downarrow_{w}\,\lambda
x.t^{\prime}_{1}\hfil\hskip
8.5359pt&\text{with}~{}t_{1}~{}{\mathcal{R}}~{}t^{\prime}_{1}\\\ \textup{(nai
4)}\hskip 8.5359pt&t\Downarrow_{w}\,n=n_{1}n_{2}\hskip
8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{w}\,n^{\prime}=n_{1}^{\prime}n_{2}^{\prime}\hfil\hskip
8.5359pt&\text{with}~{}n_{1}~{}{\mathcal{R}}~{}n_{1}^{\prime}~{}\text{and}~{}n_{2}~{}{\mathcal{R}}~{}n_{2}^{\prime}\end{array}$

_Naive nf-similarity_ $\precsim_{nai}$ is the largest naive nf-simulation.

Naive (bi)similarity seems defined very naturally, and yet it does not
validate _any_ of the equivalences of the previous section. Let’s discuss
$\equiv_{\Omega_{v}}$ and $\equiv_{lid}$.

  1. (1)

_$\Omega$ -equivalence_: $\equiv_{\Omega_{v}}$ is not validated by
$\precsim_{nai}$, and $\Omega$-terms are not minimal for $\precsim_{nai}$, in
contrast with the fact that CbN $\Omega$-terms are minimal for Sangiorgi’s
similarity $\precsim_{cbn}$. For instance, $\Omega$ is
$\precsim_{nai}$-minimal, but $\Omega^{L}$ is an $\Omega$-term and one has
$\Omega\precsim_{nai}\Omega^{L}$, because $\Omega\not\Downarrow_{w}\,$, but
not $\Omega^{L}\not\precsim_{nai}\Omega$, because $\Omega^{L}$ is
$\rightarrow_{w}$-normal.

  2. (2)

_Left identity_ : the equivalence $\equiv_{lid}$ is not validated by
$\precsim_{nai}$. In Plotkin’s calculus $\mathtt{I}(xt)$ does not reduce to
$xt$, because $xt$ is not a value—more generally this happens for all normal
open terms that are not values. Therefore, $\mathtt{I}(xt)$ and $xt$ are
$\precsim_{nai}$-incomparable.

#####  $\beta_{v}$-Conversion

From the definition of $\precsim_{nai}$, it immediately follows that naive
bisimilarity contains the $\mapsto_{{\beta_{v}}}$ root rule, that is, that if
$t\mapsto_{{\beta_{v}}}u$ then $t\simeq_{nai}u$, simply because $t$ and $u$
have the same left normal form. Since $\simeq_{nai}$ is a compatible
equivalence relation, it turns out that $\simeq_{nai}$ contains the whole of
${\beta_{v}}$-conversion $=_{{\beta_{v}}}$.

###### Proposition 6.2 (${\beta_{v}}$-conversion is validated by naive
bisimilarity).

If $t=_{{\beta_{v}}}u$ then $t\simeq_{nai}u$.

##### Naive Similarity and Fix-Points

Despite its naivety, it is possible to prove that the usual CbV variants of
Curry’s and Turing’s fix-point combinators $Y_{v}$ and $\Theta_{v}$ are
naively similar, as we now show.

$\begin{array}[]{c\colspace|\colspace c}\textsc{Curry's fix-
point}&\textsc{Turing's fix-point}\\\ Y_{v}\coloneqq\lambda
x.{\Xi_{v}\Xi_{v}}\text{, where }\Xi_{v}=\lambda z.{x\lambda
y.{zzy}}&\Theta_{v}\coloneqq(\lambda z.{\lambda x.{x\lambda
y.{zzxy}}})(\lambda z.{\lambda x.{x\lambda y.{zzxy}}})\end{array}$

Let’s build a naive (bi)simulation ${\mathcal{R}}$ relating $Y_{v}$ and
$\Theta_{v}$. The relation ${\mathcal{R}}$ must contain the pair
$(Y_{v},\Theta_{v})$. Both terms $\rightarrow_{w}$-evaluate to an abstraction
($\Theta_{v}\to\lambda x.{x\lambda y.{\Theta_{v}xy}}$). Hence their weak
normal forms are (abstractions) $\lambda x.{\Xi_{v}\Xi_{v}}$ and $\lambda
x.{x\lambda y.{\Theta_{v}xy}}$ which must satisfy the third clause for
$\precsim_{nai}$, that is, their bodies under the abstraction
$(\Xi_{v}\Xi_{v},x\lambda y.{\Theta_{v}xy})$ must appear in ${\mathcal{R}}$.
Since $\Xi_{v}\Xi_{v}\rightarrow_{w}x\lambda y.{\Xi_{v}\Xi_{v}y}$,
${\mathcal{R}}$ must contain the fourth clause requirements, that is,
$x~{}{\mathcal{R}}~{}x$ and $\lambda
y.{\Xi_{v}\Xi_{v}y}~{}{\mathcal{R}}~{}\lambda y.{\Theta_{v}xy}$. As a result,
$x~{}{\mathcal{R}}~{}x$ needs to be added to the simulation (for all possible
choice of variables when opening the abstraction at the first step), and we
continue on adding $(\lambda y.{\Xi_{v}\Xi_{v}y},\lambda y.{\Theta_{v}xy})$ to
${\mathcal{R}}$, then adding any pair of terms needed so that
${\mathcal{R}}\subseteq\langle{\mathcal{R}}\rangle_{nai}$. By repeating this
process, we eventually fall back to $x\lambda
y.{\Xi_{v}\Xi_{v}y}~{}{\mathcal{R}}~{}x\lambda y.{\Theta_{v}xy}$ which is
already in the built relation ${\mathcal{R}}$, which means it now satisfies
${\mathcal{R}}\subseteq\langle{\mathcal{R}}\rangle_{nai}$, that is,
${\mathcal{R}}$ is a naive simulation. Since similarly the symmetric relation
$sym({\mathcal{R}})$ also satisfies $sym({\mathcal{R}})\subseteq\langle
sym({\mathcal{R}})\rangle_{nai}$, ${\mathcal{R}}$ is actually a naive _bi_
simulation.

The full relation proving the next proposition is:

${\mathcal{R}}\coloneqq\\{(x,x)\mid x\text{ a
variable}\\}~{}\cup~{}\\{~{}~{}(Y_{v},\Theta_{v}),(\lambda
x.\Xi_{v}\Xi_{v},\lambda x.{x\lambda y.{\Theta_{v}xy}}),\\}~{}~{}\cup$

$\\{(\Xi_{v}\Xi_{v},{x\lambda y.{\Theta_{v}xy}}),~{}~{}(x\lambda
y.{\Xi_{v}\Xi_{v}y},{x\lambda y.{\Theta_{v}xy}}),~{}~{}(\lambda
y.{\Xi_{v}\Xi_{v}y},\lambda y.{\Theta_{v}xy})\mid x\text{ a
variable}\\}~{}~{}\cup$

$\\{({\Xi_{v}\Xi_{v}y},{\Theta_{v}xy}),((x\lambda
y^{\prime}.{\Xi_{v}\Xi_{v}y^{\prime}})y,({x\lambda
y^{\prime}.{\Theta_{v}xy^{\prime}}})y)\mid x\text{ and }y\text{ variables}\\}$

###### Proposition 6.3.

$Y_{v}\simeq_{nai}\Theta_{v}$, that is, Curry’s and Turing’s fix-points are
naive bisimilar.

##  7\. Compatibility and Lassen’s method for naive bisimilarity

In this section, we prove compatibility for the naive bisimilarity introduced
in the previous section. The aim is to provide a gentle introduction to
Lassen’s variant (1999) of Howe’s method (Howe, 1996; Pitts, 2012) for proving
the compatibility of similarities, and to delay some of the technicalities
that we shall need to address for the similarity we are really interested in.

We prove compatibility for weak naive similarity, but the proof technique
easily adapts to left and right naive similarity.

##### From Small-Step to Big-Step.

Nf-similarities look at normal forms, and the crucial proof in Howe’s method
proceeds by induction on a big-step formulation of evaluation, where _big-
step_ means that it relates a terminating term directly with its normal form,
hiding the intermediate steps. Therefore, we need to reformulate the small-
step reduction $t\rightarrow_{w}^{k}n$ where $n$ is $\rightarrow_{w}$-normal,
in a big-step manner as $t\Downarrow_{{w}}\,n$.

For the technical development, we need to keep the information about the
number $k$ of small steps, that is, we shall rather write
$t\Downarrow_{{w}}^{k}n$. Such a quantitative information is needed both to
prove the equivalence with small-step evaluation and for the crucial proof in
the method.

###### Definition 7.1 (Big-step weak evaluation $\Downarrow_{{w}}\,$).

The big-step weak evaluation predicate $t\Downarrow_{{w}}^{k}n$, read _$t$
(weak)-converges in $k$ steps to a normal form $n$_, is defined as follows.

| $v\Downarrow_{{w}}^{0}v$ | $tu\Downarrow_{{w}}^{k+h+i+1}n\lx@proof@logical@and t\Downarrow_{{w}}^{k}\lambda x.su\Downarrow_{{w}}^{h}v{s\\{x{\shortleftarrow}v\\}}\Downarrow_{{w}}^{i}n$ | $tu\Downarrow_{{w}}^{k+h}n_{1}=nn^{\prime}\lx@proof@logical@and t\Downarrow_{{w}}^{k}nu\Downarrow_{{w}}^{h}n^{\prime}$
---|---|---

Notation: $t\Downarrow_{{w}}\,n$ abbreviates _there exists a $k$ such that
$t\Downarrow_{{w}}^{k}n$_.

###### Proposition 7.2 (Equivalence of small-step and big-step in weak).

$t\Downarrow_{{w}}^{k}n$ if and only if $t\rightarrow_{w}^{k}n$ with $n$
normal.

Let us stress an important point. We recall that $\rightarrow_{w}$ is non-
deterministic but diamond. The diamond property is here crucial, in order to
make sense—at the big-step level—of the number of steps $k$, which for a
diamond reduction does not depend on the reduction path to normal form.

##### (Howe-)Lassen’s Method

Proving that a behavioral preorder $\precsim$ is compatible often cannot be
done directly, that is, just by induction on the contextual closure. The idea
of Howe’s method is that, instead of proving compatibility of $\precsim$, one
introduces a derived preorder ${\precsim}^{\mathcal{H}}$ where the compatible
closure is enforced in the definition, and then proves that $\precsim$ and
${\precsim}^{\mathcal{H}}$ coincide. Howe introduced his method (1996) to deal
with _applicative_ similarities, Lassen adapted it (1999) for _normal form_
similarities. The general idea is the same, but Lassen considers a different
closure operation ${\precsim}^{\mathcal{L}}$.

##### Lassen’s Closure.

The difficulty in proving directly that a similarity $\precsim$ is compatible
comes from the applicative contextual closure, which may introduce a
$\beta$-redex (when applying an abstraction to a term), that in turn can
substitute over $\precsim$-related terms. The idea is to define the preorder
${\precsim}^{\mathcal{L}}$ as the compatible, substitutive, and reflexive
closure of $\precsim$.

###### Definition 7.3 (Lassen closure).

The _Lassen closure_ ${{\mathcal{R}}}^{\mathcal{L}}$ of a relation
${\mathcal{R}}$ on terms is given by:

| $a\,{{\mathcal{R}}}^{\mathcal{L}}\,ba~{}{\mathcal{R}}~{}b$ | $x\,{{\mathcal{R}}}^{\mathcal{L}}\,x$ | $\lambda x.a\,{{\mathcal{R}}}^{\mathcal{L}}\,\lambda x.ba\,{{\mathcal{R}}}^{\mathcal{L}}\,b$
---|---|---
| $ap\,{{\mathcal{R}}}^{\mathcal{L}}\,bq\lx@proof@logical@and a\,{{\mathcal{R}}}^{\mathcal{L}}\,bp\,{{\mathcal{R}}}^{\mathcal{L}}\,q$ | $a\\{x{\shortleftarrow}v\\}\,{{\mathcal{R}}}^{\mathcal{L}}\,b\\{x{\shortleftarrow}v^{\prime}\\}{}\lx@proof@logical@and a\,{{\mathcal{R}}}^{\mathcal{L}}\,bv\,{{\mathcal{R}}}^{\mathcal{L}}\,v^{\prime}$
---|---

Note rule (${\mathcal{L}}_{\textsc{sub}}$): only values can be substituted, as
this is Call-by-Value’s mantra.

##### Lassen’s Closure Preserves Simulations

The proof of equivalence of $\precsim_{nai}$ and
${\precsim_{nai}}^{\mathcal{L}}$ reduces to proving that the closure operator
${\cdot}^{\mathcal{L}}$ preserves $\precsim_{nai}$ simulations, that is, that
${{\mathcal{R}}}^{\mathcal{L}}$ is a naive simulation if ${\mathcal{R}}$ is—it
is often referred to as the _main lemma_ of the method. The proof is delicate
and rests on two key intermediate properties. The first one concerns the
evaluation level, and, when expressed at the big-step level, it is a sort of
factorization property with respect to meta-level substitutions. In fact, it
is nothing else but the substitutivity of small-step evaluation, rephrased at
the big-step level.

###### Proposition 7.4 (Small-step substitutivity).

If $t\rightarrow_{w}t^{\prime}$ then
$t\\{x{\shortleftarrow}v\\}\rightarrow_{w}t^{\prime}\\{x{\shortleftarrow}v\\}$

###### Proof.

By induction on $t\rightarrow_{w}t^{\prime}$ (induction on contexts). ∎

###### Lemma 7.5 (Big-step substitutivity).

If $t\\{x{\shortleftarrow}v\\}\Downarrow_{{w}}^{k}n$ then there exist
$k^{\prime}$ and $n^{\prime}$ such that
$t\Downarrow_{{w}}^{k^{\prime}}n^{\prime}$ and
$n^{\prime}\\{x{\shortleftarrow}v\\}\Downarrow_{{w}}^{k-k^{\prime}}n$.

###### Proof.

If $t\\{x{\shortleftarrow}v\\}\Downarrow_{{w}}^{k}n$, then
$t\Downarrow_{{w}}\,n^{\prime}$ because if $t$ diverges then
$t\\{x{\shortleftarrow}v\\}$ diverges as well by substitutivity of
$\rightarrow_{w}$ (Lemma 7.4). Then there exists $k^{\prime}$ such that
$t\Downarrow_{{w}}^{k^{\prime}}n^{\prime}$. Note that by substitutivity we
have
$t\\{x{\shortleftarrow}v\\}\rightarrow_{w}^{k^{\prime}}n^{\prime}\\{x{\shortleftarrow}v\\}$,
and so $n^{\prime}\\{x{\shortleftarrow}v\\}\Downarrow_{{w}}^{k-k^{\prime}}n$
because the reduction is diamond, hence all normalizing reduction sequences
have the same length. ∎

The second key intermediate property is the coherence of naive simulations
with respect to reduction and substitution.

###### Proposition 7.6 (Coherence of simulation, reduction, and substitution).

Let $~{}{\mathcal{R}}~{}$ be a naive simulation,
$n\,\langle{{\mathcal{R}}}^{\mathcal{L}}\rangle_{nai}\,n^{\prime}$, and
$v\,\langle{{\mathcal{R}}}^{\mathcal{L}}\rangle_{nai}\,v^{\prime}$.

  1. (1)

_Normal forms_ : if $n\\{x{\shortleftarrow}v\\}$ is $\rightarrow_{w}$-normal
then $n^{\prime}\\{x{\shortleftarrow}v^{\prime}\\}$ is
$\rightarrow_{w}$-normal and
$n\\{x{\shortleftarrow}v\\}\,\langle{{\mathcal{R}}}^{\mathcal{L}}\rangle_{nai}\,n^{\prime}\\{x{\shortleftarrow}v^{\prime}\\}$.

  2. (2)

_Steps_ : if $n\\{x{\shortleftarrow}v\\}\rightarrow_{w}t$ then
$n^{\prime}\\{x{\shortleftarrow}v^{\prime}\\}\rightarrow_{w}u$ and
$t\,{{\mathcal{R}}}^{\mathcal{L}}\,u$.

Note that the second point has $\,{{\mathcal{R}}}^{\mathcal{L}}\,$ rather than
$\,\langle{{\mathcal{R}}}^{\mathcal{L}}\rangle_{nai}\,$ in the conclusion.
This is because in general $t$ and $u$ are not normal. In the proof of the
next proposition, it is shown that the normal forms of $t$ and $u$ are in fact
$\,\langle{{\mathcal{R}}}^{\mathcal{L}}\rangle_{nai}\,$-related.

We can now prove the crucial property of Lassen’s closure.

###### Proposition 7.7.

Let ${\mathcal{R}}$ be a naive simulation.

  1. (1)

_Technical auxiliary statement_ : if $a\,{{\mathcal{R}}}^{\mathcal{L}}\,b$ and
$a\Downarrow_{{w}}^{k}n$ then $b\Downarrow_{{w}}\,n^{\prime}$ and
$n\,\langle{{\mathcal{R}}}^{\mathcal{L}}\rangle_{nai}\,n^{\prime}$.

  2. (2)

_Lassen’s closure preserves naive simulations_ :
${{\mathcal{R}}}^{\mathcal{L}}$ is a naive simulation.

###### Proof.

  1. (1)

_Sketch_ (complete proof in Appendix A of the additional material on HotCRP):
by induction on $(k,d)$ where $d$ is the size of the derivation of
$a\,{{\mathcal{R}}}^{\mathcal{L}}\,b$. We proceed by case analysis on the last
rule of the derivation $a\,{{\mathcal{R}}}^{\mathcal{L}}\,b$. Cases
(${\mathcal{L}}_{\textsc{lift}}$), (${\mathcal{L}}_{\textsc{var}}$), and
(${\mathcal{L}}_{\lambda}$) are immediate by definition. Case
(${\mathcal{L}}_{@}$) relies on a second case analysis (on the last rule of
the $a\Downarrow_{{w}}^{k}n$ derivation). The sub-cases are routine and may
depend on the (${\mathcal{L}}_{\textsc{sub}}$) rule. Case
(${\mathcal{L}}_{\textsc{sub}}$) is the core of the proof. It starts by
applying big-step substitutivity (Lemma 7.5) to $a=t\\{x{\shortleftarrow}v\\}$
and then, depending on whether the obtained
$n^{\prime}\\{x{\shortleftarrow}v\\}$ is normal, it applies the corresponding
coherence property of naive simulations with respect to evaluation (Prop.
7.6).

  2. (2)

Unfolding the statement one obtains exactly the statement of point 1.∎

Finally, we can use the preservation property to prove the redundancy of the
closure, from which the compatibility and the soundness of naive similarity
follows.

###### Theorem 7.8 (Compatibility and soundness of $\precsim_{nai}$).

  1. (1)

_Redundancy of Lassen’s closure_ :
$\precsim_{nai}\,={\precsim_{nai}}^{\mathcal{L}}$.

  2. (2)

Naive similarity is compatible and included in the CbV contextual preorder
$\precsim_{C}^{v}$.

###### Proof.

  1. (1)

By construction of ${\langle\cdot\rangle}^{\mathcal{L}}$,
$\precsim_{nai}\subseteq{\precsim_{nai}}^{\mathcal{L}}$ (by rule
${\mathcal{L}}_{\textsc{lift}}$). Preservation of naive simulations by
Lassen’s closure (Prop. 7.7) and the fact that $\precsim_{nai}$ is a naive
simulation give that ${\precsim_{nai}}^{\mathcal{L}}$ is a naive simulation.
By definition, $\precsim_{nai}$ is the maximal naive simulation hence
${\precsim_{nai}}^{\mathcal{L}}\subseteq\precsim_{nai}$.

  2. (2)

Compatibility follows from point 1, because ${\precsim_{nai}}^{\mathcal{L}}$
is compatible by definition. Inclusion in $\simeq_{C}^{v}$ follows by Prop.
2.2 and by adequacy of $\precsim_{nai}$, which is trivial.∎

##  8\. Lassen’s Eager Normal Form Simulation

The CbV nf-simulation of reference in the literature is due to Lassen (Lassen,
2005a). Lassen’s simulation is interesting because it is not defined by simply
changing the notion of reduction in Sangiorgi’s. Lassen indeed exploits stuck
redexes in open terms, and defines a simulation that _unstucks_ them, a
mechanism which we shall refer to as _stop-and-go_.

##### Grammar of Left Normal Forms

Lassen’s similarity is built using _left reduction_ $\rightarrow_{l}$. The
starting point is the observation that, despite the limits of left reduction,
it admits a description of its normal forms via left contexts which is
extremely simple and elegant.

###### Lemma 8.1 (Unique decomposition, (Lassen, 2005a)).

Any (possibly open) term is either a value or admits a unique decomposition
$L\langle vv^{\prime}\rangle$. In particular, left normal forms can be
described as follows:

<EMAIL_ADDRESS>normal forms}\hfil\hskip
14.22636pt&n,n^{\prime}&\Coloneqq&v\mid L\langle xv\rangle\end{array}$

The simple structure of left normal forms is then used by Lassen to define
eager nf-simulation. The crucial clause is the fourth one, which realizes the
stop-and-go mechanism. _Notation_ : let $\Downarrow_{l}\,$ and
$\not\Downarrow_{l}\,$ be big-step termination and divergence with respect to
left CbV reduction $\rightarrow_{l}$.

###### Definition 8.2 ($\mathsf{Enf}$ simulation, (Lassen, 2005a)).

A relation ${\mathcal{R}}$ is an _eager normal form ( $\mathsf{enf}$)
simulation_ if
${\mathcal{R}}\subseteq\langle{\mathcal{R}}\rangle_{\mathit{enf}}$, where
$t\langle{\mathcal{R}}\rangle_{\mathit{enf}}t^{\prime}$ holds whenever
$t,t^{\prime}$ satisfy one of the following clauses:

$\begin{array}[]{r@{\hspace{.3cm}}r@{\hspace{.3cm}}l@{\hspace{.3cm}}l@{\hspace{.3cm}}lll}\textup{(enf
1)}\hskip 8.5359pt&\hskip 8.5359pt&\hfil\hskip
8.5359pt&t\not\Downarrow_{l}\hfil\hskip 8.5359pt&\textit{i.e.}~{}\text{has
no}\rightarrow_{l}\text{-normal form.}\\\ \textup{(enf 2)}\hskip
8.5359pt&t\Downarrow_{l}\,x\hskip 8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{l}\,x\hfil\hskip 8.5359pt\\\ \textup{(enf
3)}\hskip 8.5359pt&t\Downarrow_{l}\,\lambda x.t_{1}\hskip
8.5359pt&\text{and}\hfil\hskip 8.5359pt&t^{\prime}\Downarrow_{l}\,\lambda
x.t^{\prime}_{1}\hfil\hskip
8.5359pt&\text{with}~{}t_{1}~{}{\mathcal{R}}~{}t^{\prime}_{1}\\\ \textup{(enf
4)}\hskip 8.5359pt&t\Downarrow_{l}\,L\langle xv\rangle\hskip
8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{l}\,L^{\prime}\langle
xv^{\prime}\rangle\hfil\hskip
8.5359pt&\textup{with}~{}v~{}{\mathcal{R}}~{}v^{\prime}~{}\text{and}~{}L\langle
z\rangle~{}{\mathcal{R}}~{}L^{\prime}\langle z\rangle\\\ \hskip
8.5359pt&\hskip 8.5359pt&\hfil\hskip 8.5359pt&\hfil\hskip
8.5359pt&\text{where}~{}z~{}\text{is not free
in}~{}L~{}\text{or}~{}L^{\prime}\end{array}$

_$\mathsf{Enf}$ similarity_, written $\precsim_{\mathit{enf}}$, is defined by
co-induction as the largest $\mathsf{enf}$ simulation, that is, it is the
union of all $\mathsf{enf}$ simulations. We say that $t$ is _$\mathsf{enf}$
similar_ to $t^{\prime}$ if $t\precsim_{\mathit{enf}}t^{\prime}$.

##### Stop-and-Go, Double Task, and Left Identity.

The stop-and-go clause (enf 4) cleverly does two tasks at the same time,
subsuming clause (nai 4) of naive similarity in a bottom-up way and capturing
the left identity equivalence $\equiv_{lid}$.

About (nai 4), consider for instance comparing $t\coloneqq xyw$ with itself
via enf simulations. Clause (enf 4) reduces it to compare $zw$ and $y$ with
themselves, since $t=L\langle xy\rangle$ with $L\coloneqq\langle\cdot\rangle
w$. Then, it reduces the first one to compare $z^{\prime}$ and $w$ with
themselves. In contrast, (nai 4) (or Sangiorgi’s (cbn 4)) proceeds _top-down_
, by splitting $xyw$ into $xy$ and $w$, and then splitting $xy$.

About the left identity equivalence, consider showing that
$t\coloneqq\mathtt{I}(xx)$ and $u\coloneqq xx$ are enf similar. Evaluation is
stuck on $t$, that is, it _stops_ because $xx$ is not a value. Note that $t$
has shape $L\langle xv\rangle$ with $L=\mathtt{I}\langle\cdot\rangle$ and
$v=x$. The idea is that a term $u$ that is $\precsim_{\mathit{enf}}$-similar
to $t$ has to get stuck as well, or anyway decompose in a similar way. Now,
$u$ is not stuck, because there are no blocked redexes, but it has nonetheless
shape $L^{\prime}\langle xv^{\prime}\rangle$ by taking
$L^{\prime}=\langle\cdot\rangle$ and $v^{\prime}=x$. The comparison between
$t$ and $u$ is then reduced to compare the two pairs $L\langle
z\rangle=\mathtt{I}z$ and $L^{\prime}\langle z\rangle=z$, and $v=x$ and
$v^{\prime}=x$. The second pair trivially matches, because the identity
relation is an enf simulation. About the first pair, note that $\mathtt{I}z$
is no longer stuck, that is, it can _go_. And for the next round of comparison
(of $\mathtt{I}z$ and $z$) we have to first $\rightarrow_{l}$ reduce the
terms, so that $\mathtt{I}z\rightarrow_{l}z$ and thus also the first pair
trivially matches.

Summing up, the enf simulation relating $\mathtt{I}(xx)$ and $xx$ is the
following simulation ${\mathcal{R}}$:

${\mathcal{R}}=\\{(\mathtt{I}(xx),xx),(x,x),(\mathtt{I}z,z),(z,z)\\}$

This is just an instance, but the following more general result holds.

###### Proposition 8.3 (Enf bisimilarity validates left identity).

$\mathtt{I}t\simeq_{\mathit{enf}}t$ for any term $t$.

##### Left/Right/Weak Non-Equivalent Variants

Replacing left reduction with right reduction, one obtains a unique
decomposition lemma such as Lemma 8.1 with respect to right contexts, and,
accordingly, a notion of _right Lassen similarity_ —let us denote it with
$\precsim_{\mathit{renf}}$. It turns out that $\precsim_{\mathit{enf}}$ and
$\precsim_{\mathit{renf}}$ are different, incomparable similarities. For
instance, $\Omega$ and $\Omega(xx)$ are enf bisimilar (because they are both
$\rightarrow_{l}$-divergent) but not renf bisimilar, because
$\precsim_{\mathit{renf}}$ stops on $\Omega(xx)$ which is $\rightarrow_{r}$
normal. Similarly, $\Omega$ and $xx\Omega$ are not enf bisimilar while they
are renf bisimilar.

Replacing left reduction with weak reduction is instead problematic for
another reason. Since $\rightarrow_{w}$ is non-deterministic, the unique
decomposition lemma (Lemma 8.1) fails for it. It is not clear then what would
be the right definition of weak enf similarity, as the stop-and-go clause can
be generalized in more than one way. An appropriate definition for weak enf
similarity, as a generalization, should include terms related by enf
similarity. However, it is also unclear (to us) how to prove the compatibility
of some of such generalizations (we tried but failed111The definitions we can
come up with for weak enf similarities that could be compatible are not able
to relate as much terms as enf similarity does.).

The next paragraphs discuss the principles that are (in)validated by enf
similarity.

#####  $\beta_{v}$-Conversion

As for naive similarity, enf similarity contains $\beta_{v}$-conversion, thus
it contains left reduction as well as weak and right reductions.

###### Proposition 8.4 (${\beta_{v}}$-conversion is validated by enf
bisimilarity).

If $t=_{{\beta_{v}}}u$ then $t\simeq_{\mathit{enf}}u$.

##### Curry and Turing fix-Point Combinators are Enf Bisimilar.

The relation ${\mathcal{R}}$ proving that $Y_{v}\simeq_{nai}\Theta_{v}$ is not
an enf bisimulation. Nonetheless, it is easy to build an enf bisimulation that
relates Curry’s and Turing’s CbV fix-point combinators. The fact that those
combinators are naive bisimilar means that the _unstucking_ aspect of the
stop-and-go clause plays no role for their equivalence.

###### Proposition 8.5.

$Y_{v}\simeq_{\mathit{enf}}\Theta_{v}$, that is, Curry’s and Turing’s fix-
points are enf bisimilar.

#####  $\Omega$-Equivalence

Enf bisimilarity does not validate the $\Omega$-equivalence
$\equiv_{\Omega_{v}}$. For instance, the same counter-example used for naive
similarity works for enf, as we have $\Omega\precsim_{\mathit{enf}}\Omega^{L}$
but $\Omega^{L}\not\precsim_{\mathit{enf}}\Omega$. In fact,
$\simeq_{\mathit{enf}}$ equates some $\Omega$-terms that are separated by
$\simeq_{nai}$ and vice-versa. For instance, let $\delta_{3}\coloneqq\lambda
x.xxx$. The $\Omega$-term $\Omega_{3}\coloneqq\delta_{3}\delta_{3}$ is
divergent. We have that $\Omega^{L}_{3}\coloneqq(\lambda
x.\delta_{3})(yz)\delta_{3}$ is enf bisimilar to $\Omega^{L}$, because they
stop similarly and then both go to diverge. They are instead unrelated with
respect to $\precsim_{nai}$, because when compared as normal forms they do not
have the same structure. For the vice-versa, consider $xx\Omega$ and $\Omega$,
which are equated by $\simeq_{nai}$ but separated by $\simeq_{\mathit{enf}}$,
because $xx\Omega$ is left normal but weak divergent.

###### Proposition 8.6.

Enf bisimilarity does not validate $\Omega$-equivalence $\equiv_{\Omega_{v}}$.

The issue of enf with $\equiv_{\Omega_{v}}$ concerns clause (enf 1), as left
diverging terms are a strict subset of CbV $\Omega$-terms. To solve it, as
usual, there are two options, changing the calculus or the nf-bisimilarity.
Biernacki et al. (2019a) change the nf-bisimilarity, extending (enf 1) to all
_deferred diverging terms_ , which correspond exactly to their (CbV + state)
$\Omega$-terms. Their approach does not address the reason why $\Omega$-terms
are not equated (namely, the stuck normal forms of Plotkin’s CbV), it only
circumvents it, and it does not help when that reason affects other aspects
such as commuting $\sf{let}$s (which happens when one of the two $\sf{let}$s
is blocked deep under a stuck redex). Addressing the reason and removing stuck
normal forms amounts in fact to changing the calculus. In Sect. 11, we shall
introduce a nf-bisimilarity smoothly validating both $\equiv_{\Omega_{v}}$ and
commuting $\sf{let}$s, as it is built on an extension of Plotkin’s calculus
not suffering from stuck normal forms.

##### Further Equivalences.

The next proposition sums up the benchmarks for enf.

###### Proposition 8.7.

Enf bisimilarity validates Moggi’s equivalences, the left-to-right
restrictions of the proof nets equivalences, but it does not validate
$\eta_{v}$, all of the unrestricted proof nets equivalences, nor CbN
duplication.

Enf similarity does not validate $\eta_{v}$, since $x$ and $\lambda y.xy$ are
handled by different clauses in the definition of $\precsim_{\mathit{enf}}$.
It can however be adapted to validate $\eta_{v}$, see (Lassen, 2005a; Støvring
and Lassen, 2007; Biernacki et al., 2019b). About Moggi’s equivalences, we
have already discussed the left identity. Enf similarity validates all the
other ones. Note that in (2005a) Lassen claims that enf validates
$\equiv_{exrad}$ (defined in Sect. 5) which is actually false, it only
validates $\equiv_{rad}$ (in fact $\equiv_{exrad}$ does not correspond to
Moggi’s usual right decomposition rule, it shall be motivated by proof nets in
Sect. 10). Proofs of the validations are easy, one only needs to write the
right relation (the identity relation $\cup$ the equivalence to validate) and
show that it is indeed an $\mathsf{enf}$ bisimulation.

The validation of the left-to-right restricted versions of the proof nets
equivalences ($\equiv_{@l}$ and a restricted version of $\equiv_{@r}$) is an
easy contribution of this paper. Simple inspections show that enf does not
validate the (order-unspecified) proof nets equivalences $\equiv_{@r}$ and
$\equiv_{com}$, nor CbN duplication. Consider now renf bisimilarity, the right
variant of enf. With respect to proof nets equivalences, it has a sort of dual
behavior: it does not validate $\equiv_{@l}$ but instead validates the right-
to-left proof nets equivalences ($\equiv_{@r}$ and a restricted version of
$\equiv_{@l}$).

##  9\. Value Substitution Calculus

$\begin{array}[]{rrll@{\hspace{1cm}}rrll}\lx@intercol\hfil\textsc{Language}\hfil\lx@intercol&\lx@intercol\hfil\textsc{Lists
of<EMAIL_ADDRESS>\textsc{Terms
}&\Lambda_{\mathsf{v}{\mathsf{sub}}}\ni t,u,s&\Coloneqq&v\mid tu\mid
t[x{\shortleftarrow}u]\hfil\hskip 28.45274pt&\textsc{Sub. ctxs
}&S,S^{\prime}&\Coloneqq&\langle\cdot\rangle\mid S[x{\shortleftarrow}t]\\\
\textsc{Values }&v,v^{\prime}&\Coloneqq&x\mid\lambda x.t\par\hfil\hskip
28.45274pt\end{array}$
---
  | Weak reduction
---
$\begin{array}[]{r@{\hspace{.15cm}}r<EMAIL_ADDRESS>Contexts}\hskip 4.26773pt&E\hskip 2.84544pt&\Coloneqq\hfil\hskip
2.84544pt&\langle\cdot\rangle\mid tE\mid Et\mid E[x{\shortleftarrow}u]\mid
t[x{\shortleftarrow}E]\par\end{array}$
| $\begin{array}[]{rr@{\ }l@{\ }l}\lx@intercol\hfil\textsc{Root rules}\hfil\lx@intercol\\\ \textsc{Mult. }&S\langle\lambda x.t\rangle u&\mapsto_{\mathsf{m}}&S\langle t[x{\shortleftarrow}u]\rangle\\\ \textsc{Exp.}&t[x{\shortleftarrow}S\langle v\rangle]&\mapsto_{\mathsf{e}}&S\langle t\\{x{\shortleftarrow}v\\}\rangle\par\end{array}$ | $\begin{array}[]{rr@{\ }l@{\ }l}\textsc{Contextual Closure}\\\ \lx@intercol\ignorespaces\ignorespaces\leavevmode\lower 26.10316pt\hbox{\vbox{\hbox{\hskip 16.84726pt\hbox{\hskip 4.0pt\hbox{$t\mapsto_{a}t^{\prime}$}\hskip 4.0pt}}\vskip 2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox to56.19456pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip 2.0pt\nointerlineskip\hbox{\hbox{\hskip 4.0pt\hbox{$E\langle t\rangle\rightarrow_{a}E\langle t^{\prime}\rangle$}\hskip 4.0pt}}}}\ignorespaces\ \ \ a\\!\in\\!\\{{\mathtt{m}},{\mathtt{e}}\\}\hfil\lx@intercol\par\end{array}$
---|---
$\begin{array}[]{l@{\hspace{.15cm}}r<EMAIL_ADDRESS>4.26773pt&\ \rightarrow_{\mathtt{vsc}}\hskip 2.84544pt&\coloneqq\hfil\hskip
2.84544pt&\rightarrow_{\mathsf{m}}\cup\rightarrow_{\mathsf{e}}\end{array}$
normal forms
$\begin{array}[]{r<EMAIL_ADDRESS>terms}\hskip 14.22636pt&i,i^{\prime}&\Coloneqq&L_{i}\langle xn\rangle\mid
in\mid i[x{\shortleftarrow}i^{\prime}]&\textsc{ Inert Sub. ctxs}\hskip
14.22636pt&L_{i}&\Coloneqq&\langle\cdot\rangle\mid
L_{i}[x{\shortleftarrow}i]\par\end{array}$
<EMAIL_ADDRESS>forms}\hskip 14.22636pt&n,n^{\prime}&\Coloneqq&v\mid i\mid
n[x{\shortleftarrow}i]\end{array}$
Figure 1. Value substitution calculus and normal forms.

Intuitively, the VSC is a CbV $\lambda$-calculus extended with
$\sf{let}$-expressions, as is common for CbV $\lambda$-calculi such as Moggi’s
one [(1988; 1989)]. We do however replace a $\sf{let}$-expression ${\sf let}\
x=u\ {\sf in}\ t$ with a more compact _explicit substitution_ (ES for short)
notation $t[x{\shortleftarrow}u]$, which binds $x$ in $t$ and that has
precedence over abstraction and application (that is, $\lambda
x.t[y{\shortleftarrow}u]$ stands for $\lambda x.(t[y{\shortleftarrow}u])$ and
$ts[y{\shortleftarrow}u]$ for $t(s[y{\shortleftarrow}u])$). Moreover, our
$\sf{let}$/ES does not fix an order of evaluation between $t$ and $u$, in
contrast to many papers in the literature (e.g. Sabry and Wadler (1997); Levy
et al. (2003)) where $u$ is evaluated first.

The reduction rules of VSC are slightly unusual as they use _contexts_ both to
allow one to reduce redexes located in sub-terms, which is standard, _and_ to
define the redexes themselves, which is less standard—these kind of rules is
called _at a distance_. The rationale behind is that the rewriting rules are
designed to mimic exactly cut-elimination on linear logic proof nets, via
Girard’s (1987) CbV translation $(A\Rightarrow B)^{v}=!(A^{v}\multimap B^{v})$
of intuitionistic logic into linear logic, see Accattoli (2015).

##### Root rewriting rules

In VSC, there are two main rewrite rules, the _multiplicative_ one
$\rightarrow_{\mathsf{m}}$ and the _exponential_ one
$\rightarrow_{\mathsf{e}}$ (the terminology comes from the connection between
VSC and linear logic), and both work _at a distance_ : they use contexts even
in the definition of their _root_ rules (that is, before the contextual
closure). Their definition is based on _substitution contexts_ $S$, which are
lists of ES. In Figure 1, the root rule $\mapsto_{\mathsf{m}}$ (resp.
$\mapsto_{\mathsf{e}}$) is assumed to be capture-free, so no free variable of
$u$ (resp. $t$) is captured by the substitution context $S$ (by possibly
$\alpha$-renaming on-the-fly).

Examples: $(\lambda
x.y)[y{\shortleftarrow}t]u\mapsto_{\mathsf{m}}y[x{\shortleftarrow}u][y{\shortleftarrow}t]$
and $(\lambda
z.xx)[x{\shortleftarrow}y[y{\shortleftarrow}t]]\mapsto_{\mathsf{e}}(\lambda
z.yy)[y{\shortleftarrow}t]$. An example with on-the-fly $\alpha$-renaming is
$(\lambda
x.y)[y{\shortleftarrow}t]y\mapsto_{\mathsf{m}}z[x{\shortleftarrow}y][z{\shortleftarrow}t]$.

A key point is that $\beta$-redexes are decomposed via ES: the _by-value_
restriction is on ES-redexes, _not_ on $\beta$-redexes, because only values
can be substituted. The multiplicative rule $\mapsto_{\mathsf{m}}$ fires a
$\beta$-redex at a distance and generates an ES even when the argument is not
a value. The CbV discipline is entirely encoded in the exponential rule
$\rightarrow_{\mathsf{e}}$ (see Figure 1): it can fire an ES performing a
substitution only when its argument is a _value_ (i.e. a variable or an
abstraction) up to a list of ES. This means that only values can be duplicated
or erased.

##### Rewriting Rules

We define weak reduction, noted $\rightarrow_{\mathtt{vsc}}$, to be the
closure of the root rules by evaluation contexts which allow reduction
everywhere but under lambdas. In other papers about the VSC (Accattoli and
Paolini, 2012; Accattoli and Guerrieri, 2016; Accattoli et al., 2021;
Accattoli and Guerrieri, 2022), where other contextual closures are also
considered, they are called _weak_ or _open_ contexts. Examples:

$\begin{array}[]{r@{\hspace{.1cm}}r<EMAIL_ADDRESS>r@{\hspace{.1cm}}r@{\hspace{.1cm}}l}t[x{\shortleftarrow}(\lambda
y.u)[z{\shortleftarrow}s]r]\hskip 2.84544pt&\rightarrow_{\mathsf{m}}\hskip
2.84544pt&t[x{\shortleftarrow}u[y{\shortleftarrow}r][z{\shortleftarrow}s]]\hfil\hskip
14.22636pt&t(xx)[x{\shortleftarrow}y[z{\shortleftarrow}u]]\hskip
2.84544pt&\rightarrow_{\mathsf{e}}\hskip
2.84544pt&t(yy)[z{\shortleftarrow}u]\\\\[2.0pt]
((xx)[x{\shortleftarrow}\lambda y.z]t)[w{\shortleftarrow}u]\hskip
2.84544pt&\rightarrow_{\mathsf{e}}\hskip 2.84544pt&((\lambda y.z)(\lambda
y.z)t)[w{\shortleftarrow}u]\hfil\hskip 14.22636pt&\lambda
z.(xx)[x{\shortleftarrow}\lambda y.z]\hskip
2.84544pt&\not\rightarrow_{\mathsf{e}}\hskip 2.84544pt&\lambda z.(\lambda
y.z)\lambda y.z\end{array}$

##### Diamond

The $\rightarrow_{\mathtt{vsc}}$ reduction is non-deterministic, as for
instance:

$\delta(\delta\mathtt{I})\ \;\mbox{}_{\mathsf{e}_{\lambda}}{\leftarrow}\ \
y[y{\shortleftarrow}\delta](\delta\mathtt{I})\ \rightarrow_{\mathsf{m}}\
y[y{\shortleftarrow}\delta]((xx)[x{\shortleftarrow}\mathtt{I}]).$

It is however more than confluent, it is diamond.

###### Proposition 9.1 (Diamond, (Accattoli and Paolini, 2012)).

$\rightarrow_{\mathtt{vsc}}$ is diamond.

We now investigate normal forms for terms in the VSC, which admit a, quite
complex, inductive description via _inert terms_.

##### Inert Terms and Normal Forms

CbV is about _values_ , and, if terms are closed, normal forms are
abstractions. In going beyond the closed setting, a finer and more general
view is required. Normal forms (for $\rightarrow_{\mathtt{vsc}}$) are given by
mutual induction with the notions of _inert term_ and _inert substitution
contexts_ , as in Figure 1. Inert substitution contexts are lists of ESs where
the content of every ES is an inert, ensuring that none of the ESs can fire a
$\rightarrow_{\mathsf{e}}$-redex (as inerts are exactly normal forms which are
not of the shape $S\langle v\rangle$).

Examples: $\lambda x.y$ is a normal form as an abstraction, while $y(\lambda
x.x)$, $xy$, and $(z(\lambda x.x))(zz)(\lambda y.(zy))$ are normal forms as
inert terms. The grammars also allow to have ES containing inert terms around
abstractions and applications: $(\lambda x.y)[y{\shortleftarrow}zz]$ is a
normal form and $x[x{\shortleftarrow}y(\lambda x.x)]y$ is an inert term. One
of the key points of inert terms is that they have a _free_ head variable (in
particular they are open). Inert terms are the CbV equivalent of CbN neutral
terms. In (Grégoire and Leroy, 2002), inert terms are called _accumulators_ ,
and normal forms are called _values_. Some papers about the VSC adopt a
restricted version of the $\rightarrow_{\mathtt{vsc}}$ reduction, where
variables are not values and thus cannot be substituted by the
$\rightarrow_{\mathsf{e}}$-rule. The restriction induces slightly different
notions of normal forms (often called _fireballs_) and inert terms (still
called _inert terms_), but the difference does not change the main properties
of the VSC, as discussed in (Accattoli and Guerrieri, 2022).

###### Proposition 9.2 (Normal forms, (Accattoli and Paolini, 2012) ).

$t$ is $\rightarrow_{\mathtt{vsc}}$-normal if and only if $t$ is a $n$-term as
defined in Figure 1.

#####  $\Omega$-Equivalence

One of the features of the VSC is that it solves the issues of Plotkin’s
calculus with respect to CbV $\Omega$-terms. Consider the $\Omega$-term
$\Omega^{L}=(\lambda x.\delta)(yz)\delta$ which is contextually equivalent to
$\Omega$ but normal for Plotkin. In the VSC, instead, it diverges:

$(\lambda
x.\delta)(yz)\delta\rightarrow_{\mathsf{m}}\delta[x{\shortleftarrow}yz]\delta\rightarrow_{\mathsf{m}}ww[w{\shortleftarrow}\delta][x{\shortleftarrow}yz]\rightarrow_{\mathsf{e}_{\lambda}}\delta\delta[x{\shortleftarrow}yz]\rightarrow_{\mathsf{m}}\ldots$.

More generally, _all_ CbV $\Omega$-terms diverge: the following
characterization of CbV $\Omega$ holds, analogous to the one for CbN (Thm.
2.3) and obtained composing the diverging characterization of CbV inscrutable
terms due to Accattoli and Paolini (2012) with an easy proposition (in
Appendix C (p. C)) showing that CbV inscrutable terms and CbV $\Omega$-terms
coincide.

###### Theorem 9.3 (VSC diverging characterization of $\Omega$-terms).

$t$ is a CbV $\Omega$-term if and only if $t$ is $\rightarrow_{\mathtt{vsc}}$
diverging.

Despite the fact that the VSC makes $\Omega^{L}$ diverge as in CbN, it does
_not_ validate CbN duplication nor CbN erasure, as $(\lambda x.y)\Omega$ is
$\rightarrow_{\mathtt{vsc}}$-divergent and $(\lambda
x.yxx)(zz)\rightarrow_{\mathsf{m}}(yxx)[x{\shortleftarrow}zz]\not\rightarrow_{\mathtt{vsc}}y(zz)(zz)$.

##### Contextual Equivalence

Terms such as $\Omega^{L}$ are normal for Plotkin but divergent in the VSC,
that is, the VSC and Plotkin’s calculus have different notions of termination.
One might then suspect that contextual equivalence in the VSC is not the same
as in Plotkin’s calculus. This is not the case, in fact, because the VSC
behaves differently _only on open terms_ , while contextual equivalence is
defined reducing _closed terms_ only.

###### Proposition 9.4 ((Accattoli and Guerrieri, 2022)).

Two $\lambda$-terms without ES are contextual equivalent in Plotkin’s calculus
if and only if they are contextual equivalent in the VSC.

##  10\. Equational Benchmarks and the Value Substitution Calculus

Here, we revisit the equational benchmarks of Sect. 5 in the VSC. We begin
with the proof nets equivalences, as they are one of the _raison d’être_ of
the VSC and the key to re-understand them all.

##### Structural Equivalence

The translation of the VSC to proof nets maps some terms with ES to the same
proof net. The induced identification of terms is expressed by structural
equivalence (Accattoli and Paolini, 2012; Accattoli, 2015).

###### Definition 10.1 (Structural equivalence $\equiv_{str}$).

Structural equivalence $\equiv_{str}$ is defined as the smallest compatible
equivalence relation generated by union of the following root rules.

$\begin{array}[]{rllrcc}(ts)[x{\shortleftarrow}u]&\equiv_{@l}&t[x{\shortleftarrow}u]s&\mbox{if
}x\not\in{\tt fv}(s)\\\
(ts)[x{\shortleftarrow}u]&\equiv_{@r}&ts[x{\shortleftarrow}u]&\mbox{if
}x\not\in{\tt fv}(t)\\\
t[x{\shortleftarrow}u][y{\shortleftarrow}s]&\equiv_{ass}&t[x{\shortleftarrow}u[y{\shortleftarrow}s]]&\mbox{if
}y\not\in{\tt fv}(t)\\\
t[y{\shortleftarrow}s][x{\shortleftarrow}u]&\equiv_{com}&t[x{\shortleftarrow}u][y{\shortleftarrow}s]&\mbox{if
}x\not\in{\tt fv}(s)\mbox{ and }y\not\in{\tt fv}(u)\end{array}$

These axioms preserve the number and type of the constructors in terms, they
only rearrange the order. In particular, structurally equivalent terms have
the same number of ES. Note that the axioms simply express the constructor-
and-scope-preserving commutation of ES with applications and ES themselves
(but not abstractions, as that would break Prop. 10.2 below).

Additionally, structural equivalence behaves very well with respect to
evaluation: it commutes with reduction rules—and is therefore
postponable—preserving the number and kind of steps. This is expressed by the
following proposition. In the literature, what is below called _strong
commutation_ is usually called _strong bisimulation_. We prefer to change the
terminology here to avoid confusion with _nf-(bi)simulations_ , as the concept
is similar and yet different (no need to observe normal forms, and it
preserves the number of steps).

###### Proposition 10.2 ($\equiv_{str}$ strongly commutes with
$\rightarrow_{\mathtt{vsc}}$, Accattoli and Paolini (2012)).

Let $a\in\\{{\mathtt{m}},\mathsf{e}_{\lambda},\mathsf{e}_{y}\\}$. Structural
equivalence $\equiv_{str}$ strongly commutes with
$\rightarrow_{\mathtt{vsc}}$: if $t\equiv_{str}u$ and
$t\rightarrow_{a}t^{\prime}$ then $u\rightarrow_{a}u^{\prime}$ and
$t^{\prime}\equiv_{str}u^{\prime}$.

In fact, $\equiv_{str}$-equivalence classes are an isomorphic representation
of proof nets, as the proof net $P_{t}$ associated to $t$ does the same exact
rewriting steps as $t$, that is, the translation from $t$ to $P_{t}$ also
strongly commutes with evaluation (turning term steps into proof nets steps,
and vice-versa), see Accattoli (2015). Consequently, $\equiv_{str}$-equivalent
terms are _indistinguishable_ and should be equated by any sensible notion of
program equivalence on pure terms (extensions with effects can invalidate some
cases of structural equivalence, typically $\equiv_{com}$, as we discuss
below). In particular, structural equivalence is included in contextual
equivalence, as shown by Accattoli and Guerrieri (2022).

##### Revisiting the Benchmarks From Calculi

The equivalences of Moggi’s can be re-understood via structural equivalence.
The idea is that by applying $\rightarrow_{\mathsf{m}}$ to the two sides of an
equivalence, we can express it via ES, and many of become cases of
$\equiv_{str}$. Consider $\equiv_{ass}$:

$\begin{array}[]{ccccc}(\lambda y.t)((\lambda x.u)s)&\equiv_{ass}&(\lambda
x.(\lambda y.t)u)s)&\mbox{with }x\notin\lambda y.t\\\
\downarrow_{\mathsf{m}}&&\downarrow_{\mathsf{m}}\\\ (\lambda
y.t)u[x{\shortleftarrow}s]&\equiv_{@r}&((\lambda
y.t)u)[x{\shortleftarrow}s]\end{array}$

Similarly, the equivalences $\equiv_{@r}$ and $\equiv_{com}$ of Sect. 5 become
the axioms with the corresponding label of $\equiv_{str}$. Therefore,
structural equivalence covers the proof nets equivalences. Moggi’s
equivalences $\equiv_{lid}$, $\equiv_{lad}$ and $\equiv_{rad}$, instead, are
not covered. By applying $\rightarrow_{\mathsf{m}}$, we obtain the following
reformulation for the VSC which corresponds to Moggi’s original formulation
with $\sf{let}$-expressions. If $x\notin{\tt fv}(u)$ for $\equiv_{lad}$ and
$x\notin{\tt fv}(v)$ for $\equiv_{rad}$:

$\begin{array}[]{ccccc}(\lambda x.x)t&\equiv_{lid}&t\\\ \downarrow_{\mathsf{m}}&&=\\\ x[x{\shortleftarrow}t]&\equiv_{lid}&t\end{array}$ |  $\begin{array}[]{ccccc}(\lambda x.xu)t&\equiv_{lad}&tu\\\ \downarrow_{\mathsf{m}}&&=\\\ (xu)[x{\shortleftarrow}t]&\equiv_{lad}&tu\end{array}$ | $\begin{array}[]{ccccc}(\lambda x.vx)t&\equiv_{rad}&vt\\\ \downarrow_{\mathsf{m}}&&\downarrow_{\mathsf{m}}\\\ (vx)[x{\shortleftarrow}t]&\equiv_{rad}&vt\end{array}$
---|---|---

In presence of structural equivalence, the ES formulation of the application
decomposition equivalences $\equiv_{lad}$ and $\equiv_{rad}$ is derivable:
$\equiv_{lad}$ follows from $\equiv_{@l}$ and $\equiv_{lid}$, $\equiv_{rad}$
follows from $\equiv_{@r}$ and $\equiv_{lid}$. In fact, by using the
(unrestricted) proof nets equivalence $\equiv_{@r}$ we can actually derive the
extended version of $(ux)[x{\shortleftarrow}t]\equiv_{exrad}ut$ (if
$x\notin{\tt fv}(u)$) of $\equiv_{rad}$. Therefore, the whole of Moggi’s
equivalences is captured by simply adding $\equiv_{lid}$ to structural
equivalence.

##### A Family of Strong Commutations

It turns out that various sub-relations of structural equivalence also verify
strong commutation (to allow one to verify the claims of this paragraph, the
proof of Prop. 10.2 is in Appendix D of the additional material on HotCRP, as
the proof is omitted from Accattoli and Paolini (2012) where the result first
appeared). We here describe them by the root rules, while implicitly referring
to the same closure used in the definition of $\equiv_{str}$. For instance,
$\equiv_{com}$ by itself strongly commutes with $\rightarrow_{\mathtt{vsc}}$,
as well as $\equiv_{@l}$ by itself, or $\equiv_{@r}\cup\equiv_{ass}$, or some
of the restricted version such as ${(\equiv_{@r})_{|ltr}}\cup\equiv_{ass}$,
where $(\equiv_{@r})_{|ltr}$ is the _left-to-right_ restriction of
$\equiv_{@r}$. In particular,
$\equiv_{@l}\cup(\equiv_{@r})_{|ltr}\cup\equiv_{ass}$, which would be the
restriction of $\equiv_{str}$ to a non-commutative setting for effects, also
strongly commutes with $\rightarrow_{\mathtt{vsc}}$. In the next section, we
shall craft a nf-similarity for the VSC which is parametric with respect to
these variants of structural equivalence.

##### Shuffling

Carraro and Guerrieri’s _shuffling calculus_ (2014) is yet another extension
of Plotkin’s calculus with the CbV variants of two shuffling rules introduced
in CbN by Regnier (1994), and it is used in semantical studies about CbV
(Guerrieri et al., 2017; Kerinec et al., 2020). Its CbV shuffling rules are
also instances of structural equivalence if one applies
$\rightarrow_{\mathsf{m}}$ steps as discussed above.

##  11\. Net Similarity for the Value Substitution Calculus

In this section, we finally define the nf-similarity for the VSC we are
interested in, _net similarity_ , which extends $\precsim_{nai}$ along two
axes:

  1. (1)

_Changing the underlying calculus:_ evaluation is now based on the VSC, where
$\Omega$-terms have a diverging characterization, hence $\Omega$-equivalence
$\equiv_{\Omega}$ will be trivially included in the bisimilarity, and

  2. (2)

_Changing the nf-bisimilarity_ : allowing simulations to test terms modulo
structural equivalence $\equiv_{str}$, in order to avoid artificial
distinctions of indistinguishable terms and to validate the commutation of
$\sf{let}$s $\equiv_{com}$.

The problematic addition of the left identity equivalence $\equiv_{lid}$ is
discussed at the end of the section.

##### Changing the Underlying Calculus

Moving from Plotkin’s CbV calculus to the VSC, normal forms are harder to
describe, as one can see from the grammar of normal forms in Figure 1.

Since the case $L_{i}\langle x\rangle n$ is quite unpleasant to manage in
proofs, we go one step further and consider normal forms modulo $\equiv_{@l}$,
picking the $\equiv_{@l}$-representative of each normal form where the context
$L_{i}$ has been pushed out of the unpleasant case for inert terms. This can
be done harmlessly because $\equiv_{@l}$ by itself verifies strong
_commutation_ with respect to $\rightarrow_{\mathtt{vsc}}$ and the described
representant can be easily described at the big-step level. The following
lemma gives a grammar for normal forms modulo $\equiv_{@l}$; we
overload/redefine _inert terms_ , which from now on only refer to the new
grammar.

###### Lemma 11.1.

$t$ is $\rightarrow_{\mathtt{vsc}}$-normal iff there exists $n$, given by the
following grammar, such that $t\equiv_{@l}n$.

<EMAIL_ADDRESS>Inert terms}\hskip
14.22636pt&\mathbb{i},\mathbb{i}^{\prime}&\Coloneqq&xn\mid\mathbb{i}n\\\
\textsc{Inert terms}\hskip 14.22636pt&i,i^{\prime}&\Coloneqq&\mathbb{i}\mid
i[x{\shortleftarrow}i^{\prime}]\\\ \rightarrow_{\mathtt{vsc}}\textsc{-normal
forms modulo $\equiv_{@l}$}\hskip 14.22636pt&n,n^{\prime}&\Coloneqq&v\mid
i\mid n[x{\shortleftarrow}i^{\prime}]\end{array}$

Note the notion of applicative inert terms, which are specific inert terms
where no substitutions can be pushed outward by $\equiv_{@l}$. Example: the
$\rightarrow_{\mathtt{vsc}}$-normal form $t=x[x{\shortleftarrow}yy]z$ does not
belong to grammar above, but $t\equiv_{@l}(xz)[x{\shortleftarrow}yy]=n$ and
$n$ is described by the grammar.

##### Big-Step Evaluation

We then need to express evaluation to $\rightarrow_{\mathtt{vsc}}$-normal form
modulo $\equiv_{@l}$ as a big-step predicate. For that, we re-define the inert
substitution contexts, which at first sight are defined as before, except that
the notion of inert term now has changed.

<EMAIL_ADDRESS>Substitution
Contexts}\hskip 14.22636pt&L_{i}&\Coloneqq&\langle\cdot\rangle\mid
L_{i}[x{\shortleftarrow}i]\end{array}$

###### Definition 11.2 (Big-step evaluation $\Downarrow_{\mathtt{vsc}}^{k}$).

Big-step VSC modulo $\equiv_{@l}$ evaluation $t\Downarrow_{\mathtt{vsc}}^{k}n$
is given by:

$v\Downarrow_{\mathtt{vsc}}^{0}v$ | $tu\Downarrow_{\mathtt{vsc}}^{k+i+1}L_{i}\langle n\rangle\lx@proof@logical@and t\Downarrow_{\mathtt{vsc}}^{k}L_{i}\langle\lambda x.s\rangle{s[x{\shortleftarrow}u]}\Downarrow_{\mathtt{vsc}}^{i}n$
---|---
$tu\Downarrow_{\mathtt{vsc}}^{k+h}L_{i}\langle xn\rangle\lx@proof@logical@and t\Downarrow_{\mathtt{vsc}}^{k}L_{i}\langle x\rangle u\Downarrow_{\mathtt{vsc}}^{h}n$ | $t[x{\shortleftarrow}u]\Downarrow_{\mathtt{vsc}}^{k+i+1}L_{i}\langle n\rangle\lx@proof@logical@and u\Downarrow_{\mathtt{vsc}}^{k}L_{i}\langle v\rangle{t\\{x{\shortleftarrow}v\\}}\Downarrow_{\mathtt{vsc}}^{i}n$
$tu\Downarrow_{\mathtt{vsc}}^{k+h}L_{i}\langle\mathbb{i}n\rangle\lx@proof@logical@and t\Downarrow_{\mathtt{vsc}}^{k}L_{i}\langle\mathbb{i}\rangle u\Downarrow_{\mathtt{vsc}}^{h}n$ | $t[x{\shortleftarrow}u]\Downarrow_{\mathtt{vsc}}^{k+h}n[x{\shortleftarrow}i]\lx@proof@logical@and t\Downarrow_{\mathtt{vsc}}^{k}nu\Downarrow_{\mathtt{vsc}}^{h}i$

_Notation_ : $t\Downarrow_{\mathtt{vsc}}\,n$ abbreviates _there exists a $k$
such that $t\Downarrow_{\mathtt{vsc}}^{k}n$_.

The given big-step system captures $\equiv_{@l}$ via the rules
(${\Downarrow}\textsc{-@}x$) and (${\Downarrow}\textsc{-@i}$): when applying
an inert term / variable surrounded by an inert context $L_{i}$ to a normal
term $n$, the context $L_{i}$ is pushed out of the application, obtaining
$L_{i}\langle xn\rangle$ and $L_{i}\langle\mathbb{i}n\rangle$ instead of
$L_{i}\langle x\rangle n$ and $L_{i}\langle\mathbb{i}\rangle n$. As a result,
the $\Downarrow_{\mathtt{vsc}}$-normal forms are exactly those of the given
grammar for $\rightarrow_{\mathtt{vsc}}$-normal forms modulo $\equiv_{@l}$.

We prove this big-step system to be correct and complete with respect to
small-step reduction. Importantly, substitutivity also smoothly adapts.

###### Proposition 11.3.

$t\Downarrow_{\mathtt{vsc}}^{k}n$ if and only if there exists a normal form
$n^{\prime}$ such that
$t\rightarrow_{\mathtt{vsc}}^{k}n^{\prime}\equiv_{@l}n$.

###### Proposition 11.4 (Substitutivity).

  1. (1)

_Small-step_ : if $t~{}\rightarrow_{\mathtt{vsc}}~{}t^{\prime}$ then
$t\\{x{\shortleftarrow}v\\}~{}\rightarrow_{\mathtt{vsc}}~{}t^{\prime}\\{x{\shortleftarrow}v\\}$.

  2. (2)

_Big-step_ : if $t\\{x{\shortleftarrow}v\\}\Downarrow_{\mathtt{vsc}}^{k}n$
then $\exists$ $k^{\prime}$ and $n^{\prime}$ such that
$t\Downarrow_{\mathtt{vsc}}^{k^{\prime}}n^{\prime}$ and
$n^{\prime}\\{x{\shortleftarrow}v\\}\Downarrow_{\mathtt{vsc}}^{k-k^{\prime}}n$.

##### Changing the Nf-Bisimilarity by Adding Structural Equivalence to
Simulations, Parametrically

We are now also going to refine the definition of naive similarity by adding
structural equivalence $\equiv_{str}$ to the nf-bisimilarity. In fact, we are
going to do something more general, in order to obtain a whole family of
similarities. We abstract away structural equivalence $\equiv_{str}$ as a more
abstract notion of _mirror equivalence_ $\equiv_{M}$, defined by the
properties of $\equiv_{str}$ that are needed to prove that similarity modulo
$\equiv_{str}$ is compatible. Then, similarity is defined _parametrically_ in
a mirror $\equiv_{M}$, and net similarity is obtained by taking $\equiv_{str}$
as mirror. The terminology _mirror_ is meant to suggest that $\equiv_{M}$ can
modify terms only in inessential ways.

###### Definition 11.5 (Mirror).

An equivalence relation $\equiv_{M}$ is a _mirror_ for
$\rightarrow_{\mathtt{vsc}}$ when:

  1. (1)

_Strong commutation_ : if $t\equiv_{M}u$ and
$t\rightarrow_{\mathtt{vsc}}t^{\prime}$ then
$u\rightarrow_{\mathtt{vsc}}u^{\prime}$ and $t^{\prime}\equiv_{M}u^{\prime}$.

  2. (2)

_Substitutivity_ : if $t\equiv_{M}u$ then
$t\\{x{\shortleftarrow}v\\}\equiv_{M}u\\{x{\shortleftarrow}v\\}$ for all
values $v$.

###### Definition 11.6 (Mirrored and net similarities).

Let ${\mathcal{R}}$ be relation and $\equiv_{M}$ be a mirror over VSC terms.
We say that ${\mathcal{R}}$ is a _$\equiv_{M}$ -mirrored (mirM) simulation_ if
${\mathcal{R}}\subseteq\langle{\mathcal{R}}\rangle_{\mathtt{mir}_{M}}$, where
$t\langle{\mathcal{R}}\rangle_{\mathtt{mir}_{M}}t^{\prime}$ holds whenever
$t,t^{\prime}$ satisfy one of the following clauses:

$\begin{array}[]{r@{\hspace{.3cm}}r@{\hspace{.3cm}}l@{\hspace{.3cm}}l@{\hspace{.3cm}}lll}\textup{(mir${}_{M}$
1)}\hskip 8.5359pt&\hskip 8.5359pt&\hfil\hskip
8.5359pt&t\not\Downarrow_{\mathtt{vsc}}\hfil\hskip
8.5359pt&\textit{i.e.}~{}\text{has no}\rightarrow_{\mathtt{vsc}}\text{-normal
form.}\\\ \textup{(mir${}_{M}$ 2)}\hskip
8.5359pt&t\Downarrow_{\mathtt{vsc}}\,x\hskip 8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{\mathtt{vsc}}\,x\hfil\hskip 8.5359pt\\\
\textup{(mir${}_{M}$ 3)}\hskip 8.5359pt&t\Downarrow_{\mathtt{vsc}}\,\lambda
x.t_{1}\hskip 8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{\mathtt{vsc}}\,\lambda
x.t^{\prime}_{1}\hfil\hskip
8.5359pt&\text{with}~{}t_{1}~{}{\mathcal{R}}~{}t^{\prime}_{1}\\\
\textup{(mir${}_{M}$ 4)}\hskip
8.5359pt&t\Downarrow_{\mathtt{vsc}}\,n_{1}n_{2}\hskip
8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{\mathtt{vsc}}\,n^{\prime}\equiv_{M}n_{1}^{\prime}n_{2}^{\prime}\hfil\hskip
8.5359pt&\text{with}~{}n_{1}~{}{\mathcal{R}}~{}n_{1}^{\prime}~{}\text{and}~{}n_{2}~{}{\mathcal{R}}~{}n_{2}^{\prime}\\\
\textup{(mir${}_{M}$ 5)}\hskip
8.5359pt&t\Downarrow_{\mathtt{vsc}}\,n_{1}[x{\shortleftarrow}n_{2}]\hskip
8.5359pt&\text{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{\mathtt{vsc}}\,n^{\prime}\equiv_{M}n_{1}^{\prime}[x{\shortleftarrow}n_{2}^{\prime}]\hfil\hskip
8.5359pt&\text{with}~{}n_{1}~{}{\mathcal{R}}~{}n_{1}^{\prime}~{}\text{and}~{}n_{2}~{}{\mathcal{R}}~{}n_{2}^{\prime}\end{array}$

$\equiv_{M}$-Mirrored (mirM) similarity , written
$\precsim_{\mathtt{mir}_{M}}$, is defined the largest $\equiv_{M}$-mirrored
simulation.

Net simulations and net similarity $\precsim_{\mathit{net}}$ are defined as
the $\equiv_{M}$-mirrored simulations and similarities with structural
equivalence $\equiv_{str}$ as mirror $\equiv_{M}$.

##### Making Inert Terms Explicit in the Clauses

Cases (mirM 4) and (mirM 5) can be rewritten using the grammar of normal
forms, which is useful for clarity in proofs. For (mirM 4), it actually splits
in two:

$\begin{array}[]{r@{\hspace{.3cm}}r@{\hspace{.3cm}}l@{\hspace{.3cm}}l@{\hspace{.3cm}}lll}\text{(mir${}_{M}$
4a)}\hskip 8.5359pt&t\Downarrow_{\mathtt{vsc}}\,xn_{1}\hskip
8.5359pt&\textit{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{\mathtt{vsc}}\,n^{\prime}\equiv_{M}xn_{1}^{\prime}\hfil\hskip
8.5359pt&\textit{with}~{}n_{1}~{}{\mathcal{R}}~{}n_{1}^{\prime}\\\
\text{(mir${}_{M}$ 4b)}\hskip
8.5359pt&t\Downarrow_{\mathtt{vsc}}\,\mathbb{i}n_{1}\hskip
8.5359pt&\textit{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{\mathtt{vsc}}\,n^{\prime}\equiv_{M}\mathbb{i}^{\prime}n_{1}^{\prime}\hfil\hskip
8.5359pt&\textit{with}~{}\mathbb{i}~{}{\mathcal{R}}~{}\mathbb{i}^{\prime}~{}\textit{and}~{}n_{1}~{}{\mathcal{R}}~{}n_{1}^{\prime}\\\
\text{(mir${}_{M}$ 5)}\hskip
8.5359pt&t\Downarrow_{\mathtt{vsc}}\,n_{1}[x{\shortleftarrow}i]\hskip
8.5359pt&\textit{and}\hfil\hskip
8.5359pt&t^{\prime}\Downarrow_{\mathtt{vsc}}\,n^{\prime}\equiv_{M}n_{1}^{\prime}[x{\shortleftarrow}i^{\prime}]\hfil\hskip
8.5359pt&\textit{with}~{}i~{}{\mathcal{R}}~{}i^{\prime}~{}\textit{and}~{}n_{1}~{}{\mathcal{R}}~{}n_{1}^{\prime}\end{array}$

##### Compatibility

The compatibility proof for $\precsim_{\mathtt{mir}_{M}}$ follows the same
structure of the one for $\precsim_{nai}$ (in Appendix E of the additional
material on HotCRP). At the evaluation level, we have already seen that
substitutivity holds also for the weak reduction of the VSC and with the
addition of the equivalence $\equiv_{@l}$ (Prop. 11.4). At the level of the
simulation, we need to refine the notion of Lassen closure, by adding rule
${\mathcal{L}}^{M}_{\equiv_{M}}$ accounting for mirrors.

###### Definition 11.7 (Mirrored Lassen closure).

Let the _mirrored Lassen closure_ ${{\mathcal{R}}}^{{\mathcal{L}}^{M}}$ of
${\mathcal{R}}$ be:

| $a\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,ba~{}{\mathcal{R}}~{}b$ | $x\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,x$ | $\lambda x.a\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,\lambda x.ba\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,b$ | $ap\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,bq\lx@proof@logical@and a\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,bp\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,q$
---|---|---|---
| $a[x{\shortleftarrow}p]\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,b[x{\shortleftarrow}q]{}\lx@proof@logical@and a\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,bp\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,q$ | $a\\{x{\shortleftarrow}v_{p}\\}\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,b\\{x{\shortleftarrow}v_{q}\\}{}\lx@proof@logical@and a\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,bv_{p}\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,v_{q}$ | $a\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,b\lx@proof@logical@and a^{\prime}\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}\,b^{\prime}b^{\prime}\equiv_{M}b$
---|---|---

Then the reasoning for compatibility—and in particular the coherence
properties—smoothly adapts, using the mirror properties for rule
${\mathcal{L}}^{M}_{\equiv_{M}}$ in the proof that the closure preserves
mirrored simulations. In particular, strong commutation of $\equiv_{M}$
implies that it preserves normal forms and steps, that is, the coherence
properties. Summing up, we obtain our main result.

###### Theorem 11.8 (Compatibility and soundness of
$\precsim_{\mathtt{mir}_{M}}$ and $\precsim_{\mathit{net}}$).

Let $\equiv_{M}$ be a mirror.

  1. (1)

_Redundancy of the mirrored Lassen closure_ :
$\precsim_{\mathtt{mir}_{M}}\,={\precsim_{\mathtt{mir}_{M}}}^{{\mathcal{L}}^{M}}$.

  2. (2)

MirM similarity $\precsim_{\mathtt{mir}_{M}}$ is compatible and included in
the CbV contextual preorder $\precsim_{C}^{v}$.

  3. (3)

Net similarity $\precsim_{\mathit{net}}$ is compatible and included in the CbV
contextual preorder $\precsim_{C}^{v}$.

##### Fixpoints and Benchmarks.

For any mirror $\equiv_{M}$, and in particular for $\equiv_{M}\coloneqq Id$
and $\equiv_{M}\coloneqq\equiv_{str}$, one can show that Turing’s and Curry’s
CbV fixpoint combinators are mirM bisimilar. The proof relies on exactly the
same relation that for naive bisimilarity (Prop. 6.3). Plotkin’s ${\beta_{v}}$
and VSC conversions are included in mirM similarities. Unlike naive and enf
similarities, mirM and net similarities validate $\Omega_{v}$-equivalence
$\equiv_{\Omega_{v}}$. Net and $\equiv_{M}$-mirrored bisimilarities do not
however validate $\eta_{v}$ equivalence, one has to change the case for
abstractions to accommodate it, and it does not validate CbN duplication, as
for instance $(yxx)[x{\shortleftarrow}z\mathtt{I}]$ and
$y(z\mathtt{I})(z\mathtt{I})$ are both $\rightarrow_{\mathtt{vsc}}$-normal but
not $\equiv_{str}$-equivalent.

##### Left Identity Is Not Validated By MirM

Analogously, net similarity does not validate Moggi’s $\equiv_{lid}$ rule,
because
$x[x{\shortleftarrow}y\mathtt{I}]\not\rightarrow_{\mathtt{vsc}}y\mathtt{I}$
and $x[x{\shortleftarrow}y\mathtt{I}]\not\equiv_{str}y\mathtt{I}$. Thus,
$\mathsf{enf}$ is not included in net similarity. About adding $\equiv_{lid}$,
it is easy to define a mir${}_{\equiv_{lid}}$ bisimulation, but the current
compatibility proof does not go through, as $\equiv_{lid}$ is not a mirror for
$\rightarrow_{\mathtt{vsc}}$ (in particular, it does not strongly commute with
$\rightarrow_{\mathtt{vsc}}$) and the proof technique is not able (for now) to
handle $\equiv_{lid}$ terms, as it breaks coherence for normal forms, that is,
the fact that if $n\,{{\mathcal{R}}}^{{\mathcal{L}}^{M}}t$ then $t$ is normal
(and the symmetric statement).

One could also add $\equiv_{lid}$ as a reduction step of the VSC, but then the
reduction is no longer diamond, and the diamond property (or at least the
invariance of the number of steps to normal form) is essential in the current
proof technique. It is thus unclear how to extend net similarity as to
validate $\equiv_{lid}$. Next section introduces a program equivalence
including $\simeq_{\mathit{net}}$ and validating $\equiv_{lid}$.

##### Net Bisimilarity Cannot Be Extensional

Lassen introduced an extension of enf bisimilarity validating
$\equiv_{\eta_{v}}$, enf bisimilarity up to $\eta_{v}$, at the same time that
he introduced enf bisimilarity (Lassen, 2005a). As of now, that modification
cannot be applied to net bisimilarity. We explain the problem which boils down
to, again, the fact that net does not validate the left identity law
$\equiv_{lid}$.

Let us consider that there exists a nf-bisimilarity ${\mathcal{R}}$ based on
the VSC (i.e. $t\rightarrow_{\mathtt{vsc}}t^{\prime}$ implies
$t~{}{\mathcal{R}}~{}t^{\prime}$) which is a compatible equivalence relation,
and which validates $\equiv_{\eta_{v}}$. Then, in particular, we have that
$x~{}{\mathcal{R}}~{}\lambda y.xy$, as
$\equiv_{\eta_{v}}\subseteq{\mathcal{R}}$. By compatibility (for
$C=\langle\cdot\rangle t$), $xt~{}{\mathcal{R}}~{}(\lambda y.xy)t$ and by
reduction and transitivity, $xt~{}{\mathcal{R}}~{}xy[y{\shortleftarrow}t]$.
This means that at least $(xt,xy[y{\shortleftarrow}t])$ must be included in
the relation ${\mathcal{R}}$, which is a subcase of $\equiv_{rad}$, which
itself can be implied by the $\equiv_{lid}$ rule and structural equivalence
$\equiv_{str}$. As net bisimilarity does not validate Moggi’s laws, and we do
not currently know how to include them, net bisimilarity is unable to include
$\equiv_{\eta_{v}}$.

##  12\. From Operational to Denotational Semantics: the Type Preorder

In this section, we study a behavioral preorder, the _type preorder_
$\precsim_{type}$, which is not defined as a nf-similarity, it is instead
induced by a denotational model. Namely, Ehrhard’s CbV relational model (2012)
presented as a system of multi types, also known as _non-idempotent
intersection types_. We shall prove that both Lassen’s similarity
$\precsim_{\mathit{enf}}$ and our net similarity $\precsim_{\mathit{net}}$ are
included in $\precsim_{type}$. The aim is to show that, while
$\precsim_{\mathit{enf}}$ and $\precsim_{\mathit{net}}$ are incomparable, they
can be combined in a cost-sensitive preorder (the contextual preorder combines
them but it is not cost-sensitive). We introduce the bare minimum about CbV
multi types. For more, see (Accattoli and Guerrieri, 2018, 2022).

$\begin{array}[]{ccccc}\textsc{Linear Types}&L,L^{\prime}&\Coloneqq&M\multimap
N\\\ \textsc{Multi Types}&M,N&\Coloneqq&[{L}_{1},\ldots,{L}_{n}]&n\geq
0\end{array}$
---
| $x\\!:\\![L]\vdash x\\!:\\!L$ | $\Gamma\vdash\lambda x.t\\!:\\!M\multimap N\Gamma,x\\!:\\!M\vdash t\\!:\\!N$ | $\biguplus_{i\in I}\Gamma_{i}\vdash v\\!:\\!\biguplus_{i\in I}[L_{i}]\lx@proof@logical@and(\Gamma_{i}\vdash v\\!:\\!L_{i})_{i\in I}I~{}\text{finite}$
---|---|---
| $\Gamma\uplus\Delta\vdash tu\\!:\\!N\lx@proof@logical@and\Gamma\vdash t\\!:\\![M\multimap N]\Delta\vdash u\\!:\\!M$ | $\Gamma\uplus\Delta\vdash t[x{\shortleftarrow}u]\\!:\\!N\lx@proof@logical@and\Gamma,x\\!:\\!M\vdash t\\!:\\!N\Delta\vdash u\\!:\\!M$
---|---
Figure 2. Call-by-Value Multi Type System for VSC.

##### Multi Types

Figure 2 gives the definition of multi types $M$ for the VSC, which mutually
depends on the definition of linear types $L$. Multi types are defined as
finite multi-sets $[{L}_{1},\ldots,{L}_{n}]$, which intuitively denote the
intersection $L_{1}\cap\ldots\cap L_{n}$, where the intersection $\cap$ is a
commutative, associative and non-idempotent ($A\cap A\not=A$) operator, the
neutral element of which is $[~{}]$, the empty multi set. Note that there is
no ground type, its role is played by the empty multi type $[~{}]$.

A typing judgment is of the shape $\Gamma\vdash t\\!:\\!T$ where $T$ is a
linear or a multi type and $\Gamma$ is a typing context, that is an assignment
of multi types to a finite set of variables
($\Gamma=x_{1}\\!:\\!M_{1},\ldots,x_{n}\\!:\\!M_{n}$). A typing derivation
$\pi\vartriangleright\Gamma\vdash t\\!:\\!M$ is a tree built from the
derivation rules defined in Figure 2 which ends with the typing judgment
$\Gamma\vdash t\\!:\\!M$.

##### Typing Rules

Linear types only type values, via the rules $\mathsf{ax}$ and $\lambda$. To
give a multi type to value $v$, one has to use the $\mathsf{many}$ rule,
turning an indexed family of linear types for $v$ into a multi type. Note that
any value can be typed with the empty multi type $[~{}]$. The symbol $\uplus$
is the disjoint union operator on multi sets (which corresponds to our non-
idempotent intersection on multi types).

##### Characterization of Termination

A key property of multi types is that they characterize
$\rightarrow_{\mathtt{vsc}}$ termination. The characterization is proved via
subject reduction and expansion.

###### Theorem 12.1 (Characterization of termination, (Accattoli and
Guerrieri, 2022)).

  1. (1)

_Subject reduction and expansion_ : let $t\rightarrow_{\mathtt{vsc}}u$. Then
$\Gamma\vdash t\\!:\\!M$ if and only if $\Gamma\vdash u\\!:\\!M$.

  2. (2)

$t$ is $\rightarrow_{\mathtt{vsc}}$-terminating if and only if there exists
$\Gamma$ and $M$ such that $\Gamma\vdash t\\!:\\!M$.

Since $\rightarrow_{\mathtt{vsc}}$-divergence characterizes CbV $\Omega$-terms
(Thm. 9.3), _not being typable_ with multi types characterizes it too, by the
previous theorem.

##### Multi Types Induce a Model

Multi types induce a model by interpreting a term as the set of its type
judgments. A possibly empty list of pairwise distinct variables
$\vec{x}=(x_{1},\dots,x_{n})$ is _suitable for_ $t$ if ${\tt
fv}(t)\subseteq\\{x_{1},\dots,x_{n}\\}$. If $\vec{x}=(x_{1},\dots,x_{n})$ is
suitable for $t$, the _semantics_ $\llbracket t\rrbracket_{\vec{x}}$ _of_ $t$
_for_ $\vec{x}$ is given by:

$\llbracket
t\rrbracket_{\vec{x}}\coloneqq\\{((N_{1},\dots,N_{n}),M)\mid\exists\,\Phi\vartriangleright
x_{1}\\!:\\!N_{1},\dots,x_{n}\\!:\\!N_{n}\vdash t\\!:\\!M\\}$

This is exactly Ehrhard’s CbV relational model (2012). Ehrhard considers it
with respect to Plotkin’s calculus. We do not prove that it is a model for the
VSC, because there is no formal notion of VSC model. We do have, however, that
subject reduction and expansion (Thm. 12.1.1) ensure that the interpretation
$\llbracket t\rrbracket_{\vec{x}}$ is _invariant_ by
$\rightarrow_{\mathtt{vsc}}$, and compatibility of the induced equational
theory is proved below. These properties are what the definitions of
$\lambda$-models or categorical models are meant to ensure. Moreover, the
characterization theorem (Thm. 12.1) ensures that $\llbracket
t\rrbracket_{\vec{x}}$ is adequate.

###### Corollary 12.2 ((Accattoli and Guerrieri, 2022)).

Let $t$ be a term in the VSC with $\vec{x}=(x_{1},\dots,x_{n})$ suitable for
it.

  1. (1)

_Invariance_ : if $t(\rightarrow_{\mathtt{vsc}}\cup\equiv_{str})u$ then
$\llbracket t\rrbracket_{\vec{x}}=\llbracket u\rrbracket_{\vec{x}}$.

  2. (2)

_Adequacy for_ $\rightarrow_{\mathtt{vsc}}$: $\llbracket
t\rrbracket_{\vec{x}}$ is non-empty if and only if $t$ is
$\rightarrow_{\mathtt{vsc}}$-terminating.

##### The Type Preorder

Every model $M$ induces an equational theory defined as $t=_{M}u$ if
$\llbracket t\rrbracket_{M}=\llbracket u\rrbracket_{M}$. For the multi types
model, we consider the _preorder_ induced by $\llbracket
t\rrbracket_{\vec{x}}\subseteq\llbracket t^{\prime}\rrbracket_{\vec{x}}$.

###### Definition 12.3 (Type preorder).

The type preorder $t\precsim_{type}t^{\prime}$ holds if $\Gamma\vdash
t\\!:\\!M$ implies $\Gamma\vdash t^{\prime}\\!:\\!M$.

Rephrasing the definition with respect to interpretations, we have that
$t\precsim_{type}t^{\prime}$ if $\llbracket
t\rrbracket_{\vec{x}}\subseteq\llbracket t^{\prime}\rrbracket_{\vec{x}}$ for
every list of suitable variables $\vec{x}$. By the adequacy of $\llbracket
t\rrbracket_{\vec{x}}$, it follows the adequacy of $\precsim_{type}$.
Compatibility is easily proved directly, for once, and soundness follows.

###### Proposition 12.4 (Compatibility of $\precsim_{type}$).

  1. (1)

_Compatibility_ : if $t\precsim_{type}t^{\prime}$ then $C\langle
t\rangle\precsim_{type}C\langle t^{\prime}\rangle$.

  2. (2)

_Soundness_ : if $t\precsim_{type}t^{\prime}$ then
$t\precsim_{C}^{v}t^{\prime}$.

##### Enf and Net Are Included in Type

Now, we show that $\precsim_{\mathit{enf}}$ and $\precsim_{\mathit{net}}$ are
both included in $\precsim_{type}$. For that, we prove that, if
$t\precsim_{\mathit{enf}}t^{\prime}$ or $t\precsim_{\mathit{net}}t^{\prime}$,
then any typing derivation for $t$ can be transformed in a typing derivation
for $t^{\prime}$ having the same final judgement. The next two propositions
and the associated lemma are proved by induction on the following notion: the
_size_ $|\pi|$ of a type derivation $\pi$, defined as the number of rule
occurences in $\pi$ except for rule $\mathsf{many}$.

###### Proposition 12.5.

  1. (1)

_Net simulations and type derivations_ : let ${\mathcal{R}}$ be a net
simulation. If $t~{}{\mathcal{R}}~{}t^{\prime}$ and $\pi:\Gamma\vdash
t\\!:\\!M$ then there exists a derivation $\pi^{\prime}:\Gamma\vdash
t^{\prime}\\!:\\!M$.

  2. (2)

_Net is included in Type_ : if $t\precsim_{\mathit{net}}t^{\prime}$ then
$t\precsim_{type}t^{\prime}$.

To relate $\mathsf{enf}$ similarity and typability, we need a lemma to deal
with Lassen’s stop-and-go.

###### Lemma 12.6 (Stop-and-go and type derivations).

Let $\pi\vartriangleright\Gamma\vdash{L\langle xv\rangle}\\!:\\!M$ and $z$ be
fresh. Then there exist $\pi_{L}\vartriangleright\Gamma_{L},z\\!:\\!N\vdash
L\langle z\rangle\\!:\\!M$ with $|\pi_{L}|<|\pi|$ and
$\pi_{v}\vartriangleright\Gamma_{v}\vdash v:N_{1}$ with $|\pi_{v}|<|\pi|$.

###### Proposition 12.7.

  1. (1)

_Enf simulations and type derivations_ : let ${\mathcal{R}}$ be an
$\mathsf{enf}$ simulation. If $t~{}{\mathcal{R}}~{}t^{\prime}$ and
$\pi\vartriangleright\Gamma\vdash t\\!:\\!M$ then there exists a derivation
$\pi^{\prime}\vartriangleright\Gamma\vdash t^{\prime}\\!:\\!M$.

  2. (2)

_Enf is included in Type_ : if $t\precsim_{\mathit{enf}}t^{\prime}$ then
$t\precsim_{type}t^{\prime}$.

#####  $\eta_{v}$ Equivalence

By the fact that $\mathsf{enf}$ and net similarities are incomparable follows
that they are strictly included in $\precsim_{type}$. A further gap between
the type preorder $\precsim_{type}$ and $\precsim_{\mathit{enf}}$ or
$\precsim_{\mathit{net}}$ is $\eta_{v}$ equivalence, which is included in
$\precsim_{type}$ but not in $\precsim_{\mathit{enf}}$ nor
$\precsim_{\mathit{net}}$.

###### Proposition 12.8 ($\eta_{v}$-equivalence is included in type
equivalence).

Let $x$ a variable. Then $\lambda y.xy\precsim_{type}x$ and
$x\precsim_{type}\lambda y.xy$.

##### Characterizing Type Equivalence

We conjecture that $\precsim_{type}$ is exactly the sup of the $\mathsf{enf}$
and net similarities enriched with $\eta_{v}$ equivalence, that is, that
generalizing $\precsim_{\mathit{net}}$ as to validate $\equiv_{lid}$ and
$\equiv_{\eta_{v}}$ would match $\precsim_{type}$. If the conjecture is false,
finding a nf-similarity presentation of $\precsim_{type}$—which corresponds to
describe the equational theory of CbV relational semantics—is anyway an
interesting and challenging problem.

About full abstraction with respect to CbV contextual equivalence
$\simeq_{C}^{v}$, it fails for $\simeq_{type}$, as $\simeq_{type}$ is cost-
sensitive—it does not validate CbN duplication—while $\simeq_{C}^{v}$ is cost-
insensitive.

##  13\. Conclusions

Motivated by the fact that Lassen’s enf bisimilarity
$\simeq_{\mathit{enf}}$—the normal form bisimilarity of reference in CbV—does
not identify $\Omega$-terms and commuting $\sf{let}$s, we introduced _net
bisimilarity_ $\simeq_{\mathit{net}}$, which does identify them. It turns out,
however, that $\simeq_{\mathit{net}}$ does not validate Moggi’s laws nor
$\eta_{v}$, which are instead validated by $\simeq_{\mathit{enf}}$.
Additionally, it is unclear how to extend either enf or net bisimilarity as to
catch the other one.

Such a problematic duality led us to develop a sharp analysis of CbV and of
the principles that can be validated or not by normal form bisimulations. The
analysis shows that the semantic landscape of CbV is considerably richer and
more sophisticated than the CbN one.

Concretely, our analysis contributed two further equivalences. First, a naive
bisimilarity $\simeq_{nai}$, that mainly provides a better understanding of
Lassen’s tricky definition of enf simulations. Second, the type equivalence
$\simeq_{type}$ induced by Ehrhard’s multi types, which subsumes both enf and
net bisimilarity, and includes $\eta_{v}$-equivalence, while retaining their
cost-sensitive aspect. In practice, $\simeq_{type}$ is not really usable for
comparing programs, but it provides a sharp theoretical tool.

##### Future Work

Type equivalence suggests that it could be possible to find a normal form
bisimilarity merging the enf and net ones. We are actively working on this
challenging problem. A related question is finding an axiomatization of
$\simeq_{type}$, for which some sort of separation theorem should be
developed. We would also like to investigate how net bisimilarity
$\simeq_{\mathit{net}}$ relates to the topics connected to
$\simeq_{\mathit{enf}}$, such as game semantics (Jaber and Murawski, 2021),
extensions with effects (Dal Lago and Gavazzo, 2019; Biernacki et al., 2019a,
2020), and the $\pi$-calculus (Durier et al., 2022).

## References

  * (1)
  * Abramsky (1990) Samson Abramsky. 1990\.  _The Lazy Lambda Calculus_.  Addison-Wesley Longman Publishing Co., Inc., USA, 65–116.
  * Accattoli (2015) Beniamino Accattoli. 2015\.  Proof nets and the call-by-value $\lambda$-calculus.  _Theor. Comput. Sci._ 606 (2015), 2–24.  https://doi.org/10.1016/j.tcs.2015.08.006
  * 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, Rome, Italy, June 29 - July 2, 2021_. IEEE, 1–14.  https://doi.org/10.1109/LICS52264.2021.9470630
  * 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)_ , Atsushi Igarashi (Ed.), Vol. 10017. 206–226.  https://doi.org/10.1007/978-3-319-47958-3_12
  * Accattoli and Guerrieri (2018) Beniamino Accattoli and Giulio Guerrieri. 2018.  Types of Fireballs. In _Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings_ _(Lecture Notes in Computer Science)_ , Sukyoung Ryu (Ed.), Vol. 11275. Springer, 45–66.  https://doi.org/10.1007/978-3-030-02768-1_3
  * Accattoli and Guerrieri (2022) Beniamino Accattoli and Giulio Guerrieri. 2022.  The theory of call-by-value solvability.  _Proc. ACM Program. Lang._ 6, ICFP (2022), 855–885.  https://doi.org/10.1145/3547652
  * Accattoli and Paolini (2012) Beniamino Accattoli and Luca Paolini. 2012.  Call-by-Value Solvability, Revisited. In _Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings_ _(Lecture Notes in Computer Science)_ , Tom Schrijvers and Peter Thiemann (Eds.), Vol. 7294. Springer, 4–16.  https://doi.org/10.1007/978-3-642-29822-6_4
  * Arrial et al. (2023) Victor Arrial, Giulio Guerrieri, and Delia Kesner. 2023\.  Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework.  _Proc. ACM Program. Lang._ 7, POPL (2023), 1483–1513.  https://doi.org/10.1145/3571244
  * Barendregt (1971) Hendrik Pieter Barendregt. 1971\.  _Some extensional term models for combinatory logics and $\lambda$-calculi_.  Ph.D. Dissertation. Univ. Utrecht.
  * Barendregt (1977) Hendrik Pieter 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) Hendrik Pieter Barendregt. 1984\.  _The Lambda Calculus – Its Syntax and Semantics_. Studies in logic and the foundations of mathematics, Vol. 103.  North-Holland.
  * Biernacki and Lenglet (2012) Dariusz Biernacki and Sergueï Lenglet. 2012.  Normal Form Bisimulations for Delimited-Control Operators. In _Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings_ _(Lecture Notes in Computer Science)_ , Tom Schrijvers and Peter Thiemann (Eds.), Vol. 7294. Springer, 47–61.  https://doi.org/10.1007/978-3-642-29822-6_7
  * Biernacki et al. (2019a) Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2019a.  A Complete Normal-Form Bisimilarity for State. In _Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings_ _(Lecture Notes in Computer Science)_ , Mikolaj Bojanczyk and Alex Simpson (Eds.), Vol. 11425. Springer, 98–114.  https://doi.org/10.1007/978-3-030-17127-8_6
  * Biernacki et al. (2019b) Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2019b.  Proving Soundness of Extensional Normal-Form Bisimilarities.  _Log. Methods Comput. Sci._ 15, 1 (2019).  https://doi.org/10.23638/LMCS-15(1:31)2019
  * Biernacki et al. (2020) Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2020.  A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. In _5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)_ _(Leibniz International Proceedings in Informatics (LIPIcs))_ , Zena M. Ariola (Ed.), Vol. 167. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 7:1–7:22.  https://doi.org/10.4230/LIPIcs.FSCD.2020.7
  * 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, Akita, Japan, September 14-16, 2020, Proceedings_ _(Lecture Notes in Computer Science)_ , Keisuke Nakano and Konstantinos Sagonas (Eds.), Vol. 12073. Springer, 13–32.  https://doi.org/10.1007/978-3-030-59025-3_2
  * 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, Grenoble, France, April 5-13, 2014, Proceedings_ _(Lecture Notes in Computer Science)_ , Anca Muscholl (Ed.), Vol. 8412. Springer, 103–118.  https://doi.org/10.1007/978-3-642-54830-7_7