Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus

TL;DR

This paper explores a semantic approach to measure execution time in call-by-value lambda calculus using a linear logic-based model, revealing limitations and proposing future refinements for accurate timing analysis.

Contribution

It introduces a semantic framework for estimating execution time in call-by-value lambda calculus and highlights the challenges in transferring quantitative info from derivations to types.

Findings

Interpretation non-emptiness characterizes normalizability.

Type derivation size correlates with execution time.

Quantitative info does not naturally lift to types.

Abstract

We investigate the possibility of a semantic account of the execution time (i.e. the number of beta-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value lambda-calculus. For this purpose, we use a linear logic based denotational model that can be seen as a non-idempotent intersection type system: relational semantics. Our investigation is inspired by similar ones for linear logic proof-nets and untyped call-by-name lambda-calculus. We first prove a qualitative result: a (possibly open) term is normalizable for weak reduction (which does not reduce under abstractions) if and only if its interpretation is not empty. We then show that the size of type derivations can be used to measure the execution time. Finally, we show that, differently from the case of linear logic and call-by-name lambda-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

Equations

$$t$$

$$t,u,s$$

$$v$$

$$C$$

$$B$$

$$(\lambda x.t)v$$

$${\mapsto }_{\sigma }:={\mapsto }_{{\sigma }_1}\cup {\mapsto }_{{\sigma }_3}{\mapsto }_{\mathsf{sh}}:={\mapsto }_{{\beta }_v}\cup {\mapsto }_{\sigma }$$

$$\mathsf{r}\text{-reduction:}$$

$${\mathsf{r}}^{♭}\text{-reduction:}$$

$$a$$

$$M,N$$

$${\pi }_{\_}II=\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}73.0pt\text{vbox}\text{vbox}\text{vbox}\text{vskip}0.47777pt\text{nointerlineskip}\text{lower}-0.2ptto58.87463pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}1.52222pt\mathsf{ax}\text{vskip}0.47778pt\text{nointerlineskip}x:[]⊢x:[]\text{vskip}-0.57779pt\text{nointerlineskip}\text{lower}-0.2ptto65.40248pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.57777pt\lambda \text{vskip}-0.57777pt\text{nointerlineskip}⊢I:[[]⊸[]]\text{vbox}\text{vskip}-0.57779pt\text{nointerlineskip}\text{lower}-0.2ptto35.95815pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.57777pt\lambda \text{vskip}-0.57777pt\text{nointerlineskip}⊢I:[]\text{vskip}-0.57779pt\text{nointerlineskip}\text{lower}-0.2ptto123.77272pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.57777pt@\text{vskip}-0.57777pt\text{nointerlineskip}⊢II:[]\text{ignorespaces}$$

$${\pi }_{\_}n=\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}50.5pt\text{vbox}\text{vbox}⋮{\pi }_{\_}II\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.5pt\text{vbox}\text{vskip}1.0pt\text{lower}-0.5pt\text{vskip}2.0pt\text{nointerlineskip}y:[]⊢II:[]\stackrel{k}{\dots }\text{vbox}⋮{\pi }_{\_}II\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.5pt\text{vbox}\text{vskip}1.0pt\text{lower}-0.5pt\text{vskip}2.0pt\text{nointerlineskip}y:[]⊢II:[]\text{vskip}-0.57779pt\text{nointerlineskip}\text{lower}-0.2ptto176.06192pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.57777pt\lambda \text{vskip}-0.57777pt\text{nointerlineskip}⊢\lambda y.II:[[]⊸[],\stackrel{k}{\dots },[]⊸[]]\text{ignorespaces}$$

$$[[t{]]}_{\vec{x}}=\{((P_{\_}1,\dots ,P_{\_}k),Q)\mid \exists \pi ⊳x_{\_}1:P_{\_}1,\dots ,x_{\_}k:P_{\_}k⊢t:Q\}.$$

$${\mathcal{U}}_{\_}0$$

$$|v{|}_{♭}$$

$${\mathrm{leng}}_{{\beta }_v^{♭}}(d)=|\pi |-|t_{\_}0{|}_{♭}=|\pi |-|{\pi }_{\_}0|.$$

$${\mathrm{leng}}_{{\beta }_v^{♭}}(t)=\{\begin{array}{ll}{\mathrm{leng}}_{{\beta }_v^{♭}}(d)& \text{if there is a sh♭-normalizing reduction sequence d from t;}\\ \infty & \text{otherwise.}\end{array}$$

$$\pi :=\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}71.5pt\text{vbox}\text{vbox}\text{vbox}\text{vskip}0.47777pt\text{nointerlineskip}\text{lower}-0.2ptto53.7875pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}1.52222pt\mathsf{ax}\text{vskip}0.47778pt\text{nointerlineskip}x:[]⊢x:[]\text{vskip}-0.57779pt\text{nointerlineskip}\text{lower}-0.2ptto70.53755pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.57777pt\lambda \text{vskip}-0.57777pt\text{nointerlineskip}⊢\lambda x.x:[[]⊸[]]\text{vbox}\text{vbox}\text{vskip}0.47777pt\text{nointerlineskip}\text{lower}-0.2ptto106.78757pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}1.52222pt\mathsf{ax}\text{vskip}0.47778pt\text{nointerlineskip}x:[[]⊸[]]⊢x:[[]⊸[]]\text{vbox}\text{vskip}0.47777pt\text{nointerlineskip}\text{lower}-0.2ptto53.7875pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}1.52222pt\mathsf{ax}\text{vskip}0.47778pt\text{nointerlineskip}x:[]⊢x:[]\text{vskip}-0.57779pt\text{nointerlineskip}\text{lower}-0.2ptto186.2511pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.57777pt@\text{vskip}-0.57777pt\text{nointerlineskip}y:[[]⊸[]]⊢yy:[]\text{vskip}-0.57779pt\text{nointerlineskip}\text{lower}-0.2ptto227.88673pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.57777pt@\text{vskip}-0.57777pt\text{nointerlineskip}y:[[]⊸[]]⊢(\lambda x.x)(yy):[]\text{ignorespaces}.$$

Full text

1 Introduction

Type systems enforce properties of programs, such as termination or deadlock-freedom. The guarantee provided by most type systems for the $\lambda$-calculus is termination.

Intersection types have been introduced as a way of extending simple types for the $\lambda$-calculus to “finite polymorphism”, by adding a new type constructor $\cap$ and new typing rules governing it. Contrary to simple types, intersection types provide a sound and complete characterization of termination: not only typed programs terminate, but all terminating programs are typable as well (see [20, 21, 43, 37] where different intersection type systems characterize different notions of normalization). Intersection types are idempotent, that is, they verify the equation $A\cap A=A$. This corresponds to an interpretation of a typed term $t\colon A\cap B$ as “$t$ can be used both as data of type $A$ and as data of type $B$”.

More recently [25, 36, 39, 16, 17] (a survey can be found in [14]), non-idempotent variants of intersection types have been introduced: they are obtained by dropping the equation $A\cap A=A$. In a non-idempotent setting, the meaning of the typed term $t\colon A\cap A\cap B$ is refined as “$t$ can be used twice as data of type $A$ and once as data of type $B$”. This could give to programmers a way to keep control on the performance of their code and to count resource consumption. Finite multisets are the natural setting to interpret the associative, commutative and non-idempotent connective $\cap$: if $A$ and $B$ are non-idempotent intersection types, the multiset $[A,A,B]$ represents the non-idempotent intersection type $A\cap A\cap B$.

Non-idempotent intersection types have two main features, both enlightened by de Carvalho [16, 17]:

Bounds on the execution time: they go beyond simply qualitative characterisations of termination, as type derivations provide quantitative bounds on the execution time (i.e. on the number of $\beta$-steps to reach the $\beta$-normal form). Therefore, non-idempotent intersection types give intensional insights on programs, and seem to provide a tool to reason about complexity of programs. The approach is defining a measure for type derivations and showing that the measure gives (a bound to) the length of the evaluation of typed terms. 2. 2.

Linear logic interpretation: non-idempotent intersection types are deeply linked to linear logic ($\mathsf{LL}$) [26]. Relational semantics [27, 12] — the category $\mathbf{Rel}$ of sets and relations endowed with the comonad $\oc$ of finite multisets — is a sort of “canonical” denotational model of $\mathsf{LL}$; the Kleisli category $\mathbf{Rel}_{\_}\oc$ of the comonad $\oc$ is a CCC and then provides a denotational model of the ordinary (i.e. call-by-name) $\lambda$-calculus. Non-idempotent intersection types can be seen as a syntactic presentation of $\mathbf{Rel}_{\_}\oc$: the semantics of a term $t$ is the set of conclusions of all type derivations of $t$.

These two facts together have a potential, fascinating consequence: denotational semantics may provide abstract tools for complexity analysis, that are theoretically solid, being grounded on $\mathsf{LL}$.

Starting from [16, 17], research on relational semantics/non-idempotent intersection types has proliferated: various works in the literature explore their power in bounding the execution time or in characterizing normalization [18, 13, 11, 34, 10, 19, 41, 35, 14, 38, 4]. All these works study relational semantics/non-idempotent intersection types either in $\mathsf{LL}$ proof-nets (the graphical representation of proofs in $\mathsf{LL}$), or in some variant of ordinary (i.e. call-by-name) $\lambda$-calculus. In the second case, the construction of the relational model $\mathbf{Rel}_{\_}\oc$ sketched above essentially relies on Girard’s call-by-name translation $(\cdot)^{n}$ of intuitionistic logic into $\mathsf{LL}$, which decomposes the intuitionistic arrow as $(A\Rightarrow B)^{n}=\oc A^{n}\multimap B^{n}$.

