Dieses Kapitel präsentiert eine bahnbrechende Untersuchung der Korrespondenz der Sätze als Typen, die sie auf die lineare Logik und ihren ressourcenbewussten Ansatz ausweitet. Es führt die Lineare Logik mit eingeschränktem Zugriff ein, ein neuartiges logisches System, das jede exponentielle Modalität in Sharing- und Zugriffsmodalitäten aufteilt und so eine nuanciertere Kontrolle über ressourcensensible Phänomene wie Parallelität und Speichermanagement bietet. Das Kapitel greift erneut Girards Übersetzungen intuitionistischer Logik in lineare Logik auf, passt sie an das neue System an und bietet eine logische Grundlage für verschiedene Bewertungsmechanismen, darunter Call-by-Name, Call-by-Value und eine neu vorgeschlagene Call-by-Sharing-Strategie. Es wird auch die Einbettung dieser Bewertungsmechanismen in das neue logische System diskutiert, was Solidität und Vollständigkeit demonstriert. Darüber hinaus stellt das Kapitel einen schwachen Evaluierungsmechanismus vor, der schwache Evaluierungsstrategien in den ursprünglichen Kalkulationen simuliert und einen einheitlichen Rahmen für das Verständnis unterschiedlicher Evaluierungsstrategien bietet. Das Kapitel schließt mit einer Diskussion über verwandte Arbeiten und potenzielle Wege zukünftiger Forschung, einschließlich der Entwicklung von Beweisnetzen und Semantik für das neue logische System und der Erforschung der operativen Eigenschaften der gemeinsamen linearen Lambda-Kalkulation.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping \(A\rightarrow B\) respectively to \({!}{A}\multimap B\) and \({!}{(A\multimap B)}\), have been shown to correspond respectively to call-by-name and call-by-value.
In this work, we split the of-course modality of linear logic into two modalities, written “\({!} \)” and “\(\bullet \)”. Intuitively, the modality “\({!} \)” specifies a subproof that can be duplicated and erased, but may not necessarily be “accessed”, i.e. interacted with, while the combined modality “\({!}{\bullet }\)” specifies a subproof that can moreover be accessed. The resulting system, called \(\textsf{MSCLL}\), enjoys cut-elimination and is conservative over \(\textsf{MELL}\).
We study how restricting access to subproofs provides ways to control sharing in evaluation strategies. For this, we introduce a term-assignment for an intuitionistic fragment of \(\textsf{MSCLL}\), called the \(\lambda ^{{!}{\bullet }}\)-calculus, which we show to enjoy subject reduction, confluence, and strong normalization of the simply typed fragment. We propose three sound and complete translations that respectively simulate call-by-name, call-by-value, and a variant of call-by-name that shares the evaluation of its arguments (similarly as in call-by-need). The translations are extended to simulate the Bang-calculus, as well as weak reduction strategies.
1 Introduction
The propositions-as-types correspondence links computation and logic, relating types with propositions, programs with proofs, and program evaluation with proof normalization. The prime example is the simply typed \(\lambda \)-calculus, which corresponds to intuitionistic propositional logic. The correspondence has been extended to many other calculi and logics, including Linear Logic (\(\textsf{LL}\)) [16]. Linear Logic proposes a resource conscious approach to logic, in that only formulae prefixed with an exponential modality can be duplicated and erased. In \(\textsf{LL}\), there are two exponential modalities: of-course (“\({!} \)”), allowing duplication/erasure on the left, and why-not (“\({?} \)”), allowing duplication/erasure on the right. These modalities recover the ability to duplicate and erase formulae in a controlled way, making \(\textsf{LL}\) a suitable language to model resource-sensitive phenomena such as concurrency, memory management, and computational complexity.
Girard [16] discusses two possible ways of embedding intuitionistic logic into \(\textsf{LL}\), mapping the intuitionistic implication \(A\rightarrow B\) respectively to \({!}{A}\multimap B\) and to \({!}{A}\multimap {!}{B}\), where “\(\multimap \)” stands for the linear implication1. Maraist et al. [22] observed that these translations can be used to extend the propositions-as-types correspondence to provide a logical foundation for evaluation mechanisms.
Anzeige
The most well-known evaluation mechanism for the \(\lambda \)-calculus is perhaps call-by-name (\({{\textsf{CBN}}}\)), in which arguments to functions are re-evaluated upon each use. The theory of \({{\textsf{CBN}}}\) has been thoroughly developed, e.g. in Barendregt’s book [11]. On the other hand, in the call-by-value (\({{\textsf{CBV}}}\)) evaluation mechanism [26], arguments to functions are evaluated once and for all; then their value can be recalled upon each use. Call-by-value is less deeply studied in the literature than \({{\textsf{CBN}}}\), but it has been gaining attention since its theory is subtle and corresponds more closely to the evaluation mechanism behind most programming languages.
Embeddings Encode Evaluation Mechanisms. The first Girard translation
operates on formulae by mapping
to
. It operates on terms in such a way that a \(\lambda \)-calculus application \(t\,s\) is mapped to
in a linear\(\lambda \)-calculus2. Here “\({!} \)” is a term constructor, which corresponds to an instance of the \({!} \)-introduction rule, also called promotion. The key point is that the argument \(s\) of an application is prefixed with “\({!} \)”. This enables the (arbitrary) term
to be freely copied or discarded in
, as dictated by \({{\textsf{CBN}}}\). In this sense, the first translation provides a logical foundation for the \({{\textsf{CBN}}}\) evaluation mechanism.
The second Girard translation
operates on formulae by mapping the intuitionistic implication \(A\rightarrow B\) to
. It operates on terms in such a way that a \(\lambda \)-calculus application \(t\,s\) is mapped to
. Here, \(\texttt{der}(\cdot )\) stands for an appropriate operation in the target language that corresponds to the \({!} \)-elimination rule, also called dereliction. The key point is that the argument is not prefixed with “\({!} \)”, which means that it must be evaluated before being consumed, as dictated by \({{\textsf{CBV}}}\). This translation prefixes values, such as \(\lambda x.\,r\), with a promotion, resulting in
. Consequently, only values will end up being copied or discarded.
Linear Logic with Restricted Access. In this work, we propose a logical system that arises from splitting each exponential modality into two new modalities. We refer to this new system as Linear Logic with Restricted Access, and formally as \(\textsf{MSCLL}\), to reflect that we study the fragment with Multiplicative, Sharing, and aCcess connectives. The exponential of-course (“\({!} \)”) modality of \(\textsf{LL}\) is split into two modalities in \(\textsf{MSCLL}\): a sharing modality “\({!} \)” and an access modality “\(\bullet \)”, that “grants” access to a subproof. The sharing of-course of \(\textsf{MSCLL}\) turns out to be weaker than the exponential of-course of \(\textsf{LL}\) but, by abuse of notation, we denote it using the same symbol “\({!} \)”. Dually, the exponential why-not (“\({?} \)”) modality of \(\textsf{LL}\) is split into a sharing modality “\({?} \)” and an access modality “\(\circ \)” in \(\textsf{MSCLL}\). The resulting system \(\textsf{MSCLL}\) is a conservative extension of Multiplicative Exponential Linear Logic (\(\textsf{MELL}\)), in which the combined modality “\({!}{\bullet }\)” plays the role of the exponential of-course modality of \(\textsf{LL}\). The operational intuition is that the sharing modality “\({!} \)” in \(\textsf{MSCLL}\) specifies an expression that may be duplicated and erased, but it may not necessarily be used or accessed. The combined modality “\({!}{\bullet }\)” specifies an expression that may, additionally, be accessed, i.e. its contents can be made to interact with the surrounding computational context.
Anzeige
Embedding Call-by-Name and Call-by-Value. Following, we revisit Girard’s translations, but this time targetting the \(\lambda ^{{!}{\bullet }}\)-calculus, a linear \(\lambda \)-calculus based on \(\textsf{MSCLL}\). Our \({{\textsf{CBN}}}\) translation
operates on formulae by mapping \(A\rightarrow B\) to
. It operates on terms by mapping a \(\lambda \)-calculus application \(t\,s\) to
, indicating that the argument may be freely copied, discarded, and accessed. This mimics the original translation of \({{\textsf{CBN}}}\) to \(\textsf{LL}\). Our \({{\textsf{CBV}}}\) translation
operates on formulae by mapping \(A\rightarrow B\) to
. It operates on terms by leaving the translation of the argument of an application intact, mapping \(t\,s\) to
. As before, \(\texttt{der}(\cdot )\) is an appropriate operator corresponding to \({!} \)-elimination, while \(\texttt{req}(\cdot )\) stands for \(\bullet \)-elimination. At the same time, the translation maps values such as \(\lambda x.\,t\) (roughly3) to
. Thus an argument
cannot be copied, discarded, or accessed at all unless later, after further evaluation, it takes the form \({!}{\bullet \texttt{v}}\), for some value \(\texttt{v}\), in which case \(\texttt{v}\) can be copied. This too mimics the original translation from \({{\textsf{CBV}}}\) to \(\textsf{LL}\). The \({{\textsf{CBN}}}\) and \({{\textsf{CBV}}}\) translations are proved to be sound and complete, in the sense that two \(\lambda \)-terms are interconvertible in the source language if and only if they are mapped to interconvertible terms in the target language.
Call-by-Sharing. The two translations above suggest a “missing link” translation
that maps \(A\rightarrow B\) to
. This translation cannot be expressed directly in a linear \(\lambda \)-calculus, because the “\(\bullet \)” modality is used as a stand-alone operator. A \(\lambda \)-calculus application \(t\,s\) is now mapped to
, meaning that the argument can be copied and discarded, but not accessed yet. A value such as \(\lambda x.\,r\) is now (roughly) mapped to
. Thus an argument
cannot be accessed unless, after further evaluation, it takes the form \(\bullet \texttt{v}\), for some value \(\texttt{v}\), in which case \(\texttt{v}\) can be accessed. The fact that arguments cannot be accessed until they become values means that the evaluation mechanism can keep references to a single shared copy of the argument, until it becomes accessible. This translation suggests an evaluation mechanism that we dub call-by-sharing (\({{\textsf{CBS}}}\)).
Call-by-sharing bears a strong resemblance to call-by-need (\({{\textsf{CBNd}}}\)), an evaluation mechanism introduced by Wadsworth in 1971 [28]. Both in \({{\textsf{CBNd}}}\) and in \({{\textsf{CBS}}}\), arguments that are not used may be discarded without being evaluated. A reference to a shared argument may be freely copied, but the argument itself can only be copied after it has been evaluated to a value. Nevertheless, there are some subtle differences between \({{\textsf{CBNd}}}\) and \({{\textsf{CBS}}}\), and in particular \({{\textsf{CBS}}}\) achieves less sharing than \({{\textsf{CBNd}}}\) (see the discussion in Section 5). Unfortunately, there does not seem to be a way to embed \({{\textsf{CBNd}}}\) into \(\lambda ^{{!}{\bullet }}\).
Bang Calculus. Another approach towards providing a common framework to explain \({{\textsf{CBV}}}\) and \({{\textsf{CBN}}}\) is the Bang-calculus [15]. It is an untyped lambda calculus that has explicit constructors in the syntax for promotion (\({!} \)-introduction) and dereliction (\({!} \)-elimination). It was motivated by the fact that Girard’s original \({{\textsf{CBN}}}\) and \({{\textsf{CBV}}}\) translations of the intuitionistic logic into \(\textsf{LL}\) made use of logical exponentials (promotion and dereliction) that were not reflected in the syntax. The aim was thus to introduce an intermediate formalism between lambda calculus and proof nets, a graphical notation for \(\textsf{LL}\) proofs [16], that allows explicit use of “boxes” to mark values. Soundness and completeness of these translations with respect to reduction was proved by Guerrieri and Manzonetto [17] for slightly different notion of reduction for the Bang-calculus than that of [15]. The Bang-calculus can in fact be embedded into our \(\lambda ^{{!}{\bullet }}\)-calculus and this embedding is both sound and complete.
Contributions. A summary of the contributions are as follows:
1.
The introduction of a new logic called \(\textsf{MSCLL}\) (“Linear Logic with Restricted Access) that enjoys cut-elimination and is conservative over \(\textsf{MELL}\). It provides a split of each exponential modality into a sharing modality and an access modality.
2.
A term assignment for \(\textsf{MSCLL}\), the \(\lambda ^{{!}{\bullet }}\)-calculus, which operationally distinguishes between two kinds of expressions. Sharable expressions can be discarded, and references to shared expressions can be duplicated, but they cannot be accessed, and thus they can remain shared. Sharable accessible expressions can moreover be accessed, and they are copied whenever access to them is requested. This distinction allows to formulate the \({{\textsf{CBS}}}\) evaluation mechanism.
3.
Translations from \({{\textsf{CBV}}}\) and \({{\textsf{CBN}}}\) to \(\lambda ^{{!}{\bullet }}\) that are sound, complete and preserve normal forms.
4.
The presentation of the call-by-sharing calculus (\({{\textsf{CBS}}}\)), and a translation from \({{\textsf{CBS}}}\) to \(\lambda ^{{!}{\bullet }}\) that is sound, complete and preserves normal forms.
5.
A weak evaluation mechanism for \(\lambda ^{{!}{\bullet }}\) that can simulate weak evaluation strategies in \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\) and \({{\textsf{CBS}}}\), with soundness and completeness results.
Structure of the paper. We review some background notions in Section 2. We present \(\textsf{MSCLL}\) in Section 3 and a term assignment for this logic, the \(\lambda ^{{!}{\bullet }}\)-calculus, in Section 4. Definitions of the \({{\textsf{CBV}}}\), \({{\textsf{CBN}}}\), and \({{\textsf{CBS}}}\) calculi and their translations to \(\lambda ^{{!}{\bullet }}\) are presented in Section 5 together with results of soundness, completeness, and preservation of normal forms. Section 6 presents a notion of weak evaluation for \(\lambda ^{{!}{\bullet }}\) which is shown to simulate weak \({{\textsf{CBV}}}\), \({{\textsf{CBN}}}\), and \({{\textsf{CBS}}}\) evaluation. Finally, we conclude and discuss future work. Full proofs are available in the companion report [10]. A further section detailing a sound and complete embedding from the Bang-calculus into the \(\lambda ^{{!}{\bullet }}\)-calculus has been omitted due to lack of space, and can also be found in the companion report.
2 Preliminary Notions
In this section we present some background notions and results that we use throughout the paper.
Recall that an abstract rewriting system (ARS) is a pair \(\mathcal {X}= (X,\rightarrow _\mathcal {X})\) where X is a set and \({\rightarrow _\mathcal {X}} \subseteq X^2\) is a binary relation called reduction. We write \(\rightarrow _\mathcal {X}^*\) for the reflexive–transitive closure of \(\rightarrow _\mathcal {X}\), \(\rightarrow _\mathcal {X}^+\) for the transitive closure, \(\rightarrow _\mathcal {X}^=\) for the reflexive closure, \(\leftrightarrow _\mathcal {X}\) for the symmetric closure, \(\leftarrow _\mathcal {X}\) or \(\rightarrow _\mathcal {X}^{-1}\) for the inverse relation, and \(\rightarrow _\mathcal {X}^n\) for the composition of \(\rightarrow _\mathcal {X}\) with itself n times. An ARS is confluent (CR) if \({\leftarrow _\mathcal {X}^*\,\rightarrow _\mathcal {X}^*} \subseteq {\rightarrow _\mathcal {X}^*\,\leftarrow _\mathcal {X}^*}\) and strongly normalizing (SN) if there are no infinite reductions \(x_1 \rightarrow _\mathcal {X}x_2 \rightarrow _\mathcal {X}\ldots \).
Abstract Results on Translations Given ARSs \(\mathcal {X}= (X,\rightarrow _\mathcal {X})\) and \(\mathcal {Y}= (Y,\rightarrow _\mathcal {Y})\), a translation\(T : \mathcal {X}\rightarrow \mathcal {Y}\) is a function \(T : X \rightarrow Y\), also written T, by abuse of notation. A translation is sound if \(x_1 \rightarrow _\mathcal {X}^* x_2\) implies \(T(x_1) \rightarrow _\mathcal {Y}^* T(x_2)\) for all \(x_1,x_2 \in X\), and complete if \(T(x_1) \rightarrow _\mathcal {Y}^* T(x_2)\) implies \(x_1 \rightarrow _\mathcal {X}^* x_2\) for all \(x_1,x_2 \in X\). The following are easy results on a translation T:
Proposition 2.1
(Conditions for soundness). If \(x_1 \rightarrow _\mathcal {X}x_2\) implies \(T(x_1) \rightarrow _\mathcal {Y}^* T(x_2)\) for every \(x_1,x_2 \in X\), then T is sound.
Theorem 2.1
(Conditions for completeness). Let \(Y' \subseteq Y\) and let \(T^{-1} : Y' \rightarrow X\) be a function. Suppose that \(T^{-1}\) is the left-inverse of T, i.e. for all \(x \in X\) we have that \(T(x) \in Y'\) and \(T^{-1}(T(x)) = x\). Suppose moreover that \(T^{-1}\) simulates reduction, i.e. for all \(y_1 \in Y'\) and \(y_2 \in Y\) such that \(y_1 \rightarrow _\mathcal {Y}y_2\), we have that \(y_2 \in Y'\) and \(T^{-1}(y_1) \rightarrow _\mathcal {X}^* T^{-1}(y_2)\). Then T is complete.
The Linear Substitution Calculus The LSC is a refinement of the \(\lambda \)-calculus with explicit substitutions, introduced by Accattoli and Kesner [1, 3] as a variation over a calculus by Milner [24]. The set of LSCterms (\(\mathcal {T}_{\textsf{LSC}}\)) is defined as follows, where \([x/s]\) is called an explicit substitution (ES):
Free and bound occurrences of variables are defined as expected, and \(\textsf{fv}(t)\) denotes the set of free variables of \(t\). Terms are defined up to \(\alpha \)-renaming of bound variables.
We write \(\texttt{C}\langle t\rangle \) for the variable-capturing substitution of \(\Box \) in \(\texttt{C}\) by \(t\). We write \(\texttt{C}\langle \!\langle t\rangle \!\rangle \) for the capture-avoiding substitution of \(\Box \) in \(\texttt{C}\) by \(t\). For example, if \(\texttt{C}= \lambda x.\,\Box \) then \(\texttt{C}\langle x\rangle = \lambda x.\,x\), while \(\texttt{C}\langle \!\langle x\rangle \!\rangle = \lambda y.\,x \ne \lambda x.\,x\). In the case of substitution contexts, we usually write \(t\texttt{L}\) rather than \(\texttt{L}\langle t\rangle \). The domain of \(\texttt{L}\), written \(\textsf{dom}(\texttt{L})\), is the set of variables bound by \(\texttt{L}\). The LSC has three rewriting rules, closed by congruence under arbitrary contexts:
Distance beta (\(\textsf{db}\)) performs a \(\beta \)-step but creates an ES rather than doing meta-level substitution, linear substitution (\(\textsf{ls}\)) replaces a single occurrence of \(x\) to a term \(t\) when \(x\) is bound to \(t\) by an ES, and garbage collection (\(\textsf{gc}\)) removes an unreachable ES. Reduction in LSC is the union \({\rightarrow _{{\text {lsc}}}} :={\rightarrow _{\textsf{db}}\cup \rightarrow _{\textsf{ls}}\cup \rightarrow _{\textsf{gc}}}\).
The rewriting rules of LSC are said to operate “at a distance” due to their peculiar use of contexts. This avoids reduction getting stuck in the presence of explicit substitutions. For example, if the left-hand side of \(\textsf{db}\) were declared to be \((\lambda x.\,t)\,s\), then an expression such as \((\lambda x.\,t)[y/r]\,s\) would not be a redex. This notation has a strong connection to proof nets [2].
We write \(\varGamma \vdash _{{{\text {lsc}}}} t:A\) is \(t\) has type \(A\) under the typing context \(\varGamma \), with standard simple type assignment rules. Recall from [19, Theorem 6.11] that simply typed terms are SN:
Theorem 2.2
If \(\varGamma \vdash _{{{\text {lsc}}}} t:A\), there are no infinite reduction sequences \(t\rightarrow _{{\text {lsc}}}t_1 \rightarrow _{{\text {lsc}}}\ldots \).
3 Linear Logic with Restricted Access
We start by defining a one-sided sequent calculus presentation for a linear logic with multiplicative connectives (
, called tensor and par), sharing modalities (\({!} \), \({?} \), called of-course and why-not), and access modalities (\(\bullet \), \(\circ \), called grant and demand), which we dub \(\textsf{MSCLL}\).
Formulae and Sequent Calculus Presentation. We assume given a denumerable set of atomic formulae (\(\alpha ,\beta ,\ldots \)), each of which has a corresponding negative version (\(\overline{\alpha },\overline{\beta },\ldots \)). The set of formulae is given by the grammar:
Linear negation is the involutive operator \((\cdot )^{\perp }\) given by:
Sequents are of the form \(\vdash \varGamma \), where \(\varGamma \) is a finite multiset of formulae (note that we do not include an explicit exchange rule). If \(\varGamma = A_1,\ldots ,A_n\) and \(\mathfrak {m}\) is one of the modalities, we write \(\mathfrak {m}\varGamma \) to stand for \(\mathfrak {m}A_1,\ldots ,\mathfrak {m}A_n\), so for instance \(\circ \varGamma = \circ A_1,\ldots ,\circ A_n\). Derivable sequents are given inductively by the following rules:
Most rules are standard rules from multiplicative-exponential linear logic (\(\textsf{MELL}\)), including the standard weakening (\({?}{\texttt {w}}\)), contraction (\({?}{\texttt {c}}\)), and promotion (\({!}{\texttt {p}}\)) rules. The atypical rule is dereliction (\({?}{\circ \texttt {d}}\)), which requires the conclusion to be \(\varGamma ,{?}{\circ A}\) instead of the usual \(\varGamma ,{?}{A}\). The \(\bullet \) and \(\circ \) rules are (trivial) introduction rules for \(\bullet \) and \(\circ \).
As discussed in the introduction, the intuition is that a proof of \({!}{A}\) lies inside a box which may be duplicated or erased, but it may not necessarily be possible to access the contents of the box, which means that having a proof does not necessarily enable one to interact with its contents. A proof of \({!}{\bullet A}\) lies inside a box which may both duplicated, erased, and accessed. Informally speaking, the combined modalities \({!}{\bullet A}\) and \({?}{\circ A}\) in \(\textsf{MSCLL}\) play the role of the usual \({!}{A}\) and \({?}{A}\) modalities in \(\textsf{MELL}\).
Remark 3.1
If we define linear equivalence of formulae
as usual in linear logic, it is immediate to show that
holds, but in general
does not hold. Hence linear equivalence is not a congruence with respect to the sharing modalities.
Basic Properties. Consider the mapping \({(\cdot )}^{\bullet }\) from formulae in \(\textsf{MELL}\) to formulae in \(\textsf{MSCLL}\) which replaces each occurrence of “\({!} \)” with “\({!}{\bullet }\)”, each occurrence of “\({?} \)” with “\({?}{\circ }\)”, and leaves the other connectives unaltered. The following theorem is easy to prove by induction on the derivation of the sequents:
Theorem 3.1
(Conservativity).\( \vdash \varGamma \) holds in \(\textsf{MELL}\) if and only if \( \vdash {\varGamma }^{\bullet }\) holds in \(\textsf{MSCLL}\)
By the usual techniques, one can show that \(\textsf{MSCLL}\) enjoys cut-elimination:
Theorem 3.2
(Cut elimination). If \(\vdash \varGamma \) is provable in \(\textsf{MSCLL}\), then there is a derivation of \(\vdash \varGamma \) without instances of the \(\texttt {cut} \) rule.
4 A Sharing Linear \(\lambda \)-Calculus
In this section, we present a sharing linear \(\lambda \)-calculus based on \(\textsf{MSCLL}\), called the \(\lambda ^{{!}{\bullet }}\)-calculus. The relationship between the \(\lambda ^{{!}{\bullet }}\)-calculus and \(\textsf{MSCLL}\) is akin to that between linear \(\lambda \)-calculi and \(\textsf{MELL}\). In particular, typing rules for the \(\lambda ^{{!}{\bullet }}\)-calculus are presented in natural deduction (rather than sequent calculus) style, and, furthermore, the \(\lambda ^{{!}{\bullet }}\)-calculus is intuitionistic (rather than classical).
Syntax and Typing System We assume given denumerable sets of linear variables (\(a, b, \ldots \)) and unrestricted variables (\(u, v, \ldots \)). The set of types (\(A,B,\ldots \)) and the set \(\mathcal {T}_{\bullet }\) of \(\lambda ^{{!}{\bullet }}\)-terms (\(t,s,\ldots \)), or just terms, are given by:
A term may be a linear or an unrestricted variable, an abstraction\(\lambda a.\,t\) (binding a linear variable), an application\(t\,s\), an access grant\(\bullet t\), an access request\(\texttt{req}(t)\), a promotion\({!}{t}\) or a substitution\(t[u/s]\) (binding an unrestricted variable).
Free and bound occurrences of variables are defined as expected. We write \(\textsf{fv}(t)\) for the set of free variables of \(t\). Terms are defined up to \(\alpha \)-renaming of bound variables. By convention, we assume that \({!}{t[x/s]}\) stands for \({!}{(t[x/s])}\). Similarly, \(\bullet t[x/s]\), and \(\lambda a.\,t[x/s]\) stand, respectively, for \(\bullet (t[x/s])\), and \(\lambda a.\,(t[x/s])\).
Unrestricted typing environments (\(\varDelta ,\varDelta ',\ldots \)) are partial functions mapping unrestricted variables to types, written \(u_1:A_1,\ldots ,u_n:A_n\). Linear typing environments (\(\varGamma ,\varGamma ',\ldots \)) map linear variables to types, written \(a_1:A_1,\ldots ,a_n:A_n\). We assume that typing environments have finite domain.
Typing judgments are of the form \(\varDelta ;\varGamma \vdash t:A\). Derivable judgments are defined inductively by the following rules. The types of unrestricted variables in \(\varDelta \) may be thought of as being implicitly prefixed by “\({!}{\bullet }\)”, as attested by the rule \(\texttt {sub} \).
\(\lambda a.\,({!}{\bullet {!}{u}})[u/a]\) has type \({!}{\bullet A}\multimap {!}{\bullet {!}{\bullet A}}\), under the empty contexts.
Logical Soundness. Types of \(\lambda ^{{!}{\bullet }}\) encode formulae of \(\textsf{MSCLL}\), while terms encode proofs. Indeed, consider the translation \({(\cdot )^{\star }}\) on types below, and the following result:
Proposition 4.1
(Logical Soundness of\(\lambda ^{{!}{\bullet }}\)). If \(\varDelta ;\varGamma \vdash t:A\) holds in \(\lambda ^{{!}{\bullet }}\), then \(\vdash {?}{\circ ({\varDelta ^{\star }}^{\perp })},{\varGamma ^{\star }}^{\perp },{A^{\star }}\) holds in \(\textsf{MSCLL}\).
Note that, by design, \(\lambda ^{{!}{\bullet }}\) is not intended to be complete with respect to \(\textsf{MSCLL}\). For example, the type \(({!}{\alpha }\multimap {!}{\alpha }\multimap \beta )\multimap {!}{\alpha }\multimap \beta \) is not inhabited in \(\lambda ^{{!}{\bullet }}\), whereas the corresponding formula
is provable in \(\textsf{MSCLL}\).
Reduction Semantics Let us write \(\textsf{Ctxs}_{\bullet }\) for the the set of \(\lambda ^{{!}{\bullet }}\)-contexts (\(\texttt{C},\texttt{C}',\ldots \)), or just contexts, which are \(\lambda ^{{!}{\bullet }}\)-terms with a single occurrence of a hole “\(\Box \)”, and \(\textsf{SCtxs}_{\bullet }\) for the the set of substitution contexts (\(\texttt{L},\texttt{L}',\ldots \)), which are lists of ESs:
We write \(t\{a:=s\}\) for the capture-avoiding substitution of the free occurrences of \(a\) in \(t\) by \(s\). The domain of a substitution context (\(\textsf{dom}(\texttt{L})\)), and the plugging of a term into a context, both with capture (\(\texttt{C}\langle t\rangle \) and \(t\texttt{L}\)) and avoiding capture (\(\texttt{C}\langle \!\langle t\rangle \!\rangle \)), are defined similarly as for the LSC (see Section 2).
There are four rewriting rules, closed by compatibility under arbitrary contexts:
Reduction in \(\lambda ^{{!}{\bullet }}\) is defined as the union \({\rightarrow _{\bullet }} :={\rightarrow _{\mathsf {\bullet db}}\cup \rightarrow _{\mathsf {\bullet req}}\cup \rightarrow _{\mathsf {\bullet ls}}\cup \rightarrow _{\mathsf {\bullet gc}}}\).
The \(\mathsf {\bullet db}\) rule is a distant \(\beta \)-rule. The calculus does not assume that terms are typable; but, in typable terms, there is exactly one occurrence of \(a\) in the body of \(\lambda a.\,t\) by linearity. The \(\mathsf {\bullet req}\) rule requests access to a term. The \(\mathsf {\bullet ls}\) rule substitutes a single occurrence of \(u\) by \((\bullet t)\texttt{L}_1\), provided that \(u\) is bound to a term of the form \(({!}{(\bullet t)\texttt{L}_1})\texttt{L}_2\). Note that the subterm \((\bullet t)\texttt{L}_1\) is copied by \(\mathsf {\bullet ls}\), while \(\texttt{L}_2\) is moved outside so that its bindings remain shared. The \(\mathsf {\bullet gc}\) rule may erase an unused substitution if \(u\) is bound to a term of the form \(({!}{s})\texttt{L}\). Allowing to erase any unused substitution, e.g. with the usual \(\textsf{gc}\) rule of LSC, would break subject reduction, as it could lead to weakening (erasure) of a linear variable.
The \(\mathsf {\bullet gc}\) rule requires that it first be evaluated to a sharable term, of the form \({!}{s'}\), or more in general \(({!}{s'})\texttt{L}\). A sharable term may not, a priori, be accessed. For example, in \((\texttt{req}(u)\,\texttt{req}(u))[u/{!}{v}]\) the two occurrences of \(u\) cannot be substituted by \(v\), because the \(\mathsf {\bullet ls}\) rule requires the argument to be a sharable accessible term, of the form \({!}{\bullet s'}\), or more in general \(({!}{(\bullet s')\texttt{L}_1})\texttt{L}_2\).
A first routine result is:
Proposition 4.2
(Subject Reduction). If \(\varDelta ;\varGamma \vdash t:A\) and \(t\rightarrow _{\bullet }s\), then \(\varDelta ;\varGamma \vdash s:A\).
Confluence. Confluence is tricky since standard techniques are not immediately applicable. A variant of Tait–Martin-Löf’s method [11, § 3.2] would require to define parallel reduction, which is not immediate due to the fact that rewrite rules operate at a distance. The interpretation method, used for confluence of the structural lambda calculus [4], a close relative of LSC, does not apply since full composition, i.e.\(t[x/s] \rightarrow ^* t\{x:=s\}\), does not hold for \(\lambda ^{{!}{\bullet }}\). An axiomatic rewriting approach based on residuals and orthogonality fails for \(\lambda ^{{!}{\bullet }}\) too. A simple example is the following, where we use labels \(\alpha \) and \(\beta \) to mark redexes:
where, however, \(t[v/({!}{\bullet s})\texttt{L}] \ne t[v/{!}{\bullet s}]\texttt{L}\). Nevertheless, confluence holds for \(\lambda ^{{!}{\bullet }}\) modulo the congruence generated by \( t[u/s[v/r]] \equiv t[u/s][v/r] \), provided that \(v\notin \textsf{fv}(t)\). To prove this, we develop a theory of residuals for \(\lambda ^{{!}{\bullet }}\) modulo \(\equiv \). We then resort to the axiomatic rewriting framework due to Melliès [23], verifying that \(\lambda ^{{!}{\bullet }}\) modulo \(\equiv \) can be modeled as an orthogonal axiomatic rewriting system, which entails confluence (see [23, Theorem 2.4]):
Proposition 4.3
(Confluence).\(\lambda ^{{!}{\bullet }}\) modulo \(\equiv \) is confluent.
Strong Normalization. Typable terms in \(\lambda ^{{!}{\bullet }}\) are strongly normalizing. To prove this, we reduce SN of typed \(\lambda ^{{!}{\bullet }}\) to SN of simply typed LSC.
Let us write \(\rightarrow _{\bullet {\text {i}}}\) for \({\rightarrow _{\bullet }}\!\setminus \!{\rightarrow _{\mathsf {\bullet gc}}}\) and \(\rightarrow _{{\text {lsc}}{\text {i}}}\) for \({\rightarrow _{{\text {lsc}}}}\!\setminus \!{\rightarrow _{\mathsf {\bullet gc}}}\). Garbage collection \(\rightarrow _{\mathsf {\bullet gc}}\) can be postponed, so to show there are no infinite reduction sequences \(t\rightarrow _{\bullet }t_1 \rightarrow _{\bullet }t_2 \ldots \) we may assume without loss of generality that the sequence consists of \(\rightarrow _{\bullet {\text {i}}}\) steps.
We start by defining a translation \([\![\cdot ]\!]\) from \(\lambda ^{{!}{\bullet }}\) to LSC. Let 1 be any inhabited type in simply typed LSC, and \({*}\) a closed inhabitant of 1 in normal form. Types and terms are translated as follows (where \(z\) is assumed to be fresh in the “\(\bullet \)” case):
An unrestricted variable \(u:A\) in the environment is translated as \(u: {\textbf {1}}\rightarrow [\![A]\!]\), while a linear variable \(a:A\) is translated as \(a:[\![A]\!]\). It is easy to show that the translation preserves typing, in the sense that \(\varDelta ;\varGamma \vdash t:A\) implies \([\![\varDelta ]\!],[\![\varGamma ]\!]\vdash _{{{\text {lsc}}}} [\![t]\!]:[\![A]\!]\).
To conclude, it would suffice to show that LSC simulates \(\lambda ^{{!}{\bullet }}\) reduction; more precisely that \(t\rightarrow _{\bullet }s\) implies \([\![t]\!] \rightarrow _{{\text {lsc}}}^+ [\![s]\!]\). Unfortunately, this is not the case; for instance, in the following example, the \(\rightarrow _{\mathsf {\bullet ls}}\) rule of \(\lambda ^{{!}{\bullet }}\)extrudes the \([y/z]\) outside to share the binding, while the \(\rightarrow _{\textsf{ls}}\) rule of LSC makes a copy of \([y/z]\):
To address this, we define a binary relation \({\Rrightarrow }\) on LSC terms called fusion, that allows to “extrude and fuse” ESs, given by the reflexive, transitive, and contextual closure of the following rules, avoiding capture:
The two key technical properties are, first, that the \(\rightarrow _{{\text {lsc}}{\text {i}}}\) simulates \(\rightarrow _{\bullet {\text {i}}}\) up to fusion, more precisely that \(t\rightarrow _{\bullet {\text {i}}}s\) implies \([\![t]\!] \rightarrow _{{\text {lsc}}{\text {i}}}^+\Rrightarrow [\![s]\!]\). Second, that fusion can be postponed, i.e. that \({\Rrightarrow \rightarrow _{\bullet {\text {i}}}} \subseteq {\rightarrow _{\bullet {\text {i}}}^+\Rrightarrow }\). Thus an infinite reduction sequence \(t\rightarrow _{\bullet {\text {i}}}t_1 \rightarrow _{\bullet {\text {i}}}t_2 \ldots \) can be mapped to \([\![t]\!] \rightarrow _{{\text {lsc}}{\text {i}}}^+\Rrightarrow [\![t_1]\!] \rightarrow _{{\text {lsc}}{\text {i}}}^+\Rrightarrow [\![t_2]\!] \ldots \) and by postponing fusion we obtain an infinite reduction in LSC. If \(t\) is typable in \(\lambda ^{{!}{\bullet }}\) then \([\![t]\!]\) is typable in LSC, contradicting Thm. 2.2. To sum up:
Theorem 4.1
(Termination). If \(t\) is typable in \(\lambda ^{{!}{\bullet }}\) then \(t\) is \(\rightarrow _{\bullet }\)-SN.
To conclude this section, we remark that \(\rightarrow _{\bullet }\)-normal forms can be characterized inductively. We omit the characterization for lack of space, but see Section ?? for details.
5 Embedding \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\) and \({{\textsf{CBS}}}\)
In this section, we recall known \({{\textsf{CBN}}}\) and \({{\textsf{CBV}}}\) calculi, and we introduce a sharing variant of call-by-name we dub call-by-sharing (\({{\textsf{CBS}}}\)). Second, we define translations that provide embeddings into \(\lambda ^{{!}{\bullet }}\), and study their properties.
Our first step is to give precise definitions of each of the calculi we will work with. These calculi operate on LSC terms, and some of them also use the notions of strict values (\(\texttt{v},\texttt{w},\ldots \)) and lax values (\(\texttt{v}^\texttt {+ },\texttt{w}^\texttt {+ },\ldots \)), defined as follows:
We define the following rewriting rules on LSC terms, closed by compatibility under arbitrary contexts:
Definition 5.1
(Notions of reduction). The relations corresponding to \({{\textsf{CBN}}}\) (
), \({{\textsf{CBV}}}\) (
), and \({{\textsf{CBS}}}\) (
) reduction are defined by:
The call-by-name (\({{\textsf{CBN}}}\)) calculus
corresponds to usual reduction in LSC [3].
The call-by-value (\({{\textsf{CBV}}}\)) calculus
is a variant of Accattoli and Paolini’s value-substitution calculus [5] (VSC), with two differences. First, the rule \(\rightarrow _{\textsf{lsv}}\) is linear in that it substitutes one occurrence of a variable \(x\) at a time, while the corresponding rule of VSC substitutes all occurrences of \(x\) at once. This difference allows us to present the calculi in a uniform way. Second, \(\rightarrow _{\textsf{lsv}}\) allows substituting variables for strict values (abstractions), while VSC allows substituting lax values (both abstractions and variables). This is necessary to be able to define a complete embedding (see also Rem. 5.2).
The call-by-sharing (\({{\textsf{CBS}}}\)) calculus
is a sharing variant of \({{\textsf{CBN}}}\), in which the argument may be discarded without being evaluated (using \(\textsf{gc}\)). At the same time, the evaluation of the argument is shared, in the sense that \(\textsf{lsw}\) only allows copying arguments when they have been evaluated to the form \(\texttt{v}\texttt{L}\). The \({{\textsf{CBS}}}\) calculus bears a strong resemblance to the call-by-need \(\lambda \)-calculus of Ariola et al. [6], which can be obtained by changing \(\rightarrow _{\textsf{lsw}}\) to \(\rightarrow _{\textsf{lsv}}\), i.e. call-by-need is
(see for instance [8]). Note that \({{\textsf{CBS}}}\) achieves less sharing that \({{\textsf{CBNd}}}\), because the \(\rightarrow _{\textsf{lsw}}\) rule makes two copies of \(\texttt{L}\), whereas \(\rightarrow _{\textsf{lsv}}\) keeps a single shared copy of \(\texttt{L}\). Unfortunately, it does not seem possible to give a sound embedding of \({{\textsf{CBNd}}}\) into \(\lambda ^{{!}{\bullet }}\).
Remark 5.1
The reduction relations above are calculi, i.e. orientations of equational theories, not evaluation mechanisms. We shall turn our attention to evaluation in Section 6.
Next, we describe the translations
, and
. Each translation maps a simple type into a \(\lambda ^{{!}{\bullet }}\)-type, an LSC term into a \(\lambda ^{{!}{\bullet }}\)-term, and an LSC typing judgment into an \(\lambda ^{{!}{\bullet }}\) typing judgment.
Embedding Call-by-Name The \({{\textsf{CBN}}}\) translation
is defined on types and terms by:
In the abstraction case, \(a\) is assumed to be fresh, i.e.
. The translation is extended to typing environments:
, and judgments:
.
Proposition 5.1
(\({{\textsf{CBN}}}\)typing). If \(\varGamma \vdash t:A\) then
.
Lemma 5.1
(\({{\textsf{CBN}}}\)simulation). If
then
. Furthermore, the reduction uses either at least one, and at most two \(\rightarrow _{\bullet }\) steps.
Proof
By induction on the derivation of
. The interesting cases are when there is a \(\textsf{db}\), \(\textsf{ls}\), or \(\textsf{gc}\) step at the root. If \((\lambda x.\,t)\texttt{L}\,s\rightarrow _{\textsf{db}}t[x/s]\texttt{L}\), then:
If \(t[x/s] \rightarrow _{\textsf{gc}}t\) with \(x\notin \textsf{fv}(t)\), then
, where that
because
. \(\blacksquare \)
For completeness, we define an inverse\({{\textsf{CBN}}}\)translation. We define a subset
, containing the closure by \(\rightarrow _{\bullet }\)-reduction of the image of
:
where, in the production \(\underline{t}\,{:}{:=}\, \lambda a.\,\underline{t}[u/a]\) we assume that \(a\) is fresh, that is, \(a\notin \textsf{fv}(\underline{t})\). The inverse\({{\textsf{CBN}}}\)translation is a function
defined as follows, by induction on the derivation of a term with the grammar above4.
It is easy to check that
is the left-inverse of
, i.e. if \(t\in \mathcal {T}_{\textsf{LSC}}\) then
and
. Moreover:
Lemma 5.2
(Inverse\({{\textsf{CBN}}}\)simulation). Let
and \(s\in \mathcal {T}_{\bullet }\) such that \(\underline{t}\rightarrow _{\bullet }s\). Then
and
.
Using the abstract soundness and completeness results (Prop. 2.1, Thm. 2.1) together with the lemmas above, we obtain:
Theorem 5.1
(Sound and complete\({{\textsf{CBN}}}\)embedding). Given terms \(t,s\in \mathcal {T}_{\textsf{LSC}}\),
if and only if
. Moreover, \(t\) is in
-normal form iff
is in \(\rightarrow _{\bullet }\)-normal form.
Embedding Call-by-Value The \({{\textsf{CBV}}}\) translation
is defined on types and terms by:
where, as for \({{\textsf{CBN}}}\), \(a\) is assumed to be fresh in the abstraction case. The translation is extended to typing environments:
, and judgments:
.
Proposition 5.2
(\({{\textsf{CBV}}}\)typing). If \(\varGamma \vdash t:A\) then
.
Lemma 5.3
(\({{\textsf{CBV}}}\)simulation). If
then
. Furthermore, the reduction uses at least one, and at most four \(\rightarrow _{\bullet }\) steps.
We turn our attention to completeness for
. A first comment is that the \({{\textsf{CBV}}}\) translation only turns out to be complete up to garbage collection. More precisely, soundness with respect to reduction holds, in the sense that
implies
, but completeness only holds in the following weak form:
implies
, where
. Resorting to confluence, it is possible recover “plain” soundness and completeness of the translation, i.e. with respect to the equational theory and not to reduction; more precisely
if and only if
. Besides:
Remark 5.2
The study of completeness motivates the fact that in CBV the \(\textsf{ls}\) rule can substitute only strict values (abstractions) while the \(\mathsf {gcv\texttt {+ }}\) rule can erase lax values (abstractions and variables). To allow substituting variables, the translation of a variable \(x\) should be a term of the form \({!}{\bullet t}\). A preliminary version of this work used a CBV translation
similar to
but with
. However,
is not complete. In fact, it can be checked
does not hold in general (because \(t\) may not be convertible to a value), while it can be seen that
always holds. On the other hand, if the \(\mathsf {gcv\texttt {+ }}\) rule were not allowed to erase variables, this would again lead to incompleteness, as
would not hold, but
would hold, since
.
Next, we define an inverse\({{\textsf{CBV}}}\)translation. First, we define a subset
, containing the closure by \(\rightarrow _{\bullet }\)-reduction of the image of
, as well as a subset
:
where in the occurrences of \(\lambda a.\,\underline{t}[x/a]\) we assume that \(a\) is fresh. The inverse\({{\textsf{CBV}}}\)translation is a function
defined as follows, by induction on the derivation of a term with the (unambiguous) grammar above:
It is easy to check that
is the left-inverse of
.
Lemma 5.4
(Inverse\({{\textsf{CBV}}}\)simulation, up to\(\mathsf {gcv\texttt {+ }}\)). Let
and \(s\in \mathcal {T}_{\bullet }\) such that \(\underline{t}\rightarrow _{\bullet }s\). Then
and
, where
.
Theorem 5.2
(Sound and complete\({{\textsf{CBV}}}\)embedding). Given terms \(t,s\in \mathcal {T}_{\textsf{LSC}}\):
1.
implies
2.
implies
where
.
3.
if and only if
4.
\(t\) is in
-normal form iff
is in \(\rightarrow _{\bullet }\)-normal form.
Remark 5.3
Arrial [7] suggests an additional \({{\textsf{CBV}}}\) translation mapping \(A\rightarrow B\) to \({!}{(A\multimap {!}{B})}\). In our setting, this means mapping \(A\rightarrow B\) to \({!}{\bullet (A\multimap {!}{\bullet B})}\). This translation is also sound and complete but still requires
to obtain completeness.
Embedding Call-by-Sharing The \({{\textsf{CBS}}}\) translation
is defined on types and terms by:
where, as before, \(a\) is assumed to be fresh in the abstraction case. The translation is extended to typing environments:
, and judgments:
.
Proposition 5.3
(\({{\textsf{CBS}}}\)typing). If \(\varGamma \vdash t:A\) then
.
Lemma 5.5
(\({{\textsf{CBS}}}\)simulation). If
then
.
Proof
By induction on the derivation of
. The interesting cases are when there is a \(\textsf{db}\), \(\textsf{lsv}\), or \(\textsf{gc}\) step at the root.
If \((\lambda x.\,t)\texttt{L}\,s\rightarrow _{\textsf{db}}t[x/s]\texttt{L}\), then:
If \(\texttt{C}\langle \!\langle x\rangle \!\rangle [x/\texttt{v}\texttt{L}] \rightarrow _{\textsf{lsw}}\texttt{C}\langle \!\langle \texttt{v}\texttt{L}\rangle \!\rangle [x/\texttt{v}\texttt{L}]\), note that \(\texttt{v}= \lambda y.\,t\) so
. Then:
If \(t[x/s] \rightarrow _{\textsf{gc}}t\), where \(x\notin \textsf{fv}(t)\), then
, where
because
. \(\blacksquare \)
For completeness, we define an inverse\({{\textsf{CBS}}}\)translation. First, we define a subset
, containing the closure by \(\rightarrow _{\bullet }\)-reduction of the image of
, as well as a subset
, as follows:
where, in the productions involving a subterm of the form \(\lambda a.\,\underline{t}[x/a]\), we assume that \(a\) is fresh, that is, \(a\notin \textsf{fv}(\underline{t})\).
The inverse\({{\textsf{CBS}}}\)translation is a function
defined as follows, by induction on the derivation of a term with the (unambiguous) grammar above:
It is easy to check that
is the left-inverse of
.
Lemma 5.6
(Inverse\({{\textsf{CBS}}}\)simulation). Let
and \(s\in \mathcal {T}_{\bullet }\) such that \(\underline{t}\rightarrow _{\bullet }s\). Then
and
.
Theorem 5.3
(Sound and complete\({{\textsf{CBS}}}\)embedding). Let \(t,s\in \mathcal {T}_{\textsf{LSC}}\). Then
if and only if
. Moreover, \(t\) is in
-normal form iff
is in \(\rightarrow _{\bullet }\)-normal form.
As previously mentioned, it does not seem possible to embed Wadsworth’s call-by-need (i.e.\({{\textsf{CBNd}}}\)) in \(\lambda ^{{!}{\bullet }}\). One could imagine a variant of \(\lambda ^{{!}{\bullet }}\) that includes the following \(\mathsf {\bullet ls}'\) rule rather than \(\mathsf {\bullet ls}\):
The resulting calculus allows embeddings from \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBNd}}}\). However, it is not well-behaved, as confluence fails. Let \(\varOmega :=(\lambda a.\,a\,a)\,(\lambda a.\,a\,a)\). For example, \(x[y/{!}{u}][u/{!}{(\bullet v)[v/\varOmega ]}] \rightarrow _{\mathsf {\bullet gc}} x[u/{!}{(\bullet v)[v/\varOmega ]}] \rightarrow _{\mathsf {\bullet gc}}x\). But also \(x[y/{!}{u}][u/{!}{(\bullet v)[v/\varOmega ]}] \rightarrow _{\mathsf {\bullet ls}} x[y/{!}{\bullet v}][u/{!}{(\bullet v)}][v/\varOmega ] \rightarrow _{\mathsf {\bullet gc}} x[u/{!}{(\bullet v)}][v/\varOmega ] \rightarrow _{\mathsf {\bullet gc}} x[v/\varOmega ]\).
6 Simulating Weak Evaluation Strategies
In Section 5, we have shown that \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBS}}}\) calculi can be embedded in the \(\lambda ^{{!}{\bullet }}\)-calculus. Reduction in these calculi is intended to capture equivalence, rather than evaluation, of programs. That is, these calculi are orientations of \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBS}}}\) equational theories rather than evaluation mechanisms.
Reduction in the calculi of Section 5 is closed by arbitrary contexts. E.g. in the \({{\textsf{CBV}}}\)calculus, a step
is allowed if
, while typically call-by-value evaluation would proceed to contract the outermost redex.
In this section, we first define weak evaluation relations
, and
for \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBS}}}\) respectively. Recall that evaluation is called weak if it does not proceed inside the bodies of \(\lambda \)-abstractions. Second, we define an evaluation relation \(\rightsquigarrow \) for \(\lambda ^{{!}{\bullet }}\), which is also “weak” in that it does not reduce inside \(\lambda \)-abstractions, boxes (\(\bullet \)), nor promotions (\({!} \)). Finally, we show that evaluation according to
, and
can be simulated by \(\rightsquigarrow \) via the translations already introduced in Section 5.
Weak\({{\textsf{CBN}}}\)Evaluation The one-step weak \({{\textsf{CBN}}}\) evaluation judgment is of the form
, where \(t,t' \in \mathcal {T}_{\textsf{LSC}}\) and the set of \({{\textsf{CBN}}}\)-rulenames (\(\rho ,\rho ',\ldots \)) is given by \( \rho \,{:}{:=}\, \textsf{db}\mid \mathsf {\varsigma }(x,t) \mid \textsf{ls}\mid \textsf{gc}\). Weak \({{\textsf{CBN}}}\) evaluation is the union
, excluding auxiliary \(\mathsf {\varsigma }(x,t)\) steps. It is defined by the following inductive rules:
The
, and
rules derive root reduction steps. The
and
rules correspond to congruence closure below weak head evaluation contexts. The side condition in the
rule is to avoid unwanted variable capture. The somewhat atypical
rule derives steps of the form
, which substitute a single free occurrence of \(x\) (in evaluation position) by \(s\). This rule works in synchrony with
to allow \(\textsf{ls}\) steps: for example,
and
. This is inspired the formulation of strong call-by-need of Balabonski et al. [9].
It is straightforward to show that
. Note also that
is non-deterministic, although confluent. The source of non-determinism is that \(\textsf{gc}\) steps can be performed in any order. For example \(((\lambda x.\,x)\,y)[z/s]\) reduces both with a \(\textsf{db}\) and with a \(\textsf{gc}\) step.
Weak\({{\textsf{CBV}}}\)Evaluation The one-step weak \({{\textsf{CBV}}}\) evaluation judgment is of the form
, where \(t,t' \in \mathcal {T}_{\textsf{LSC}}\) and the set of \({{\textsf{CBV}}}\)-rulenames (\(\rho ,\rho ',\ldots \)) is given by \( \rho \,{:}{:=}\, \textsf{db}\mid \mathsf {\varsigma }(x,\texttt{v}) \mid \textsf{lsv}\mid \mathsf {gcv\texttt {+ }}\). Weak \({{\textsf{CBV}}}\) evaluation is
, excluding auxiliary \(\mathsf {\varsigma }(x,\texttt{v})\) steps. It is defined by the following inductive rules:
Similar remarks as for \({{\textsf{CBN}}}\) apply, in particular
. Rules
, and
are root reduction rules, while
, and
correspond to congruence closure rules. The
rule plays a similar role as the analogue rule in \({{\textsf{CBN}}}\), but only allows substituting variables for strict values. In this notion of \({{\textsf{CBV}}}\) evaluation, arguments of applications are not evaluated. The restriction that the argument is a value is not imposed to contract a \(\beta \)-like redex, but rather to perform the substitution. These ideas can already be found in the \(\lambda _{CBV}\)-calculus of [18]. Note that in \({{\textsf{CBV}}}\) evaluation (
) there is a second source of non-determinism, namely that
and
overlap, so the body and the argument of an ES can be evaluated concurrently.
Weak\({{\textsf{CBS}}}\)Evaluation The one-step weak \({{\textsf{CBS}}}\) evaluation judgment is of the form
, where \(t,t' \in \mathcal {T}_{\textsf{LSC}}\) and the set of \({{\textsf{CBS}}}\)-rulenames (\(\rho ,\rho ',\ldots \)) is given by \( \rho \,{:}{:=}\, \textsf{db}\mid \mathsf {\varsigma }(x,\texttt{v}\texttt{L}) \mid \mathsf {\iota }(x) \mid \textsf{lsw}\mid \textsf{gc}\). Weak \({{\textsf{CBS}}}\) evaluation is the union
, excluding auxiliary \(\mathsf {\varsigma }(x,\texttt{v}\texttt{L})\) and \(\mathsf {\iota }(x)\) steps. It is defined by the following inductive rules:
Similar remarks as for \({{\textsf{CBN}}}\) apply, in particular
. Rules
, and
are root reduction rules, while
, and
are congruence closure rules. The rule
plays a similar role as the analogue rules in \({{\textsf{CBN}}}\) and \({{\textsf{CBV}}}\), but only allows substituting variables for terms of the form \(\texttt{v}\texttt{L}\) (known as answers in the literature). The rule
is a variant of
that acts on the argument of an ES; this rule is not strictly necessary for evaluation, but it is crucial for the embedding into \(\lambda ^{{!}{\bullet }}\) to be complete. The
rule is used in synchrony with the congruence rules to derive steps that are always of the form
indicating that \(x\) occurs in \(t\) in an evaluation position. This is used to check whether \(x\) it a needed variable. For example,
and
, so the fact that \(x\) is needed on the left triggers the evaluation of the argument:
. From this, one obtains the substitution step
.
Weak\(\lambda ^{{!}{\bullet }}\)-Calculus Evaluation The one-step weak \(\lambda ^{{!}{\bullet }}\) evaluation judgment is of the form \(t\rightsquigarrow _{\rho } t'\), where \(t,t'\in \mathcal {T}_{\bullet }\), and the set of rulenames (\(\rho ,\rho ',\ldots \)) is given by \( \rho \,{:}{:=}\, \mathsf {\bullet db}\mid \mathsf {\varsigma }(u,(\bullet t)\texttt{L}) \mid \mathsf {\iota }(u) \mid \mathsf {\bullet ls}\mid \mathsf {\bullet gc}\mid \mathsf {\bullet req}\). Weak \(\lambda ^{{!}{\bullet }}\) evaluation is the union \({\rightsquigarrow } :={\rightsquigarrow _{\mathsf {\bullet db}} \cup \rightsquigarrow _{\mathsf {\bullet ls}} \cup \rightsquigarrow _{\mathsf {\bullet gc}}}\), excluding auxiliary \(\mathsf {\varsigma }(x,\texttt{v}\texttt{L})\) and \(\mathsf {\iota }(x)\) steps. It is defined by the following inductive rules:
Weak \(\lambda ^{{!}{\bullet }}\) evaluation is a sub-ARS of \(\lambda ^{{!}{\bullet }}\), in the sense that \({\rightsquigarrow } \subseteq {\rightarrow _{\bullet }}\). Rules
, and
are root reduction rules, while
, and
are congruence rules. Rule
plays a similar role as the analogue rules in \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBNd}}}\), but only allows substituting a variable by a term of the form \((\bullet t)\texttt{L}\). Rule
plays a similar role as the analogue rule in \({{\textsf{CBNd}}}\), used to check whether a variable is in evaluation position. Note that there are no congruence rules below \(\lambda \)-abstraction, box (\(\bullet \)), nor promotion (\({!} \)). Evaluation can proceed below promotion in two particular cases. First, the
rule allows to perform substitution immediately below a promotion; for instance \(({!}{u})[u/{!}{\bullet v}] \rightsquigarrow _{\mathsf {\bullet ls}} ({!}{\bullet v})[u/{!}{\bullet v}]\). Second, the
rule allows evaluation below a promotion when a term is the argument of a “needed” substitution; for instance \((uv)[u/{!}{((\lambda a.\,a)(\bullet w))}] \rightsquigarrow _{\mathsf {\bullet db}} (uv)[u/{!}{\bullet w}] \rightsquigarrow _{\mathsf {\bullet ls}} ((\bullet w)v)[u/{!}{\bullet w}] \).
The \(\lambda ^{{!}{\bullet }}\)-calculus is designed with the goal in mind of providing a unifying framework for call-by-name, call-by-value, and call-by-sharing. As a matter of fact, weak \(\lambda ^{{!}{\bullet }}\) evaluation simulates weak \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBS}}}\) evaluation via the
, and
translations introduced in Section 5:
Theorem 6.1
(Simulation and inverse simulation of evaluation).
In the \({{\textsf{CBV}}}\) case, completeness only holds for an extended relation
, defined as
but adding an inverse garbage collection rule that derives
.
7 Related Work and Conclusions
Related Work. The seminal work [22] is the first work to have related Girard’s embeddings of intuitionistic logic into \(\textsf{LL}\) with evaluation mechanisms5. Call-by-push-value (\({{\textsf{CBPV}}}\)) [20, 21] is a calculus that distinguishes values from computations and allows to subsume both the \({{\textsf{CBV}}}\) and \({{\textsf{CBN}}}\) evaluation mechanisms. Ehrhard [14] studied the connection between \({{\textsf{CBPV}}}\) [20, 21] and \(\textsf{LL}\), producing a calculus which was later modified to become the Bang-calculus [15]. \({{\textsf{CBV}}}\) and \({{\textsf{CBN}}}\) translations to the Bang-calculus were studied in [15]. Soundness and completeness of these translations with respect to reduction was proved by Guerrieri and Manzonetto [17] for a slightly different notion of reduction for the Bang-calculus than that of [15]. The \({{\textsf{CBV}}}\) translation does not preserve normal forms; an amended translation that does was studied in [12, 13]. Intuitionistic truth in terms of classical provability underlies Gödel’s embedding of intuitionistic logic into (classical) S4. In [27], the authors consider a program similar to that of \({{\textsf{CBPV}}}\) but where that target language is a modal lambda calculus. Promotion and derelection are recast as boxing and unboxing and \({{\textsf{CBV}}}\) and \({{\textsf{CBN}}}\) are described in terms of a so called call-by-box evaluation mechanism [27].
Conclusions. This work introduces \(\textsf{MSCLL}\), a Sharing Linear Logic. It arises from splitting each exponential modality (\({!} /{?} \)) into a sharing modality (\({!} /{?} \)) and a cloning modality (\(\bullet /\circ \)). \(\textsf{MSCLL}\) is conservative over \(\textsf{MELL}\) and enjoys cut-elimination. The usual embeddings of intuitionistic logic into \(\textsf{LL}\) can be restated in the setting of \(\lambda ^{{!}{\bullet }}\), a Sharing Linear \(\lambda \)-calculus derived from \(\textsf{MSCLL}\). The decomposition of the of-course modality allows us to define an embedding of intuitionistic logic into \(\lambda ^{{!}{\bullet }}\), corresponding to a call-by-need\(\lambda \)-calculus \({{\textsf{CBS}}}\). The following table summarizes the, sound and complete, embeddings studied in Section 5:
A weak evaluation mechanism can be defined for \(\lambda ^{{!}{\bullet }}\) that simulates weak evaluation in the original calculi in a sound and complete way. Moreover, \(\textsf{MSCLL}\) also admits a sound and complete embedding of the Bang-calculus (see the companion report [10]).
There are several avenues worth pursuing. First, developing an appropriate notion of proof nets and semantics for \(\textsf{MSCLL}\), which perhaps would help clarify the somewhat intriguing interaction between the sharing and access modalities. Second, studying operational properties of the \(\lambda ^{{!}{\bullet }}\)-calculus such as standardization (as developed for LSC [3]) and solvability. Additionally, one can consider extending weak evaluation in \(\lambda ^{{!}{\bullet }}\) to strong evaluation, to simulate strong \({{\textsf{CBN}}}\)/\({{\textsf{CBV}}}\)/\({{\textsf{CBS}}}\) evaluation. Also, our use of multiple exponentials is reminiscent of subexponentials [25], where instead of one pair of of-course and why-not modalities one introduces a family of them, each of which cannot be proven equivalent to any other. Further work is required to determine if there is a rigorous connection with subexponentials.
It should be noted that our original motivation to study \(\textsf{MSCLL}\) was to try to provide a unified logical account of \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBNd}}}\). In [22], an attempt was made at embedding \({{\textsf{CBNd}}}\) in a linear \(\lambda \)-calculus, but the target language had to be changed to become affine, allowing weakening of arbitrary propositions.
Acknowledgments
The first author was partially supported by project grants PUNQ 2219/22 and PICT-2021-I-INVI-00602.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Sometimes the second embedding is defined as mapping \(A\rightarrow B\) to \({!}{(A\multimap B)}\). This is just an apparent difference, which is canceled out by adjusting the translation of sequents accordingly.
Girard’s original translations target Linear Logic presented in sequent calculus style. We follow here Maraist et al. [22], in which the target language is presented as a linear \(\lambda \)-calculus, in natural deduction style.
operates on formulae by mapping
to
. It operates on terms in such a way that a \(\lambda \)-calculus application \(t\,s\) is mapped to
in a linear \(\lambda \)-calculus2. Here “\({!} \)” is a term constructor, which corresponds to an instance of the \({!} \)-introduction rule, also called promotion. The key point is that the argument \(s\) of an application is prefixed with “\({!} \)”. This enables the (arbitrary) term
to be freely copied or discarded in
, as dictated by \({{\textsf{CBN}}}\). In this sense, the first translation provides a logical foundation for the \({{\textsf{CBN}}}\) evaluation mechanism.
operates on formulae by mapping the intuitionistic implication \(A\rightarrow B\) to
. It operates on terms in such a way that a \(\lambda \)-calculus application \(t\,s\) is mapped to
. Here, \(\texttt{der}(\cdot )\) stands for an appropriate operation in the target language that corresponds to the \({!} \)-elimination rule, also called dereliction. The key point is that the argument is not prefixed with “\({!} \)”, which means that it must be evaluated before being consumed, as dictated by \({{\textsf{CBV}}}\). This translation prefixes values, such as \(\lambda x.\,r\), with a promotion, resulting in
. Consequently, only values will end up being copied or discarded.
operates on formulae by mapping \(A\rightarrow B\) to
. It operates on terms by mapping a \(\lambda \)-calculus application \(t\,s\) to
, indicating that the argument may be freely copied, discarded, and accessed. This mimics the original translation of \({{\textsf{CBN}}}\) to \(\textsf{LL}\). Our \({{\textsf{CBV}}}\) translation
operates on formulae by mapping \(A\rightarrow B\) to
. It operates on terms by leaving the translation of the argument of an application intact, mapping \(t\,s\) to
. As before, \(\texttt{der}(\cdot )\) is an appropriate operator corresponding to \({!} \)-elimination, while \(\texttt{req}(\cdot )\) stands for \(\bullet \)-elimination. At the same time, the translation maps values such as \(\lambda x.\,t\) (roughly3) to
. Thus an argument
cannot be copied, discarded, or accessed at all unless later, after further evaluation, it takes the form \({!}{\bullet \texttt{v}}\), for some value \(\texttt{v}\), in which case \(\texttt{v}\) can be copied. This too mimics the original translation from \({{\textsf{CBV}}}\) to \(\textsf{LL}\). The \({{\textsf{CBN}}}\) and \({{\textsf{CBV}}}\) translations are proved to be sound and complete, in the sense that two \(\lambda \)-terms are interconvertible in the source language if and only if they are mapped to interconvertible terms in the target language.
that maps \(A\rightarrow B\) to
. This translation cannot be expressed directly in a linear \(\lambda \)-calculus, because the “\(\bullet \)” modality is used as a stand-alone operator. A \(\lambda \)-calculus application \(t\,s\) is now mapped to
, meaning that the argument can be copied and discarded, but not accessed yet. A value such as \(\lambda x.\,r\) is now (roughly) mapped to
. Thus an argument
cannot be accessed unless, after further evaluation, it takes the form \(\bullet \texttt{v}\), for some value \(\texttt{v}\), in which case \(\texttt{v}\) can be accessed. The fact that arguments cannot be accessed until they become values means that the evaluation mechanism can keep references to a single shared copy of the argument, until it becomes accessible. This translation suggests an evaluation mechanism that we dub call-by-sharing (\({{\textsf{CBS}}}\)).
, called tensor and par), sharing modalities (\({!} \), \({?} \), called of-course and why-not), and a ccess modalities (\(\bullet \), \(\circ \), called grant and demand), which we dub \(\textsf{MSCLL}\).
as usual in linear logic, it is immediate to show that
holds, but in general
does not hold. Hence linear equivalence is not a congruence with respect to the sharing modalities.
is provable in \(\textsf{MSCLL}\).
), \({{\textsf{CBV}}}\) (
), and \({{\textsf{CBS}}}\) (
) reduction are defined by: 
corresponds to usual reduction in 
is a variant of Accattoli and Paolini’s value-substitution calculus [5] (VSC), with two differences. First, the rule \(\rightarrow _{\textsf{lsv}}\) is linear in that it substitutes one occurrence of a variable \(x\) at a time, while the corresponding rule of VSC substitutes all occurrences of \(x\) at once. This difference allows us to present the calculi in a uniform way. Second, \(\rightarrow _{\textsf{lsv}}\) allows substituting variables for strict values (abstractions), while VSC allows substituting lax values (both abstractions and variables). This is necessary to be able to define a complete embedding (see also Rem. 5.2).
is a sharing variant of \({{\textsf{CBN}}}\), in which the argument may be discarded without being evaluated (using \(\textsf{gc}\)). At the same time, the evaluation of the argument is shared, in the sense that \(\textsf{lsw}\) only allows copying arguments when they have been evaluated to the form \(\texttt{v}\texttt{L}\). The \({{\textsf{CBS}}}\) calculus bears a strong resemblance to the call-by-need \(\lambda \)-calculus of Ariola et al. [6], which can be obtained by changing \(\rightarrow _{\textsf{lsw}}\) to \(\rightarrow _{\textsf{lsv}}\), i.e. call-by-need is
(see for instance [8]). Note that \({{\textsf{CBS}}}\) achieves less sharing that \({{\textsf{CBNd}}}\), because the \(\rightarrow _{\textsf{lsw}}\) rule makes two copies of \(\texttt{L}\), whereas \(\rightarrow _{\textsf{lsv}}\) keeps a single shared copy of \(\texttt{L}\). Unfortunately, it does not seem possible to give a sound embedding of \({{\textsf{CBNd}}}\) into \(\lambda ^{{!}{\bullet }}\).
, and
. Each translation maps a simple type into a \(\lambda ^{{!}{\bullet }}\)-type, an LSC term into a \(\lambda ^{{!}{\bullet }}\)-term, and an LSC typing judgment into an \(\lambda ^{{!}{\bullet }}\) typing judgment.
is defined on types and terms by: 
. The translation is extended to typing environments:
, and judgments:
.
.
then
. Furthermore, the reduction uses either at least one, and at most two \(\rightarrow _{\bullet }\) steps.
. The interesting cases are when there is a \(\textsf{db}\), \(\textsf{ls}\), or \(\textsf{gc}\) step at the root. If \((\lambda x.\,t)\texttt{L}\,s\rightarrow _{\textsf{db}}t[x/s]\texttt{L}\), then: 
, where that
because
. \(\blacksquare \)
, containing the closure by \(\rightarrow _{\bullet }\)-reduction of the image of
:where, in the production \(\underline{t}\,{:}{:=}\, \lambda a.\,\underline{t}[u/a]\) we assume that \(a\) is fresh, that is, \(a\notin \textsf{fv}(\underline{t})\). The inverse \({{\textsf{CBN}}}\) translation is a function
defined as follows, by induction on the derivation of a term with the grammar above4. 
is the left-inverse of
, i.e. if \(t\in \mathcal {T}_{\textsf{LSC}}\) then
and
. Moreover:
and \(s\in \mathcal {T}_{\bullet }\) such that \(\underline{t}\rightarrow _{\bullet }s\). Then
and
.
if and only if
. Moreover, \(t\) is in
-normal form iff
is in \(\rightarrow _{\bullet }\)-normal form.
is defined on types and terms by: 
, and judgments:
.
.
then
. Furthermore, the reduction uses at least one, and at most four \(\rightarrow _{\bullet }\) steps.
. A first comment is that the \({{\textsf{CBV}}}\) translation only turns out to be complete up to garbage collection. More precisely, soundness with respect to reduction holds, in the sense that
implies
, but completeness only holds in the following weak form:
implies
, where
. Resorting to confluence, it is possible recover “plain” soundness and completeness of the translation, i.e. with respect to the equational theory and not to reduction; more precisely
if and only if
. Besides:
similar to
but with
. However,
is not complete. In fact, it can be checked
does not hold in general (because \(t\) may not be convertible to a value), while it can be seen that
always holds. On the other hand, if the \(\mathsf {gcv\texttt {+ }}\) rule were not allowed to erase variables, this would again lead to incompleteness, as
would not hold, but
would hold, since
.
, containing the closure by \(\rightarrow _{\bullet }\)-reduction of the image of
, as well as a subset
:where in the occurrences of \(\lambda a.\,\underline{t}[x/a]\) we assume that \(a\) is fresh. The inverse \({{\textsf{CBV}}}\) translation is a function
defined as follows, by induction on the derivation of a term with the (unambiguous) grammar above: 
is the left-inverse of
.
and \(s\in \mathcal {T}_{\bullet }\) such that \(\underline{t}\rightarrow _{\bullet }s\). Then
and
, where
.
implies
implies
where
.
if and only if
-normal form iff
is in \(\rightarrow _{\bullet }\)-normal form.
to obtain completeness.
is defined on types and terms by: 
, and judgments:
.
.
then
.
. The interesting cases are when there is a \(\textsf{db}\), \(\textsf{lsv}\), or \(\textsf{gc}\) step at the root.
. Then: 
, where
because
. \(\blacksquare \)
, containing the closure by \(\rightarrow _{\bullet }\)-reduction of the image of
, as well as a subset
, as follows: 
defined as follows, by induction on the derivation of a term with the (unambiguous) grammar above: 
is the left-inverse of
.
and \(s\in \mathcal {T}_{\bullet }\) such that \(\underline{t}\rightarrow _{\bullet }s\). Then
and
.
if and only if
. Moreover, \(t\) is in
-normal form iff
is in \(\rightarrow _{\bullet }\)-normal form.
is allowed if
, while typically call-by-value evaluation would proceed to contract the outermost redex.
, and
for \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBS}}}\) respectively. Recall that evaluation is called weak if it does not proceed inside the bodies of \(\lambda \)-abstractions. Second, we define an evaluation relation \(\rightsquigarrow \) for \(\lambda ^{{!}{\bullet }}\), which is also “weak” in that it does not reduce inside \(\lambda \)-abstractions, boxes (\(\bullet \)), nor promotions (\({!} \)). Finally, we show that evaluation according to
, and
can be simulated by \(\rightsquigarrow \) via the translations already introduced in Section 5.
, where \(t,t' \in \mathcal {T}_{\textsf{LSC}}\) and the set of \({{\textsf{CBN}}}\)-rulenames (\(\rho ,\rho ',\ldots \)) is given by \( \rho \,{:}{:=}\, \textsf{db}\mid \mathsf {\varsigma }(x,t) \mid \textsf{ls}\mid \textsf{gc}\). Weak \({{\textsf{CBN}}}\) evaluation is the union
, excluding auxiliary \(\mathsf {\varsigma }(x,t)\) steps. It is defined by the following inductive rules: 
, and
rules derive root reduction steps. The
and
rules correspond to congruence closure below weak head evaluation contexts. The side condition in the
rule is to avoid unwanted variable capture. The somewhat atypical
rule derives steps of the form
, which substitute a single free occurrence of \(x\) (in evaluation position) by \(s\). This rule works in synchrony with
to allow \(\textsf{ls}\) steps: for example,
and
. This is inspired the formulation of strong call-by-need of Balabonski et al. [9].
. Note also that
is non-deterministic, although confluent. The source of non-determinism is that \(\textsf{gc}\) steps can be performed in any order. For example \(((\lambda x.\,x)\,y)[z/s]\) reduces both with a \(\textsf{db}\) and with a \(\textsf{gc}\) step.
, where \(t,t' \in \mathcal {T}_{\textsf{LSC}}\) and the set of \({{\textsf{CBV}}}\)-rulenames (\(\rho ,\rho ',\ldots \)) is given by \( \rho \,{:}{:=}\, \textsf{db}\mid \mathsf {\varsigma }(x,\texttt{v}) \mid \textsf{lsv}\mid \mathsf {gcv\texttt {+ }}\). Weak \({{\textsf{CBV}}}\) evaluation is
, excluding auxiliary \(\mathsf {\varsigma }(x,\texttt{v})\) steps. It is defined by the following inductive rules: 
. Rules
, and
are root reduction rules, while
, and
correspond to congruence closure rules. The
rule plays a similar role as the analogue rule in \({{\textsf{CBN}}}\), but only allows substituting variables for strict values. In this notion of \({{\textsf{CBV}}}\) evaluation, arguments of applications are not evaluated. The restriction that the argument is a value is not imposed to contract a \(\beta \)-like redex, but rather to perform the substitution. These ideas can already be found in the \(\lambda _{CBV}\)-calculus of [18]. Note that in \({{\textsf{CBV}}}\) evaluation (
) there is a second source of non-determinism, namely that
and
overlap, so the body and the argument of an ES can be evaluated concurrently.
, where \(t,t' \in \mathcal {T}_{\textsf{LSC}}\) and the set of \({{\textsf{CBS}}}\)-rulenames (\(\rho ,\rho ',\ldots \)) is given by \( \rho \,{:}{:=}\, \textsf{db}\mid \mathsf {\varsigma }(x,\texttt{v}\texttt{L}) \mid \mathsf {\iota }(x) \mid \textsf{lsw}\mid \textsf{gc}\). Weak \({{\textsf{CBS}}}\) evaluation is the union
, excluding auxiliary \(\mathsf {\varsigma }(x,\texttt{v}\texttt{L})\) and \(\mathsf {\iota }(x)\) steps. It is defined by the following inductive rules: 
. Rules
, and
are root reduction rules, while
, and
are congruence closure rules. The rule
plays a similar role as the analogue rules in \({{\textsf{CBN}}}\) and \({{\textsf{CBV}}}\), but only allows substituting variables for terms of the form \(\texttt{v}\texttt{L}\) (known as answers in the literature). The rule
is a variant of
that acts on the argument of an ES; this rule is not strictly necessary for evaluation, but it is crucial for the embedding into \(\lambda ^{{!}{\bullet }}\) to be complete. The
rule is used in synchrony with the congruence rules to derive steps that are always of the form
indicating that \(x\) occurs in \(t\) in an evaluation position. This is used to check whether \(x\) it a needed variable. For example,
and
, so the fact that \(x\) is needed on the left triggers the evaluation of the argument:
. From this, one obtains the substitution step
.
, and
are root reduction rules, while
, and
are congruence rules. Rule
plays a similar role as the analogue rules in \({{\textsf{CBN}}}\), \({{\textsf{CBV}}}\), and \({{\textsf{CBNd}}}\), but only allows substituting a variable by a term of the form \((\bullet t)\texttt{L}\). Rule
plays a similar role as the analogue rule in \({{\textsf{CBNd}}}\), used to check whether a variable is in evaluation position. Note that there are no congruence rules below \(\lambda \)-abstraction, box (\(\bullet \)), nor promotion (\({!} \)). Evaluation can proceed below promotion in two particular cases. First, the
rule allows to perform substitution immediately below a promotion; for instance \(({!}{u})[u/{!}{\bullet v}] \rightsquigarrow _{\mathsf {\bullet ls}} ({!}{\bullet v})[u/{!}{\bullet v}]\). Second, the
rule allows evaluation below a promotion when a term is the argument of a “needed” substitution; for instance \((uv)[u/{!}{((\lambda a.\,a)(\bullet w))}] \rightsquigarrow _{\mathsf {\bullet db}} (uv)[u/{!}{\bullet w}] \rightsquigarrow _{\mathsf {\bullet ls}} ((\bullet w)v)[u/{!}{\bullet w}] \).
, and
translations introduced in Section 5:
, defined as
but adding an inverse garbage collection rule that derives
.