Ehrhard [23] showed that the relational semantics $\mathbf{Rel}$ of $\mathsf{LL}$ induces also a denotational model for the call-by-value $\lambda$-calculus111In call-by-value evaluation $\rightarrow_{{\beta_{v}}}$, function’s arguments are evaluated before being passed to the function, so that $\beta$-redexes can fire only when their arguments are values, i.e. abstractions or variables. The idea is that only values can be erased or duplicated. Call-by-value evaluation is the most common parameter passing mechanism used by programming languages. that can still be viewed as a non-idempotent intersection type system.

The syntactic counterpart of this construction is Girard’s (“boring”) call-by-value translation $(\cdot)^{v}$ of intuitionistic logic into $\mathsf{LL}$ [26], which decomposes the intuitionistic arrow as $(A\Rightarrow B)^{v}=\oc(A^{v}\multimap B^{v})$. Just few works have started the study of relational semantics/non-idempotent intersection types in a call-by-value setting [23, 22, 15, 24], and no one investigates their bounding power on the execution time in such a framework. Our paper aims to fill this gap and study the information enclosed in relational semantics/non-idempotent intersection types concerning the execution time in the call-by-value $\lambda$-calculus.

A difficulty arises immediately in the qualitative characterization of call-by-value normalization via the relational model. One would expect that the semantics of a term $t$ is non-empty if and only if $t$ is (strongly) normalizable for (some restriction of) the call-by-value evaluation $\rightarrow_{{\beta_{v}}}$, but it is impossible to get this result in Plotkin’s original call-by-value $\lambda$-calculus $\lambda_{\_}v$ [42]. Indeed, the terms $t$ and $u$ below are ${\beta_{v}}$-normal but their semantics in the relational model are empty:

[TABLE]

Actually, $t$ and $u$ should behave like the famous divergent term $\Delta\Delta$, since in $\lambda_{\_}v$ they are observationally equivalent to $\Delta\Delta$ with respect all closing contexts and have the same semantics as $\Delta\Delta$ in all non-trivial denotational models of Plotkin’s $\lambda_{\_}v$.

The reason of this mismatching is that in $\lambda_{\_}v$ there are stuck $\beta$-redexes such as $(\lambda y.\Delta)(zI)$ in Eq. (1), i.e. $\beta$-redexes that ${\beta_{v}}$-reduction will never fire because their argument is normal but not a value (nor will it ever become one). The real problem with stuck $\beta$-redexes is that they may prevent the creation of other $\beta_{\_}v$-redexes, providing “premature” $\beta_{\_}v$-normal forms like $t$ and $u$ in Eq. (1). The issue affects termination and thus can impact on the study of observational equivalence and other operational properties in $\lambda_{\_}v$.

In a call-by-value setting, the issue of stuck $\beta$-redexes and then of premature $\beta_{\_}v$-normal forms arises only with open terms (in particular, when the reduction under abstractions is allowed, since it forces to deal with “locally open” terms). Even if to model functional programming languages with a call-by-value parameter passing, such as OCaml, it is usually enough to just consider closed terms and weak evaluation (i.e. not reducing under abstractions: function bodies are evaluated only when all parameters are supplied), the importance to consider open terms in a call-by-value setting can be found, for example, in partial evaluation (which evaluates a function when not all parameters are supplied, see [33]), in the theory of proof assistants such as Coq (in particular, for type checking in a system based on dependent types, see [28]), or to reason about (denotational or operational) equivalences of terms in $\lambda_{\_}v$ that are congruences, or about other theoretical properties of $\lambda_{\_}v$ such as separability or solvability [40, 46, 8, 15].

To overcome the issue of stuck $\beta$-redexes, we study relational semantics/non-idempotent intersection types in the shuffling calculus $\lambda_{\mathsf{sh}}$, a conservative extension of Plotkin’s $\lambda_{\_}{v}$ proposed in [15] and further studied in [29, 31, 5, 32]. It keeps the same term syntax as $\lambda_{\_}{v}$ and adds to ${\beta_{v}}$-reduction two commutation rules, $\sigma_{\_}{1}$ and $\sigma_{\_}{3}$, which “shuffle” constructors in order to move stuck $\beta$-redexes: they unblock $\beta_{\_}v$-redexes that are hidden by the “hyper-sequential structure” of terms. These commutation rules (referred also as $\sigma$-reduction rules) are similar to Regnier’s $\sigma$-rules for the call-by-name $\lambda$-calculus [44, 45] and are inspired by the aforementioned $(\cdot)^{v}$ translation of the $\lambda$-calculus into $\mathsf{LL}$ proof-nets.

Following the same approach used in [17] for the call-by-name $\lambda$-calculus and in [18] for $\mathsf{LL}$ proof-nets, we prove that in the shuffling calculus $\lambda_{\mathsf{sh}}$:

(qualitative result) relational semantics is adequate for $\lambda_{\mathsf{sh}}$, i.e. a possibly open term is normalizable for weak reduction (not reducing under $\lambda$’s) if and only if its interpretation in relational semantics is not empty (Thm. 16); this result was already proven in [15] using different techniques; 2. 2.

(quantiative result) the size of type derivations can be used to measure the execution time, i.e. the number of ${\beta_{v}}$-steps (and not $\sigma$-steps) to reach the normal form of the weak reduction (Prop. 21).

Finally, we show that, differently from the case of $\mathsf{LL}$ and call-by-name $\lambda$-calculus, we are not able to lift the quantitative information enclosed in type derivations to types (i.e. to the interpretation of terms) following the same technique used in [17, 18], as our Ex. 28 shows. In order to get a genuine semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

Even if our main goal has not yet been achieved, this investigation led to new interesting results:

all normalizing weak reduction sequences (if any) in $\lambda_{\mathsf{sh}}$ from a given term have the same number of ${\beta_{v}}$-steps (Cor. 22); this is not obvious, as we shall explain in Ex. 23; 2. 2.

terms whose weak reduction in $\lambda_{\mathsf{sh}}$ ends in a value has an elegant semantic characterization (Prop. 18), and the number of ${\beta_{v}}$-steps needed to reach their normal form can be computed in a simple way from a specific type derivation (Thm. 24). 3. 3.

all our qualitative and quantitative results for $\lambda_{\mathsf{sh}}$ are still valid in Plotkin’s $\lambda_{\_}v$ restricted to closed terms (which models functional programming languages), see Thm. 25, Cor. 26 and Thm. 27.

Proofs are omitted. They can be found in [30], the extended version of this paper.

1.1 Preliminaries and notations

The set of $\lambda$-terms is denoted by $\Lambda$. We set $I\coloneqq\lambda x.x$ and $\Delta\coloneqq\lambda x.xx$. Let $\rightarrow_{\mathsf{r}}\,\subseteq\Lambda\times\Lambda$.

• •

The reflexive-transitive closure of $\rightarrow_{\mathsf{r}}$ is denoted by $\rightarrow_{\mathsf{r}}^{*}$. The $\mathsf{r}$-equivalence $\simeq_{\_}\mathsf{r}$ is the reflexive-transitive and symmetric closure of $\to_{\_}\mathsf{r}$.

• •

Let $t$ be a term: $t$ is $\mathsf{r}$-normal if there is no term $u$ such that $t\to_{\_}\mathsf{r}u$; $t$ is $\mathsf{r}$-normalizable if there is a $\mathsf{r}$-normal term $u$ such that $t\to_{\_}\mathsf{r}^{*}u$, and we then say that $u$ is a $\mathsf{r}$-normal form of $t$; $t$ is strongly $\mathsf{r}$-normalizable if there is no infinite sequence $(t_{\_}i)_{\_}{i\in\mathbb{N}}$ of terms such that $t=t_{\_}0$ and $t_{\_}i\to_{\_}\mathsf{r}t_{\_}{i+1}$ for all $i\in\mathbb{N}$. Finally, $\to_{\_}\mathsf{r}$ is strongly normalizing if every $u\in\Lambda$ is strongly $\mathsf{r}$-normalizable.

• •

$\rightarrow_{\mathsf{r}}$ is confluent if ${\,}_{\mathsf{r}}^{*}\!\!\leftarrow\cdot\!\rightarrow_{\mathsf{r}}^{*}\ \subseteq\ \rightarrow_{\mathsf{r}}^{*}\!\cdot{\,}_{\mathsf{r}}^{*}\!\!\leftarrow$. From confluence it follows that: $t\simeq_{\_}{\mathsf{r}}u$ iff $t\to_{\_}\mathsf{r}^{*}s\,\,{}_{\_}\mathsf{r}^{*}\!\!\!\leftarrow u$ for some term $s$; and any $\mathsf{r}$-normalizable term has a unique $\mathsf{r}$-normal form.

2 The shuffling calculus

In this section we introduce the shuffling calculus $\lambda_{\mathsf{sh}}$, namely the call-by-value $\lambda$-calculus defined in [15] and further studied in [29, 31, 5, 32]: it adds two commutation rules — the $\sigma_{\_}1$- and $\sigma_{\_}3$-reductions — to Plotkin’s pure (i.e. without constants) call-by-value $\lambda$-calculus $\lambda_{\_}v$ [42]. The syntax for terms of $\lambda_{\mathsf{sh}}$ is the same as Plotkin’s $\lambda_{\_}v$ and then the same as the ordinary (i.e. call-by-name) $\lambda$-calculus, see Fig. 1.

Clearly, $\Lambda_{v}\subsetneq\Lambda$. All terms are considered up to $\alpha$-conversion (i.e. renaming of bound variables). The set of free variables of a term $t$ is denoted by $\mathsf{fv}(t)$: $t$ is open if $\mathsf{fv}(t)\neq\emptyset$, closed otherwise. Given $v\in\Lambda_{v}$, $t\{v/x\}$ denotes the term obtained by the capture-avoiding substitution of $v$ for each free occurrence of $x$ in the term $t$. Note that values are closed under substitution: if $v,v^{\prime}\in\Lambda_{\_}v$ then $v\{v^{\prime}/x\}\in\Lambda_{v}$.

One-hole contexts $C$ are defined as usual, see Fig. 1. We use $C\langle t\rangle$ for the term obtained by the capture-allowing substitution of the term $t$ for the hole $\langle\cdot\rangle$ in the context $C$. In Fig. 1 we define also a special kind of contexts, balanced contexts $B$.

Reductions in the shuffling calculus are defined in Fig. 1 as follows: given a root-step rule $\mapsto_{\mathsf{r}}\,\subseteq\Lambda\times\Lambda$, we define the $\mathsf{r}$-reduction $\rightarrow_{\mathsf{r}}$ (resp. ${\mathsf{r}}^{\flat\!}$-reduction $\rightarrow_{{\mathsf{r}}^{\flat\!}}$) as the closure of $\mapsto_{\mathsf{r}}$ under contexts (resp. balanced contexts). The ${\mathsf{r}}^{\flat\!}$-reduction is non-deterministic and — because of balanced contexts — can reduce under abstractions, but it is “morally” weak: it reduces under a $\lambda$ only when the $\lambda$ is applied to an argument. Clearly, $\rightarrow_{{\mathsf{sh}}^{\flat\!}}\,\subsetneq\,\rightarrow_{\mathsf{sh}}$ since $\rightarrow_{\mathsf{sh}}$ can freely reduce under $\lambda$’s.

The root-steps used in the shuffling calculus are $\mapsto_{{\beta_{v}}}$ (the reduction rule in Plotkin’s $\lambda_{\_}v$), the commutation rules $\mapsto_{\sigma_{\_}1}$ and $\mapsto_{\sigma_{\_}3}$, and $\mapsto_{\sigma}\,\coloneqq\ \mapsto_{\sigma_{\_}1}\!\cup\mapsto_{\sigma_{\_}3}$ and $\mapsto_{\mathsf{sh}}\,\coloneqq\ \mapsto_{\beta_{\_}v}\!\cup\mapsto_{\sigma}$. The side conditions for $\mapsto_{\sigma_{\_}1}$ and $\mapsto_{\sigma_{\_}3}$ in Fig. 1 can be always fulfilled by $\alpha$-renaming. For any $\mathsf{r}\in\{\beta_{\_}v,\sigma_{\_}1,\sigma_{\_}3,\sigma,\mathsf{sh}\}$, if $t\mapsto_{\mathsf{r}}t^{\prime}$ then $t$ is a $\mathsf{r}$-redex and $t^{\prime}$ is its $\mathsf{r}$-contractum. A term of the shape $(\lambda x.{t})u$ is a $\beta$-redex. Clearly, any ${\beta_{v}}$-redex is a $\beta$-redex but the converse does not hold: $(\lambda x.{z})(yI)$ is a $\beta$-redex but not a ${\beta_{v}}$-redex. Redexes of different kind may overlap: for instance, the term $\Delta I\Delta$ is a $\sigma_{\_}1$-redex and contains the $\beta_{\_}v$-redex $\Delta I$; the term $\Delta(I\Delta)(xI)$ is a $\sigma_{\_}1$-redex and contains the $\sigma_{\_}3$-redex $\Delta(I\Delta)$, which contains in turn the $\beta_{\_}v$-redex $I\Delta$.

From definitions in Fig. 1 it follows that $\rightarrow_{\mathsf{sh}}\,=\,\rightarrow_{{\beta_{v}}}\!\cup\rightarrow_{\sigma}$ and $\rightarrow_{\sigma}\,=\,\rightarrow_{\sigma_{\_}1}\!\cup\rightarrow_{\sigma_{\_}3}$, as well as $\rightarrow_{{\mathsf{sh}}^{\flat\!}}\,=\,\rightarrow_{{{\beta}^{\flat\!}_{v}}}\!\cup\rightarrow_{{\sigma}^{\flat\!}}$ and $\rightarrow_{{\sigma}^{\flat\!}}\,=\,\rightarrow_{{\sigma}^{\flat\!}_{1}}\!\cup\rightarrow_{{\sigma}^{\flat\!}_{3}}$. The shuffling (resp. balanced shuffling) calculus $\lambda_{\mathsf{sh}}$ (resp. $\lambda_{\mathsf{sh}}^{\flat\!}$) is the set $\Lambda$ of terms endowed with the reduction $\to_{\_}{\mathsf{sh}}$ (resp. $\rightarrow_{{\mathsf{sh}}^{\flat\!}}$). The set $\Lambda$ endowed with the reduction $\to_{\_}{\beta_{\_}v}$ is Plotkin’s pure call-by-value $\lambda$-calculus $\lambda_{\_}v$ [42], a sub-calculus of $\lambda_{\mathsf{sh}}$.

Proposition 1** (Basic properties of reductions, [42, 15]).**

The $\sigma$- and ${\sigma}^{\flat\!}$-reductions are confluent and strongly normalizing. The ${\beta_{v}}$-, ${{\beta}^{\flat\!}_{v}}$-, $\mathsf{sh}$- and ${\mathsf{sh}}^{\flat\!}$-reductions are confluent.

Example 2**.**

Recall the terms $t$ and $u$ in Eq. (1): $t=\!(\lambda y.\Delta)(xI)\Delta\!\rightarrow_{{\sigma}^{\flat\!}_{1}}\!(\lambda y.\Delta\Delta)(xI)\!\rightarrow_{{{\beta}^{\flat\!}_{v}}}\!(\lambda y.\Delta\Delta)(xI)\allowbreak\rightarrow_{{{\beta}^{\flat\!}_{v}}}\!\dots$ and $u=\Delta((\lambda y.\Delta)(xI))\!\rightarrow_{{\sigma}^{\flat\!}_{3}}\!(\lambda y.\Delta\Delta)(xI)\!\rightarrow_{{{\beta}^{\flat\!}_{v}}}\!(\lambda y.\Delta\Delta)(xI)\!\rightarrow_{{{\beta}^{\flat\!}_{v}}}\!\dots$ are the only possible $\mathsf{sh}$-reduction paths from $t$ and $u$ respectively: $t$ and $u$ are not $\mathsf{sh}$-normalizable and $t\simeq_{\mathsf{sh}}u$. But $t$ and $u$ are ${\beta_{v}}$-normal ($(\lambda y.\Delta)(xI)$ is a stuck $\beta$-redex) and different, so $t\not\simeq_{\_}{{\beta_{v}}}u$ by confluence of $\to_{\_}{{\beta_{v}}}$ (Prop. 1). Thus, $\simeq_{\_}{{\beta_{v}}}\,\subsetneq\,\simeq_{\mathsf{sh}}$.

Example 2 shows how $\sigma$-reduction shuffles constructors and moves stuck $\beta$-redex in order to unblock $\beta_{\_}v$-redexes which are hidden by the “hyper-sequential structure” of terms, avoiding “premature” normal forms. An alternative approach to circumvent the issue of stuck $\beta$-redexes is given by $\lambda_{\_}\mathsf{vsub}$, the call-by-value $\lambda$-calculus with explicit substitutions introduced in [8], where hidden $\beta_{\_}v$-redexes are reduced using rules acting at a distance. In [5] it has been shown that $\lambda_{\_}\mathsf{vsub}$ and $\lambda_{\mathsf{sh}}$ can be embedded in each other preserving termination and divergence. Interestingly, both calculi are inspired by an analysis of Girard’s “boring” call-by-value translation of $\lambda$-terms into linear logic proof-nets [26, 2] according to the linear recursive type $o=\oc o\multimap\oc o$, or equivalently $o=\oc(o\multimap o)$. In this translation, $\mathsf{sh}$-reduction corresponds to cut-elimination, more precisely ${\beta_{v}}$-steps (resp. $\sigma$-steps) correspond to exponential (resp. multiplicative) cut-elimination steps; ${\mathsf{sh}}^{\flat\!}$-reduction corresponds to cut-elimination at depth [math].

Consider the two subsets of terms defined by mutual induction (notice that $\Lambda_{a}\subsetneq\Lambda_{n}\supsetneq\Lambda_{v}$):

[TABLE]

Any $t\in\Lambda_{a}$ is neither a value nor a $\beta$-redex, but an open applicative term with a free “head variable”.

Proposition 3** (Syntactic characterization on ${\mathsf{sh}}^{\flat\!}$-normal forms).**

Let $t$ be a term:

• •

$t$* is ${\mathsf{sh}}^{\flat\!}$-normal iff $t\in\Lambda_{n}$;*

• •

$t$* is ${\mathsf{sh}}^{\flat\!}$-normal and is neither a value nor a $\beta$-redex iff $t\in\Lambda_{a}$.*

Stuck $\beta$-redexes correspond to ${\mathsf{sh}}^{\flat\!}$-normal forms of the shape $(\lambda x.{n})a$. As a consequence of Prop. 3, the behaviour of closed terms with respect to ${\mathsf{sh}}^{\flat\!}$-reduction (resp. ${{\beta}^{\flat\!}_{v}}$-reduction) is quite simple: either they diverge or they ${\mathsf{sh}}^{\flat\!}$-normalize (resp. ${{\beta}^{\flat\!}_{v}}$-normalize) to a closed value. Indeed:

Corollary 4** (Syntactic characterization of closed ${\mathsf{sh}}^{\flat\!}$- and ${{\beta}^{\flat\!}_{v}}$-normal forms).**

Let $t$ be a closed term: $t$ is ${\mathsf{sh}}^{\flat\!}$-normal iff $t$ is ${{\beta}^{\flat\!}_{v}}$-normal iff $t$ is a value iff $t=\lambda x.{u}$ for some term $u$ with $\mathsf{fv}(u)\subseteq\{x\}$.

3 A non-idempotent intersection type system

We recall the non-idempotent intersection type system introduced by Ehrhard [23] (nothing but the call-by-value version of de Carvalho’s system $\mathsf{R}$ [16, 17]). We use it to characterize the (strong) normalizable terms for the reduction $\rightarrow_{{\mathsf{sh}}^{\flat\!}}$. Types are positive or negative, defined by mutual induction as follows:

[TABLE]

where $[N_{\_}1,\dots,N_{\_}n]$ is a (possibly empty) finite multiset of negative types; in particular the empty multiset $[\,]$ (obtained for $n=0$) is the only atomic (positive) type. A positive type $[N_{\_}1,\dots,N_{\_}n]$ has to be intended as a conjunction $N_{\_}1\land\dots\land N_{\_}n$ of negative types $N_{\_}1,\dots,N_{\_}n$, for a commutative and associative conjunction connective $\land$ that is not idempotent and whose neutral element is $[\,]$.

The derivation rules for the non-idempotent intersection type system are in Fig. 2. In this typing system, judgments have the shape $\Gamma\vdash t:P$ where $t$ is a term, $P$ is a positive type and $\Gamma$ is an environment (i.e. a total function from variables to positive types whose domain $\mathsf{dom}(\Gamma)=\{x\mid\Gamma(x)\neq[\,]\}$ is finite). The sum of environments $\Gamma\uplus\Delta$ is defined pointwise via multiset sum: $(\Gamma\uplus\Delta)(x)=\Gamma(x)\uplus\Delta(x)$. An environment $\Gamma$ such that $\mathsf{dom}(\Gamma)\subseteq\{x_{\_}1,\dots,x_{\_}n\}$ with $x_{\_}i\neq x_{\_}j$ and $\Gamma(x_{\_}i)=P_{\_}i$ for all $1\leq i\neq j\leq k$ is often written as $\Gamma=x_{\_}1\colon\!P_{\_}1,\dots,x_{\_}n\colon\!P_{\_}k$. In particular, $\Gamma$ and $\Gamma,x\colon\![\,]$ (where $x\notin\mathsf{dom}(\Gamma)$) are the same environment; and $\vdash t\colon\!P$ stands for the judgment $\Gamma\vdash t\colon\!P$ where $\Gamma$ is the empty environment, i.e. $\mathsf{dom}(\Gamma)=\emptyset$ (that is, $\Gamma(x)=[\,]$ for any variable $x$). Note that the sum of environments $\uplus$ is commutative, associative and its neutral element is the empty environment: given an environment $\Gamma$, one has $\Gamma\uplus\Delta=\Gamma$ iff $\mathsf{dom}(\Delta)=\emptyset$. The notation $\pi\vartriangleright\Gamma\vdash t\colon\!P$ means that $\pi$ is a derivation with conclusion the judgment $\Gamma\vdash t\colon P$. We write $\pi\vartriangleright t$ if $\pi$ is such that $\pi\vartriangleright\Gamma\vdash t\colon\!P$ for some environment $\Gamma$ and positive type $P$.

It is worth noticing that the type system in Fig. 2 is syntax oriented: for each type judgment $J$ there is a unique derivation rule whose conclusion matches the judgment $J$.

The size $\lvert\pi\rvert$ of a type derivation $\pi$ is just the the number of $@$ rules in $\pi$. Note that judgments play no role in the size of a derivation.

Example 5**.**

Let $I=\lambda x.{x}$. The derivations (typing $II$ and $I$ with same type and same environment)

[TABLE]

are such that $\lvert\pi_{\_}{II}\rvert=1$ and $\lvert\pi_{\_}I\rvert=0$. Note that $II\rightarrow_{{\mathsf{sh}}^{\flat\!}}I$ and $\lvert\pi_{\_}{II}\rvert=\lvert\pi_{\_}{I}\rvert+1$.

The following lemma (whose proof is quite technical) will play a crucial role to prove the substitution lemma (Lemma 7) and the subject reduction (Prop. 8) and expansion (Prop. 10).

Lemma 6** (Judgment decomposition for values).**

*Let

$v\in\Lambda_{\_}v$, $\Delta$ be an environment, and $P_{\_}1,\dots,P_{\_}p$ be positive types (for some $p\in{\rm Nature}$). There is a derivation $\pi\vartriangleright\Delta\vdash v\colon\!P_{\_}1\uplus\dots\uplus P_{\_}p$ iff for all $1\leq i\leq p$ there are an environment $\Delta_{\_}i$ and a derivation $\pi_{\_}i\vartriangleright\Delta_{\_}i\vdash v\colon\!P_{\_}i$ such that $\Delta=\biguplus_{\_}{i=1}^{p}\Delta_{\_}i$. Moreover, $\lvert\pi\rvert=\sum_{\_}{i=1}^{p}\lvert\pi_{\_}i\rvert$.*

The left-to-right direction of Lemma 6 means that, given $\pi\vartriangleright\Delta\vdash v\colon\!P$, for every $p\in{\rm Nature}$ and every decomposition of the positive type $P$ into a multiset sum of positive types $P_{\_}1,\dots,P_{\_}p$, there are environments $\Delta_{\_}1,\dots,\Delta_{\_}p$ such that $\Delta_{\_}i\vdash v\colon\!P_{\_}i$ is derivable for all $1\leq i\leq p$.

Lemma 7** (Substitution).**

*Let

$t\in\Lambda$ and $v\in\Lambda_{\_}v$. If $\pi\vartriangleright\Gamma,x\colon\!P\vdash t\colon\!Q$ and $\pi^{\prime}\vartriangleright\Delta\vdash v\colon\!P$, then there exists $\pi^{\prime\prime}\vartriangleright\Gamma\uplus\Delta\vdash t\{v/x\}\colon\!Q$ such that $\lvert\pi^{\prime\prime}\rvert=\lvert\pi\rvert+\lvert\pi^{\prime}\rvert$.*

We can now prove the subject reduction, with a quantitative flavour about the size of type derivations in order to extract information about the execution time.

Proposition 8** (Quantitative balanced subject reduction).**

*Let

$t,t^{\prime}\in\Lambda$ and $\pi\vartriangleright\Gamma\vdash t\colon\!Q$.*

Shrinkage under ${{\beta}^{\flat\!}_{v}}$-step:* If $t\rightarrow_{{{\beta}^{\flat\!}_{v}}}t^{\prime}$ then $\lvert\pi\rvert>0$ and there exists a derivation $\pi^{\prime}$ with conclusion $\Gamma\vdash t^{\prime}\colon\!Q$ such that $\lvert\pi^{\prime}\rvert=\lvert\pi\rvert-1$.* 2. 2.

Size invariance under ${\sigma}^{\flat\!}$-step:* If $t\rightarrow_{{\sigma}^{\flat\!}}t^{\prime}$ then $\lvert\pi\rvert>0$ and there exists a derivation $\pi^{\prime}$ with conclusion $\Gamma\vdash t^{\prime}\colon\!Q$ such that $\lvert\pi^{\prime}\rvert=\lvert\pi\rvert$.*

In Prop. 8, the fact that $\rightarrow_{{\mathsf{sh}}^{\flat\!}}$ does not reduce under $\lambda$’s is crucial to get the quantitative information, otherwise one can have a term $t$ such that every derivation $\pi\vartriangleright\Gamma\vdash t\colon\!P$ is such that $\lvert\pi\rvert=0$ (and then there is no derivation $\pi^{\prime}$ with conclusion $\Gamma\vdash t^{\prime}\colon P$ such that $\lvert\pi\rvert=\lvert\pi^{\prime}\rvert-1$): this is the case, for example, for $t=\lambda x.\delta\delta\rightarrow_{{\beta_{v}}}t$. This shows that the quantitative study for evaluation reducing under $\lambda$’s is subtler.

In order to prove the quantitative subject expansion (Prop. 10), we first need the following technical lemma stating the commutation of abstraction with abstraction and application.

Lemma 9** (Abstraction commutation).**

Abstraction vs. abstraction:* Let $k\in{\rm Nature}$. If $\pi\vartriangleright\Delta\vdash\lambda y.{(\lambda x.{t})v}\colon\!\biguplus_{\_}{i=1}^{k}[P_{\_}i^{\prime}\multimap P_{\_}i]$ and $y\notin\mathsf{fv}(v)$, then there is $\pi^{\prime}\vartriangleright\Delta\vdash(\lambda x.{\lambda y.{t}})v\colon\!\biguplus_{\_}{i=1}^{k}[P_{\_}i^{\prime}\multimap P_{\_}i]$ such that $\lvert\pi^{\prime}\rvert=\lvert\pi\rvert+1-k$.* 2. 2.

Application vs. abstraction:* If $\pi\vartriangleright\Delta\vdash((\lambda x.{t})v)((\lambda x.{u})v)\colon\!P$ then there exists a derivation $\pi^{\prime}\vartriangleright\Delta\vdash(\lambda x.{tu})v\colon\!P$ such that $\lvert\pi^{\prime}\rvert=\lvert\pi\rvert-1$.*

Proposition 10** (Quantitative balanced subject expansion).**

Let $t,t^{\prime}\in\Lambda$ and $\pi^{\prime}\vartriangleright\Gamma\vdash t^{\prime}\colon\!Q$.

Enlargement under anti-${{\beta}^{\flat\!}_{v}}$-step:* If $t\rightarrow_{{{\beta}^{\flat\!}_{v}}}t^{\prime}$ then there is $\pi\vartriangleright\Gamma\vdash t\colon\!Q$ with $\lvert\pi\rvert=\lvert\pi^{\prime}\rvert+1$.* 2. 2.

Size invariance under anti-${\sigma}^{\flat\!}$-step:* If $t\rightarrow_{{\sigma}^{\flat\!}}t^{\prime}$ then $\lvert\pi^{\prime}\rvert>0$ and there is $\pi\vartriangleright\Gamma\vdash t\colon\!Q$ with $\lvert\pi\rvert=\lvert\pi^{\prime}\rvert$.*

Actually, subject reduction and expansion hold for the whole $\mathsf{sh}$-reduction $\rightarrow_{\mathsf{sh}}$, not only for the balanced $\mathsf{sh}$-reduction $\rightarrow_{{\mathsf{sh}}^{\flat\!}}$. The drawback for $\rightarrow_{\mathsf{sh}}$ is that the quantitative information about the size of the derivation is lost in the case of a ${\beta_{v}}$-step, see the comments just after Prop. 8 and Lemma 12.

Lemma 11** (Subject reduction).**

Let $t,t^{\prime}\in\Lambda$ and $\pi\vartriangleright\Gamma\vdash t\colon\!Q$.

Shrinkage under ${\beta_{v}}$-step:* If $t\rightarrow_{{\beta_{v}}}t^{\prime}$ then there is $\pi^{\prime}\vartriangleright\Gamma\vdash t^{\prime}\colon\!Q$ with $\lvert\pi\rvert\geq\lvert\pi^{\prime}\rvert$.* 2. 2.

Size invariance under $\sigma$-step:* If $t\rightarrow_{\sigma}t^{\prime}$ then there is $\pi^{\prime}\vartriangleright\Gamma\vdash t^{\prime}\colon\!Q$ such that $\lvert\pi\rvert=\lvert\pi^{\prime}\rvert$.*

Lemma 12** (Subject expansion).**

Let $t,t^{\prime}\in\Lambda$ and $\pi^{\prime}\vartriangleright\Gamma\vdash t^{\prime}\colon\!Q$.

Enlargement under anti-${\beta_{v}}$-step:* If $t\rightarrow_{{\beta_{v}}}t^{\prime}$ then there is $\pi\vartriangleright\Gamma\vdash t\colon\!Q$ with $\lvert\pi\rvert\geq\lvert\pi^{\prime}\rvert$.* 2. 2.

Size invariance under anti-$\sigma$-step:* If $t\rightarrow_{\sigma}t^{\prime}$ then there is $\pi\vartriangleright\Gamma\vdash t\colon\!Q$ such that $\lvert\pi\rvert=\lvert\pi^{\prime}\rvert$.*

In Lemmas 11.1 and 12.1 it is impossible to estimate more precisely the relationship between $\lvert\pi\rvert$ and $\lvert\pi^{\prime}\rvert$. Indeed, Ex. 5 has shown that there are $\pi_{\_}I\vartriangleright y\colon[\,]\vdash I\colon\![\,]$ and $\pi_{\_}{II}\vartriangleright y\colon\![\,]\vdash II\colon\![\,]$ such that $\lvert\pi_{\_}I\rvert=0$ and $\lvert\pi_{\_}{II}\rvert=1$ (where $I=\lambda x.{x}$). So, given $k\in{\rm Nature}$, consider the derivations $\pi_{\_}k\vartriangleright\,\vdash\lambda y.{II}\colon\![[\,]\multimap[\,],\,\overset{k}{\dots}\,,[\,]\multimap[\,]]$ and $\pi_{\_}k^{\prime}\vartriangleright\,\vdash\lambda y.{I}\colon\![[\,]\multimap[\,],\,\overset{k}{\dots}\,,[\,]\multimap[\,]]$ below:

[TABLE]

Clearly, $\lambda y.{II}\rightarrow_{\mathsf{sh}}\lambda y.{I}$ (but $\lambda y.{II}\not\rightarrow_{{\mathsf{sh}}^{\flat\!}}\lambda y.{I}$) and the $\pi_{\_}k^{\prime}$ (resp. $\pi_{\_}k$) is the only derivation typing $\lambda y.{I}$ (resp. $\lambda y.{II}$) with the same type and environment as $\pi_{\_}k$ (resp. $\pi_{\_}k^{\prime}$). One has $\lvert\pi_{\_}k\rvert=k\cdot\lvert\pi_{\_}{II}\rvert=k$ and $\lvert\pi_{\_}k^{\prime}\rvert=k\cdot\lvert\pi_{\_}I\rvert=0$, thus the difference of size of the derivations $\pi_{\_}k$ and $\pi_{\_}k^{\prime}$ can be arbitrarely large (since $k\in{\rm Nature}$); in particular $\lvert\pi_{\_}0\rvert=\lvert\pi_{\_}0^{\prime}\rvert$, so for $k=0$ the size of derivations does not even strictly decrease.

4 Relational semantics: qualitative results

Lemmas 11 and 12 have an important consequence: the non-idempotent intersection type system of Fig. 2 defines a denotational model for the shuffling calculus $\lambda_{\mathsf{sh}}$ (Thm. 14 below).

Definition 13** (Suitable list of variables for a term, semantics of a term).**

Let $t\in\Lambda$ and let $x_{\_}1,\dots,x_{\_}k$ be pairwise distinct variables, for some $k\in{\rm Nature}$.

If $\mathsf{fv}(t)\subseteq\{x_{\_}1,\dots,x_{\_}k\}$, then we say that the list $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ is suitable for $t$.

If $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ is suitable for $t$, the (relational) semantics, or interpretation, of $t$ for $\vec{x}$ is

[TABLE]

Essentially, the semantics of a term $t$ for a suitable list $\vec{x}$ of variables is the set of judgments for $\vec{x}$ and $t$ that can be derived in the non-idempotent intersection type system of Fig. 2.

If we identify the negative type $P\multimap Q$ with the pair $(P,Q)$ and if we set $\mathcal{U}\coloneqq\bigcup_{\_}{k\in\mathbb{N}}\mathcal{U}_{\_}k$ where:

[TABLE]

then, for any $t\in\Lambda$ and any suitable list $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ for $t$, one has $\llbracket t\rrbracket_{\vec{x}}\subseteq\mathcal{M}_{\mathrm{f}}(\mathcal{U})^{k}\times\mathcal{M}_{\mathrm{f}}(\mathcal{U})$; in particular, if $t$ is closed and $\vec{x}=(\,)$, then $\llbracket t\rrbracket=\{Q\mid\exists\,\pi\vartriangleright\ \vdash t\colon\!Q\}\subseteq\mathcal{M}_{\mathrm{f}}(\mathcal{U})$ (up to an obvious isomorphism). Note that $\mathcal{U}=\mathcal{M}_{\mathrm{f}}(\mathcal{U})\times\mathcal{M}_{\mathrm{f}}(\mathcal{U})$: [23, 15] proved that the latter identity is enough to have a denotational model for $\lambda_{\mathsf{sh}}$. We can also prove it explicitly using Lemmas 11 and 12.

Theorem 14** (Invariance under $\mathsf{sh}$-equivalence).**

Let $t,u\in\Lambda$, let $k\in{\rm Nature}$ and let $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ be a suitable list of variables for $t$ and $u$. If $t\simeq_{\mathsf{sh}}u$ then $\llbracket t\rrbracket_{\vec{x}}=\llbracket u\rrbracket_{\vec{x}}$.

An interesting property of relational semantics is that all ${\mathsf{sh}}^{\flat\!}$-normal forms have a non-empty interpretation (Lemma 15). To prove that we use the syntactic characterization of ${\mathsf{sh}}^{\flat\!}$-normal forms (Prop. 3). Note that a stronger statement (Lemma 15.1) is required for ${\mathsf{sh}}^{\flat\!}$-normal forms belonging to $\Lambda_{a}$, in order to handle the case where the ${\mathsf{sh}}^{\flat\!}$-normal form is a $\beta$-redex.

Lemma 15** (Semantics and typability of ${\mathsf{sh}}^{\flat\!}$-normal forms).**

Let $t$ be a term, let $k\in{\rm Nature}$ and let $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ be a list of variables suitable for $t$.

If $t\in\Lambda_{a}$ then for every positive type $Q$ there exist positive types $P_{\_}1,\dots,P_{\_}k$ and a derivation $\pi\vartriangleright x_{\_}1\colon\!P_{\_}1,\dots,x_{\_}k\colon\!P_{\_}k\vdash t\colon\!Q$. 2. 2.

If $t\in\Lambda_{n}$ then there are positive types $Q,P_{\_}1,\dots,P_{\_}k$ and a derivation $\pi\vartriangleright x_{\_}1\colon\!P_{\_}1,\dots,x_{\_}k\colon\!P_{\_}k\allowbreak\vdash t\colon\!Q$. 3. 3.

If $t$ is ${\mathsf{sh}}^{\flat\!}$-normal then $\llbracket t\rrbracket_{\vec{x}}\neq\emptyset$.

A consequence of Prop. 8 (and Thm. 14 and Lemma 15) is a qualitative result: a semantic and logical (if we consider our non-idempotent type system as a logical framework) characterization of (strong) ${\mathsf{sh}}^{\flat\!}$-normalizable terms (Thm. 16). In this theorem, the main equivalences are between Points 1, 3 and 5, already proven in [15] using different techniques. Points 2 and 4 can be seen as “intermediate stages” in the proof of the main equivalences, which are informative enough to deserve to be explicitely stated.

Theorem 16** (Semantic and logical characterization of ${\mathsf{sh}}^{\flat\!}$-normalization).**

Let $t\in\Lambda$ and let $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ be a suitable list of variables for $t$. The following are equivalent:

Normalizability:* $t$ is ${\mathsf{sh}}^{\flat\!}$-normalizable;* 2. 2.

Completeness:* $t\simeq_{\mathsf{sh}}u$ for some ${\mathsf{sh}}^{\flat\!}$-normal $u\in\Lambda$;* 3. 3.

Adequacy:* $\llbracket t\rrbracket_{\vec{x}}\neq\emptyset$;* 4. 4.

Derivability:* there is a derivation $\pi\vartriangleright x_{\_}1\colon\!P_{\_}1,\dots,x_{\_}k\colon\!P_{\_}k\vdash t\colon\!Q$ for some positive types $P_{\_}1,\dots,P_{\_}k,Q$;* 5. 5.

Strong normalizabilty:* $t$ is strongly ${\mathsf{sh}}^{\flat\!}$-normalizable.*

As implication (5)$\Rightarrow$(1) is trivial, the proof of Thm. 16 follows the structure (1)$\Rightarrow$(2)$\Rightarrow$(3)$\Rightarrow$(4)$\Rightarrow$(5): essentially, non-idempotent intersection types are used to prove that normalization implies strong normalization for ${\mathsf{sh}}^{\flat\!}$-reduction. Equivalence (5)$\Leftrightarrow$(1) means that normalization and strong normalization are equivalent for ${\mathsf{sh}}^{\flat\!}$-reduction, thus in studying the termination of ${\mathsf{sh}}^{\flat\!}$-reduction no intricacy arises from its non-determinism. Although $\rightarrow_{{\mathsf{sh}}^{\flat\!}}$ does not evaluate under $\lambda$’s, this result is not trivial because $\rightarrow_{{\mathsf{sh}}^{\flat\!}}$ does not enjoy any form of (quasi-)diamond property, as we show in Ex. 23 below. Equivalence (1)$\Leftrightarrow$(2) says that ${\mathsf{sh}}^{\flat\!}$-reduction is complete with respect to $\mathsf{sh}$-equivalence to get ${\mathsf{sh}}^{\flat\!}$-normal forms; in particular, this entails that every $\mathsf{sh}$-normalizable term is ${\mathsf{sh}}^{\flat\!}$-normalizable. Equivalence (1)$\Leftrightarrow$(2) is the analogue of a well-known theorem [9, Thm. 8.3.11] for ordinary (i.e. call-by-name) $\lambda$-calculus relating head $\beta$-reduction and $\beta$-equivalence: this corroborates the idea that ${\mathsf{sh}}^{\flat\!}$-reduction is the “head reduction” in a call-by-value setting, despite its non-determinism. The equivalence (3)$\Leftrightarrow$(4) holds by definition of relational semantics.

Implication (1)$\Rightarrow$(3) (or equivalently (1)$\Rightarrow$(4), i.e. “normalizable $\Rightarrow$ typable”) does not hold in Plotkin’s $\lambda_{\_}v$: indeed, the (open) terms $t$ and $u$ in Eq. (1) (see also Ex. 2) are ${\beta_{v}}$-normal (because of a stuck $\beta$-redex) but $\llbracket t\rrbracket_{x}=\emptyset=\llbracket u\rrbracket_{x}$. Equivalences such as the ones in Thm. 16 hold in a call-by-value setting provided that ${\beta_{v}}$-reduction is extended, e.g. by adding $\sigma$-reduction. In [5], $\lambda_{\mathsf{sh}}$ is proved to be termination equivalent to other extensions of $\lambda_{\_}v$ (in the framework Open Call-by-Value, where evaluation is call-by-value and weak, on possibly open terms) such as the fireball calculus [46, 28, 3] and the value substitution calculus [8], so Thm. 16 is a general result characterizing termination in those calculi as well.

Lemma 17** (Uniqueness of the derivation with empty types; Semantic and logical characterization of values).**

Let $t\in\Lambda$ be ${\mathsf{sh}}^{\flat\!}$-normal.

If $\pi\vartriangleright\,\vdash t\colon\![\,]$ and $\pi^{\prime}\vartriangleright\Gamma\vdash t\colon\![\,]$, then $t\in\Lambda_{v}$, $\lvert\pi\rvert=0$, $\mathsf{dom}(\Gamma)=\emptyset$ and $\pi=\pi^{\prime}$. More precisely, $\pi$ consists of a rule $\mathsf{ax}$ if $t$ is a variable, otherwise $t$ is an abstraction and $\pi$ consists of a 0-ary rule $\lambda$. 2. 2.

Given a list $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ of variables suitable for $t$, the following are equivalent:

1. (a)

$t$* is a value;* 2. (b)

$(([\,],\overset{k}{\dots\,},[\,]),[\,])\in\llbracket t\rrbracket_{\vec{x}}$* ;* 3. (c)

there exists $\pi\vartriangleright\,\vdash t\colon\![\,]$ ; 4. (d)

there exists $\pi\vartriangleright t$ such that $\lvert\pi\rvert=0$.

Qualitatively, Lemma 17 allows us to refine the semantic and logical characterization given by Thm. 16 for a specific class of terms: the valuable ones, i.e. the terms that ${\mathsf{sh}}^{\flat\!}$-normalize to a value. Valuable terms are all and only the terms whose semantics contains a specific element: the point with only empty types.

Proposition 18** (Logical and semantic characterization of valuability).**

Let $t$ be a term and $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ be a suitable list of variables for $t$. The following are equivalent:

Valuability:* $t$ is ${\mathsf{sh}}^{\flat\!}$-normalizable and the ${\mathsf{sh}}^{\flat\!}$-normal form of $t$ is a value;* 2. 2.

Empty point in the semantics:* $(([\,],\overset{k}{\dots}\,,[\,]),[\,])\in\llbracket t\rrbracket_{\vec{x}}$;* 3. 3.

Derivability with empty types:* there exists a derivation $\pi\vartriangleright\,\vdash t\colon\![\,]$.*

5 The quantitative side of type derivations

By the quantitative subject reduction (Prop. 8), the size of any derivation typing a (${\mathsf{sh}}^{\flat\!}$-normalizable) term $t$ is an upper bound on the number $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d)$ of ${{\beta}^{\flat\!}_{v}}$-steps in any ${\mathsf{sh}}^{\flat\!}$-normalizing reduction sequence $d$ from $t$, since the size of a type derivation decreases by $1$ after each ${{\beta}^{\flat\!}_{v}}$-step, and does not change after each ${\sigma}^{\flat\!}$-step.

Corollary 19** (Upper bound on the number of ${{\beta}^{\flat\!}_{v}}$-steps).**

Let $t$ be a ${\mathsf{sh}}^{\flat\!}$-normalizable term and $t_{\_}0$ be its ${\mathsf{sh}}^{\flat\!}$-normal form. For any reduction sequence $d\colon t\rightarrow_{{\mathsf{sh}}^{\flat\!}}^{*}t_{\_}0$ and any $\pi\vartriangleright t$, $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d)\leq\lvert\pi\rvert$.

In order to extract from a type derivation the exact number of ${{\beta}^{\flat\!}_{v}}$-steps to reach the ${\mathsf{sh}}^{\flat\!}$-normal form, we have to take into account also the size of derivations of ${\mathsf{sh}}^{\flat\!}$-normal forms. Indeed, by Lemma 17.2, ${\mathsf{sh}}^{\flat\!}$-normal forms that are not values admit only derivations with sizes greater than [math]. The sizes of type derivations of a ${\mathsf{sh}}^{\flat\!}$-normal form $t$ are related to a special kind of size of $t$ that we now define.

The balanced size of a term $t$, denoted by $\lvert t\rvert_{\flat\!}$, is defined by induction on $t$ as follows ($v\in\Lambda_{v}$):

[TABLE]

So, the balanced size of a term $t$ is the number of applications occurring in $t$ under a balanced context, i.e. the number of pairs $(u,s)$ such that $t=B\langle us\rangle$ for some balanced context $B$. For instance, $\lvert(\lambda x.{yy})(zz)\rvert_{\flat\!}=3$ and $\lvert(\lambda x.{\lambda x^{\prime}\!.{yy}})(zz)\rvert_{\flat\!}=2$. The following lemma can be seen as a quantitative version of Lemma 15.

Lemma 20** (Relationship between sizes of normal forms and derivations).**

Let $t\in\Lambda$.

If $t$ is ${\mathsf{sh}}^{\flat\!}$-normal then $\lvert t\rvert_{\flat\!}=\min{\{\lvert\pi\rvert\mid\pi\vartriangleright t\}}$. 2. 2.

If $t$ is a value then $\lvert t\rvert_{\flat\!}=\min{\{\lvert\pi\rvert\mid\pi\vartriangleright t\}}=0$.

Thus, the balanced size of a ${\mathsf{sh}}^{\flat\!}$-normal form $n$ equals the minimal size of the type derivation of $n$.

Proposition 21** (Exact number of ${{\beta}^{\flat\!}_{v}}$-steps).**

Let $t$ be a ${\mathsf{sh}}^{\flat\!}$-normalizable term and $t_{\_}0$ be its ${\mathsf{sh}}^{\flat\!}$-normal form. For every reduction sequence $d\colon t\rightarrow_{{\mathsf{sh}}^{\flat\!}}^{*}t_{\_}0$ and every $\pi\vartriangleright t$ and $\pi_{\_}0\vartriangleright t_{\_}0$ such that $\lvert\pi\rvert=\min\{\lvert\pi^{\prime}\rvert\mid\pi^{\prime}\vartriangleright t\}$ and $\lvert\pi_{\_}0\rvert=\min\{\lvert\pi_{\_}0^{\prime}\rvert\mid\pi_{\_}0^{\prime}\vartriangleright t_{\_}0\}$, one has

[TABLE]

If moreover $t_{\_}0$ is a value, then $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d)=\lvert\pi\rvert$.

In particular, Eq. (2) implies that for any reduction sequence $d\colon t\rightarrow_{{\mathsf{sh}}^{\flat\!}}^{*}t_{\_}0$ and any $\pi\vartriangleright t$ and $\pi_{\_}0\vartriangleright t_{\_}0$ such that $\lvert\pi_{\_}0\rvert=\min\{\lvert\pi_{\_}0^{\prime}\rvert\mid\pi_{\_}0^{\prime}\vartriangleright t_{\_}0\}$, one has $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d)\leq\lvert\pi\rvert-\lvert t_{\_}0\rvert_{\flat\!}=\lvert\pi\rvert-\lvert\pi_{\_}0\rvert\,$, since $\lvert\pi\rvert\geq\min\{\lvert\pi^{\prime}\rvert\mid\pi^{\prime}\vartriangleright t\}$.

Prop. 21 could seem slightly disappointinig: it allows us to know the exact number of ${{\beta}^{\flat\!}_{v}}$-steps of a ${\mathsf{sh}}^{\flat\!}$-normalizing reduction sequence from $t$ only if we already know the ${\mathsf{sh}}^{\flat\!}$-normal form $t_{\_}0$ of $t$ (or the minimal derivation of $t_{\_}0$), which essentially means that we have to perform the reduction sequence in order to know the exact number of its ${{\beta}^{\flat\!}_{v}}$-steps. However, Prop. 21 says also that this limitation is circumvented in the case $t$ ${\mathsf{sh}}^{\flat\!}$-reduces to a value. Moreover, a notable and immediate consequence of Prop. 21 is:

Corollary 22** (Same number of ${{\beta}^{\flat\!}_{v}}$-steps).**

Let $t$ be a ${\mathsf{sh}}^{\flat\!}$-normalizable term and $t_{\_}0$ be its ${\mathsf{sh}}^{\flat\!}$-normal form. For all reduction sequences $d\colon t\rightarrow_{{\mathsf{sh}}^{\flat\!}}^{*}t_{\_}0$ and $d^{\prime}\colon t\rightarrow_{{\mathsf{sh}}^{\flat\!}}^{*}t_{\_}0$, one has $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d)=\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d^{\prime})$.

Even if ${\mathsf{sh}}^{\flat\!}$-reduction is weak, in the sense that it does not reduce under $\lambda$’s, Cor. 22 is not obvious at all, since the rewriting theory of ${\mathsf{sh}}^{\flat\!}$-reduction is not quite elegant, in particular it does not enjoy any form of (quasi-)diamond property because of $\sigma$-reduction, as shown by the following example.

Example 23**.**

Let $t\coloneqq(\lambda y.{y^{\prime}})(\Delta(xI))I$: one has $u\coloneqq(\lambda y.{y^{\prime}})(\Delta(xI)){\,}_{{\sigma}^{\flat\!}_{1}}\!\!\leftarrow t\rightarrow_{{\sigma}^{\flat\!}_{3}}(\lambda z.{(\lambda y.{y^{\prime}})(zz)})(xI)I\eqqcolon s$ and the only way to join this critical pair is by performing one ${\sigma}^{\flat\!}_{3}$-step from $u$ and two ${\sigma}^{\flat\!}_{1}$-steps from $s$, so that $u\rightarrow_{{\sigma}^{\flat\!}_{3}}(\lambda z.{(\lambda y.{y^{\prime}I})(zz)})(xI){\,}_{{\sigma}^{\flat\!}_{1}}\!\!\leftarrow(\lambda z.{(\lambda y.{y^{\prime}})(zz)I})(xI){\,}_{{\sigma}^{\flat\!}_{1}}\!\!\leftarrow s$. Since each ${\sigma}^{\flat\!}$-step can create a new ${\beta_{v}}$-redex in a balanced context (as shown in Ex. 2), a priori there is no evidence that Cor. 22 should hold.

Cor. 22 allows us to define the following function $\mathrm{leng}_{\_}{\beta_{v}}\colon\Lambda\to{\rm Nature}\cup\{\infty\}$

[TABLE]

In other words, in $\lambda_{\mathsf{sh}}$ we can univocally associate with every term the number of ${{\beta}^{\flat\!}_{v}}$-steps needed to reach its ${\mathsf{sh}}^{\flat\!}$-normal form, if any (the infinity $\infty$ is associated with non-${\mathsf{sh}}^{\flat\!}$-normalizable terms). The characterization of ${\mathsf{sh}}^{\flat\!}$-normalization given in Thm. 16 allows us to determine through semantic or logical means if the value of $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(t)$ is a finite number or not.

Quantitatively, via Lemma 17 we can simplify the way to compute the number of ${{\beta}^{\flat\!}_{v}}$-steps to reach the ${\mathsf{sh}}^{\flat\!}$-normal form of a valuable (i.e. that reduces to a value) term $t$, using only a specific type derivation of $t$.

Theorem 24** (Exact number of ${{\beta}^{\flat\!}_{v}}$-steps for valuables).**

*If $t\rightarrow_{{\mathsf{sh}}^{\flat\!}}^{*}\!v\in\Lambda_{v}$ then $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(t)=\lvert\pi\rvert$ for $\pi\vartriangleright\,\vdash t\colon\![\,]$. *

Prop. 18 and Thm. 24 provide a procedure to determine if a term $t$ ${\mathsf{sh}}^{\flat\!}$-normalizes to a value and, in case, how many ${{\beta}^{\flat\!}_{v}}$-steps are needed to reach its ${\mathsf{sh}}^{\flat\!}$-normal form (this number does not depend on the reduction strategy according to Cor. 22), considering only the term $t$ and without performing any ${\mathsf{sh}}^{\flat\!}$-step:

check if there is a derivation $\pi$ with empty types, i.e. $\pi\vartriangleright\,\vdash t\colon\![\,]$; 2. 2.

if it is so (i.e. if $t$ ${\mathsf{sh}}^{\flat\!}$-normalize to a value, according to Prop. 18), compute the size $\lvert\pi\rvert$.

Remind that, according to Cor. 4, any closed term either is not ${\mathsf{sh}}^{\flat\!}$-normalizable, or it ${\mathsf{sh}}^{\flat\!}$-normalizes to a (closed) value. So, this procedure completely determines (qualitatively and quantitatively) the behavior of closed terms with respect to ${\mathsf{sh}}^{\flat\!}$-reduction (and to ${{\beta}^{\flat\!}_{v}}$-reduction, as we will see in Sect. 6).

6 Conclusions

Back to Plotkin’s $\lambda_{\_}v$.

The shuffling calculus $\lambda_{\mathsf{sh}}$ can be used to prove some properties of Plotkin’s call-by-value $\lambda$-calculus $\lambda_{\_}v$ (whose only reduction rule is $\rightarrow_{{\beta_{v}}}$) restricted to closed terms. This is an example of how the study of some properties of a framework (in this case, $\lambda_{\_}v$) can be naturally done in a more general framework (in this case, $\lambda_{\mathsf{sh}}$). It is worth noting that $\lambda_{\_}v$ with only closed terms is an interesting fragment: it represents the core of many functional programming languages, such as OCaml.

The starting point is Cor. 4, which says that, in the closed setting with weak reduction, normal forms for $\lambda_{\mathsf{sh}}$ and $\lambda_{\_}v$ coincide: they are all and only closed values. We can then reformulate Thm. 16 and Prop. 18 as a semantic and logical characterization of ${{\beta}^{\flat\!}_{v}}$-normalization in Plotkin’s $\lambda_{\_}v$ restricted to closed terms.

Theorem 25** (Semantic and logical characterization of ${{\beta}^{\flat\!}_{v}}$-normalization in the closed case).**

Let $t$ be a closed term. The following are equivalent:

Normalizability:* $t$ is ${{\beta}^{\flat\!}_{v}}$-normalizable;* 2. 2.

Valuability:* $t\rightarrow_{{{\beta}^{\flat\!}_{v}}}^{*}v$ for some closed value $v$;* 3. 3.

Completeness:* $t\simeq_{\beta_{v}}v$ for some closed value $v$;* 4. 4.

Adequacy:* $\llbracket t\rrbracket_{\vec{x}}\neq\emptyset$ for any list $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ (with $k\in{\rm Nature}$) of pairwise distinct variables;* 5. 5.

Empty point:* $(([\,],\overset{k}{\dots}\,,[\,]),[\,])\in\llbracket t\rrbracket_{\vec{x}}$ for any list $\vec{x}=(x_{\_}1,\dots,x_{\_}k)$ ($k\in{\rm Nature}$) of pairwise distinct variables;* 6. 6.

Derivability with empty types:* there exists a derivation $\pi\vartriangleright\,\vdash t\colon\![\,]$;* 7. 7.

Derivability:* there exists a derivation $\pi\vartriangleright\,\vdash t\colon\!Q$ for some positive type $Q$; * 8. 8.

Strong normalizabilty:* $t$ is strongly ${{\beta}^{\flat\!}_{v}}$-normalizable.*

We have already seen on pp. 16–17 that Thm. 25 does not hold in $\lambda_{\_}v$ with open terms: closure is crucial.

Thm. 25 entails that a closed term is ${\mathsf{sh}}^{\flat\!}$-normalizable iff it is ${{\beta}^{\flat\!}_{v}}$-normalizable iff it ${{\beta}^{\flat\!}_{v}}$-reduces to a closed value. Thus, Cor. 22 and Thm. 24 can be reformulated for $\lambda_{\_}v$ restricted to closed terms as follows.

Corollary 26** (Same number of ${{\beta}^{\flat\!}_{v}}$-steps).**

Let $t$ be a closed ${{\beta}^{\flat\!}_{v}}$-normalizable term and $t_{\_}0$ be its ${{\beta}^{\flat\!}_{v}}$-normal form. For all reduction sequences $d\colon t\rightarrow_{{{\beta}^{\flat\!}_{v}}}^{*}t_{\_}0$ and $d^{\prime}\colon t\rightarrow_{{{\beta}^{\flat\!}_{v}}}^{*}t_{\_}0$, one has $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d)=\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(d^{\prime})$.

Theorem 27** (Number of ${{\beta}^{\flat\!}_{v}}$-steps).**

If $t$ is closed and ${{\beta}^{\flat\!}_{v}}$-normalizable, then $\mathrm{leng}_{{{\beta}^{\flat\!}_{v}}}(t)=\lvert\pi\rvert$ for $\pi\vartriangleright\,\vdash t\colon\![\,]$.

Clearly, the procedure sketched on p. 6, when applied to a closed term $t$, determines if $t$ ${{\beta}^{\flat\!}_{v}}$-normalizes and, in case, how many ${{\beta}^{\flat\!}_{v}}$-steps are needed to reach its ${{\beta}^{\flat\!}_{v}}$-normal form.

Towards a semantic measure.

In order to get a truly semantic measure of the execution time in the shuffling calculus $\lambda_{\mathsf{sh}}$, we should first be able to give an upper bound to the number of ${{\beta}^{\flat\!}_{v}}$-steps in a ${\mathsf{sh}}^{\flat\!}$-reduction looking only at the semantics of terms. Therefore, we need to define a notion of size for the elements of the semantics of terms. The most natural approach is the following. For any positive type $P=[P_{\_}1\multimap Q_{\_}1,\dots,P_{\_}k\multimap Q_{\_}k]\in\mathcal{M}_{\mathrm{f}}(\mathcal{U})$ (with $k\in{\rm Nature}$), the size of $P$ is $\lvert P\rvert=k+\sum_{\_}{i=1}^{k}(\lvert P_{\_}i\rvert+\lvert Q_{\_}i\rvert)$. So, the size of a positive type $P$ is the number of occurrences of $\multimap$ in $P$; in particular, $\lvert[\,]\rvert=0$. For any $((P_{\_}1,\dots,P_{\_}n),Q)\in\mathcal{M}_{\mathrm{f}}(\mathcal{U})^{k}\times\mathcal{M}_{\mathrm{f}}(\mathcal{U})$ (with $k\in{\rm Nature}$), the size of $((P_{\_}1,\dots,P_{\_}k),Q)$ is $\lvert((P_{\_}1,\dots,P_{\_}k),Q)\rvert=\lvert Q\rvert+\sum_{\_}{i=1}^{k}\lvert P_{\_}i\rvert$.

The approach of [17, 18] relies on a crucial lemma to find an upper bound (and hence the exact length) of the execution time: it relates the size of a type derivation to the size of its conclusion, for a normal term/proof-net. In $\lambda_{\mathsf{sh}}$ this lemma should claim that “For every $\mathsf{sh}$-normal form $t$, if $\pi\vartriangleright x_{\_}1\colon\!P_{\_}1,\dots,x_{\_}k\colon\!P_{\_}k\vdash t\colon\!Q$ then $\lvert\pi\rvert\leq\lvert((P_{\_}1,\dots,P_{\_}k),Q)\rvert$”. Unfortunately, in $\lambda_{\mathsf{sh}}$ this property is false!

Example 28**.**

Let $t\coloneqq(\lambda x.{x})(yy)$, which is a $\mathsf{sh}$-normal form. Consider the derivation

[TABLE]

Then, $\lvert\pi\rvert=2>1=\lvert([[\,]\multimap[\,]],[\,])\rvert$, which provides a counterexample to the property demanded above.

We conjecture that in order to overcome this counterexample (and to successfully follow the method of [17, 18] to get a purely semantic measure of the execution time) we should change the syntax and the operational semantics of our calculus, always remaining in a call-by-value setting equivalent (from the termination point of view) to $\lambda_{\mathsf{sh}}$ and the other calculi studied in [5]. Intuitively, in Ex. 28 $t$ contains one application — $(\lambda x.{x})(yy)$ — that is a stuck $\beta$-redex and is the source of one “useless” instance of the rule $@$ in $\pi$. The idea for the new calculus is to “fire” a stuck $\beta$-redex $(\lambda x.{t})u$ without performing the substitution $t\{u/x\}$ (as $u$ might not be a value), but just creating an explicit substitution $t[u/x]$ that removes the application but “stores” the stuck $\beta$-redex. Such a calculus has been recently introduced in [6].

Related work.

This work has been presented at the workshop ITRS 2018. Later, the author further investigated this topic with Beniamino Accattoli in [6], where we applied the same type system (and hence the same relational semantics) to a different call-by-value calculus with weak evaluation, $\lambda_{\mathsf{fire}}$. The techniques used in both papers are similar (but not identical), some differences are due to the distinct calculi the type system is applied to. Some results are analogous: semantic and logical characterization of termination, extraction of quantitative information from type derivations. In [6] we focused on an abstract characterization of the type derivations that provide an exact bound on the number of steps to reach the normal form. Here, the semantic and logical characterization of termination is more informative than in [6] because the reduction in $\lambda_{\mathsf{sh}}$ is not deterministic, contrary to $\lambda_{\mathsf{fire}}$ (the proof that normalization and strong normalization coincide makes sense only for $\lambda_{\mathsf{sh}}$). Moreover here, unlike [6], we investigate in detail the case of terms reducing to values and how the general results for $\lambda_{\mathsf{sh}}$ can be applied to analyze qualitative and quantitative properties of Plotkin’s $\lambda_{\_}v$ restricted to closed terms (see above).

Recently, Mazza, Pellissier and Vial [38] introduced a general, elegant and abstract framework for building intersection (idempotent and non-idempotent) type systems characterizing normalization in different calculi. However, such a work contains a wrong claim in one of its applications to concrete calculi and type systems, confirmed by a personal communication with the authors: they affirm that the same type system as the one used here characterizes normalization in Plotkin’s $\lambda_{\_}v$ (endowed with the reduction $\rightarrow_{{{\beta}^{\flat\!}_{v}}}$), but we have shown on pp. 16–17 that this is false for open terms. Indeed, the property called full expansiveness in [38] (which entails that “normalizable $\Rightarrow$ typable”) actually does not hold in $\lambda_{\_}v$. It is still true that their approach can be applied to characterize termination in Plotkin’s $\lambda_{\_}v$ restricted to closed terms and in the shuffling calculus $\lambda_{\mathsf{sh}}$. Proving that the abstract properties described in [38] to characterize normalization hold in closed $\lambda_{\_}v$ or in $\lambda_{\mathsf{sh}}$ amounts essentially to show that subject reduction (our Prop. 8), subject expansion (our Prop. 10) and typability of normal forms (our Lemma 15) hold.

The shuffling calculus $\lambda_{\mathsf{sh}}$ is compatible with Girard’s call-by-value translation of $\lambda$-terms into linear logic ($\mathsf{LL}$) proof-nets: according to that, $\lambda$-values (which are the only duplicable and erasable $\lambda$-terms) are the only $\lambda$-terms translated as boxes; also, $\mathsf{sh}$-reduction corresponds to cut-elimination and ${\mathsf{sh}}^{\flat\!}$-reduction corresponds to cut-elimination at depth [math] (i.e. outside exponential boxes). The exact correspondence has many technical intricacies, which are outside the scope of this paper, anyway it can be recovered by composing the translation of the value substitution calculus (another extension of Plotkin’s $\lambda_{\_}v$) into $\mathsf{LL}$ proof-nets (see [2]), and the encoding (studied in [5]) of $\lambda_{\mathsf{sh}}$ into the value substitution calculus. The relational semantics studied here is nothing but the relational semantics for $\mathsf{LL}$ (see [18]) restricted to fragment of $\mathsf{LL}$ that is the image of Girard’s call-by-value translation. The notion of “experiment” in [18] corresponds to our type derivation, and the “result” of an experiment there corresponds to the conclusion of a type derivation here. The main results of de Carvalho, Pagani and Tortora de Falco [18] are similar to ours: characterization of normalization for $\mathsf{LL}$ proof-nets, extraction of quantitative information from (results of) experiments. Nonetheless, the properties shown here for $\lambda_{\mathsf{sh}}$ cannot be derived by simply analyzing the analogous results for $\mathsf{LL}$ proof-nets (proven in [18]) within its call-by-value fragment. Indeed, Ex. 28 shows that some property, which holds in the — apparently — more general case of untyped $\mathsf{LL}$ proof-nets (as proven in [18]), does not hold in the — apparently — special case of terms in $\lambda_{\mathsf{sh}}$. It could seem surprising but, actually, there is no contradiction because $\mathsf{LL}$ proof-nets in [18] always require an explicit constructor for dereliction, whereas $\lambda_{\mathsf{sh}}$ is outside of this fragment since variables correspond in $\mathsf{LL}$ proof-nets to exponential axioms (which keep implicit the dereliction).

All the papers cited in this section are (more or less explicitly) inspired by de Carvalho’s seminal work [16, 17], which first used relational semantics and non-idempotent intersection types to count the number of $\beta$-steps to reach the normal form in the call-by-name $\lambda$-calculus. Our results, although analogous and proven following an approach similar to [16, 17], cannot be derived directly from [16, 17]: indeed, the call-by-name $\lambda$-calculus corresponds to a different fragment of $\mathsf{LL}$ than call-by-value (as said in Sect. 1, call-by-name and call-by-value $\lambda$-calculi are translated into $\mathsf{LL}$ via two distinct embeddings). There is also another difference: de Carvalho [16, 17] counts the number of $\beta$-steps in linear call-by-name evaluation, which substitutes the argument of a $\beta$-redex for one variable occurrence at a time; here we compute the number of $\beta$-steps in non-linear call-by-value evaluation, which substitutes the argument of a ${\beta_{v}}$-redex for all the free occurrences of the redex-variable in just one step. A comprehensive study of the quantitative information given by non-idempotent intersection type systems for several (linear and non-linear) variants of call-by-name evaluation is provided in [4]. In [7] it has been introduced a non-idempotent intersection type system that combines some features of both call-by-name and call-by-value systems, providing quantitative information about the number of $\beta$-steps to reach the normal form by call-by-need evaluation.