Dieses Kapitel vertieft sich in die komplizierte Verbindung zwischen funktionalen Sprachen und der Beweistheorie und baut auf Howards bahnbrechender Erkenntnis auf, dass das System einfacher Typen für die λ-Berechnung Gentzens natürlicher Schlussfolgerung minimaler intuitionistischer Logik entspricht. Der Text stellt die gängige Meinung in Frage, dass der natürliche Abzug keine solide logische Grundlage für die CbV-Bewertung bietet, und präsentiert eine neuartige Interpretation des Vanilla Sequent Calculus als eine natürliche Curry-Howard-Interpretation von CbV. Das Kapitel untersucht die Vorteile des Umschreibens von Regeln aus der Ferne und bietet einen eleganteren und kompakteren Ansatz zur Reduzierung von Schnittbildern. Er diskutiert auch die Implikationen dieser neuen Perspektive für Korrekturassistenten basierend auf abhängigen Typen und befürwortet eine minimalistische logische Grundlage für die CbV. Das Kapitel schließt mit einem Vergleich dieses Ansatzes mit bestehender Literatur und der Skizzierung potenzieller Wege für zukünftige Forschung, einschließlich einer Curry-Howard-Korrespondenz für Call-by-need, die nicht auf linearen / affinen Konzepten beruht.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Existing Curry-Howard interpretations of call-by-value evaluation for the \(\lambda \)-calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear logic, despite the fact that call-by-value was introduced in an intuitionistic setting without linear features.
This paper shows that the most basic sequent calculus for minimal intuitionistic logic—dubbed here vanilla—can naturally be seen as a logical interpretation of call-by-value evaluation. This is obtained by establishing mutual simulations with a well-known formalism for call-by-value evaluation.
1 Introduction
The connection between functional languages and proof theory stems from Howard’s insight that the system of simple types for the \(\lambda \)-calculus is exactly Gentzen’s natural deduction for minimal intuitionistic logic [41]. Additionally, \(\beta \)-reduction exactly matches the logical process of detour elimination, also called normalization. This correspondence concerns the unrestricted, or call-by-name, notion of \(\beta \)-reduction.
In practice, the evaluation mechanism at work in functional languages never follows that of call-by-name of the ordinary \(\lambda \)-calculus. Plotkin’s call-by-value \(\lambda \)-calculus [52] restricts \(\beta \)-reduction to fire when the argument is a value, that is, a variable or an abstraction, and it is often seen as a better fit for applications.
Anzeige
Call-by-Value and Natural Deduction. Natural deduction, unfortunately, does not provide a solid logical foundation for call-by-value (shortened to CbV). On the positive side, values are proofs ending in a logical introduction rule. The restriction to values in the proof normalization process, however, has to be enforced; it does not arise naturally from the structure of natural deduction. Moreover, when one considers open terms and/or strong evaluation (that is, under abstraction), the normal forms of Plotkin’s CbV calculus have a complex inductive structure not corresponding to any natural concept in natural deduction. The study of strong evaluation is essential for proof assistants based on dependent types. Notably, Leroy and Grégoire use strong CbV for Coq [37]. Strong evaluation is also advocated by Scherer and Rémy [57] as relevant for a solid theory of functional languages. Lastly, in proof theory one speaks of cut/detour elimination, and they can be eliminated only if evaluation goes under abstractions.
The issue with normal forms is delicate. It is well-known that the rewriting rules of Plotkin’s calculus are not suited for open terms and strong evaluation, causing premature normal forms, as pointed out by Paolini and Ronchi della Rocca [50, 51, 55]. The literature contains many alternative CbV \(\lambda \)-calculi fixing this defect, as surveyed by Accattoli and Guerrieri [6], often extending the syntax of the \(\lambda \)-calculus with \(\textsf{let}\)-expressions or explicit substitutions, as for instance is the case in Moggi’s calculus [46, 47].
Logically, both \(\textsf{let}\)-expressions and explicit substitutions are decorations for the (intuitionistic) cut rule. Even when one considers these alternative CbV \(\lambda \)-calculi not suffering of premature normal forms, natural deduction with cut is not really a solid logical foundation, because CbV normal terms correspond to proofs with cuts. That is, not all cuts are eliminable.
Call-by-Value and Proof Theory. Beyond natural deduction for minimal intuitionistic logic (shortened to MIL), there are two main ways of looking at CbV via proof theory. One of them is as a certain intuitionistic fragment of linear logic, as first done by Girard [35], which can also be seen as a certain embedding into the modal logic S4, as pointed out recently by Espírito Santo et al. [30]. Another way is via the duality between CbV and call-by-name (CbN) in classical logic, usually traced back to Filinski [31]. This duality was then analyzed through linear logic lenses by Danos et al. [21], and crystallized as the computational interpretation of a sequent calculus by Curien and Herbelin [18].
Anzeige
What is not ideal, however, is that these are additional logical concepts. In Plotkin’s CbV (and in many of the alternative CbV \(\lambda \)-calculi), indeed, there is no trace of linearity nor of classical principles. It is natural to wonder whether there is a neat logical way of modeling CbV using only MIL. There are works connecting CbV and MIL, such as Dyckhoff and Lengrand’s study of Herbelin’s LJQ [25, 26, 40] or Ohori [49], but they are based on modifications of the deductive system imposing the CbV reading. This paper presents a fresh perspective on this question.
Fig. 1.
Vanilla sequent calculus for minimal intuitionistic logic (MIL).
The Vanilla Sequent Calculus. Our result is that the most basic presentation of Gentzen’s sequent calculus [34] for MIL, here dubbed vanilla sequent calculus and shown in Fig. 1 (the proper additive presentation of MIL requires some further details about contractions, see Sect. 3), is a natural Curry-Howard reading of CbV evaluation. The system comes with a natural notion of values, which are proofs ending with right deduction rules. Crucially, we exploit a splitting property that is specific to sequent proofs of MIL: every proof of \(\Gamma \vdash A\) can be uniquely split into a value sub-proof of \(\Delta \vdash A\) followed by a sequence of left rules turning \(\Delta \) into \(\Gamma \) without touching \(A\). Thanks to this feature, there is no need to modify the sequent calculus with a so-called stoup (i.e. a distinguished formula in a formula context) as in Curien and Herbelin [18], adding restrictions on the shape of proofs as in Herbelin’s presentation of LJQ [40] or Ohori [49], or having a separate judgment for values as in Lengrand and Dyckhoff’s presentation of LJQ [25, 26]. Essentially, values are recovered on-the-fly, with no need to mark them out explicitly.
Beyond the splitting property, our fresh perspective stems from the observation that the ineliminable cuts in the CbV reading of natural deduction correspond exactly to occurrences of the left rule \((\Rightarrow _l)\) for \(\Rightarrow \) in the vanilla sequent calculus. In other words, the cut rule in CbV natural deduction is overloaded. When one looks at it through the vanilla sequent calculus, it represents both the vanilla \((\texttt{cut})\) and \((\Rightarrow _l)\) rules. Disentangling the two concepts, the vanilla sequent calculus provides a neater logical foundation where CbV normal terms have no cuts, as one would expect.
Concretely, we adopt proof terms for the vanilla sequent calculus defined without the application \(ts\) construct (which is specific to natural deduction) and with distinct explicit substitutions constructs for rules \((\texttt{cut})\) and \((\Rightarrow _l)\), what we dub here vanilla\(\lambda \)-terms.
Cut Elimination at a Distance: the Vanilla\(\lambda \)-Calculus. Once it is clarified that cut-free vanilla proofs are a good formalism for CbV normal forms, one needs to pair them with a natural notion of cut elimination. Quoting Zucker [61]: "we know at the outset what a cut-free derivation is, and the problem is to define the conversions".
For that, we give a very compact definition of cut elimination following the at a distance style of rewriting rules promoted by Accattoli and Kesner for natural deduction calculi [4, 10, 42], and recently shown to be a good fit for the intuitionistic linear logic sequent calculus (without stoup) by Accattoli [1]. To avoid misunderstandings, note that, while rewriting at a distance is also an additional concept, it is fundamentally different from linear or classical logic. Linear and classical logic are logical concepts; they change the logic. Rewriting at a distance is a rewriting concept, not a logical one; the logic stays the same, what changes is only how proofs/terms are rewritten.
The key point of rewriting at a distance is that it avoids the many rewriting rules propagating explicit substitutions through the term structure, which are found in many extended \(\lambda \)-calculi, via generalizations of the rewriting rules exploiting contexts (that is, terms with a hole). This is particularly useful in the study of sequent calculi, where commuting cut elimination cases are a notorious burden. Essentially, rewriting at a distance allows one to have only principal cut elimination cases, avoiding completely the commutative ones. This is similar to what happens with proof nets, except that it is simpler, because the graphical language is avoided altogether by means of—again—contexts.
Rules at a distance rest on on-the-fly decompositions of a term into a context and a sub-term. In our setting, this decomposition becomes the splitting property mentioned above. Distance thus allows for a smooth treatment of values at the rewriting level.
Our proof terms plus cut elimination at a distance form what we dub as the vanilla\(\lambda \)-calculus.
Results. The central result of the paper is that two standard translations, from natural deduction to sequent calculus, and back, induce termination-preserving simulations between the vanilla \(\lambda \)-calculus and one of the formalisms extending Plotkin’s CbV. To make things as smooth as possible, our choice of formalism for CbV is Accattoli and Paolini’s value substitution calculus [13], a natural deduction \(\lambda \)-calculus with explicit substitutions at a distance, used in various recent studies about CbV [5, 6, 8, 9, 12].
For the sake of keeping this fresh perspective light and readable, we focus on explaining the inception of the calculus, rewriting rules at a distance, and the simulation results. As a check of good design for the vanilla \(\lambda \)-calculus, we also prove strong normalization for typed terms. This result is more challenging than the simulations, but it is expected and proved via an established technique, namely, the bi-orthogonal reducibility method. Therefore, we only give the statements and refer to the technical report [3] for the details of the proof, which is adapted from Accattoli [1].
How Our Approach Fits in the Literature. Certainly, ours is not the first computational interpretation of a sequent calculus for MIL, whether vanilla or not. Essentially, there are three kinds of interpretations in the literature. For the first two, we adopt Mint’s local / global terminology [44]:
1.
The local approach. It decorates sequent proofs using a language of terms without application and with \(\textsf{let}\)-expressions (or explicit substitutions) for both the cut rule and the left rule for \(\Rightarrow \), as we do. In particular, this approach does not use ordinary \(\lambda \)-terms to decorate proofs. These alternative terms are then endowed with (usually many) rewriting rules mimicking the propagation of cuts (that is, they are not at a distance). This approach is followed e.g. by Gallier [33], Ohori [49], Dyckhoff and Lengrand [25, 26], and Cerrito and Kesner [16]. Gallier and Cerrito and Kesner do not notice the connection with CbV, while Ohori and Dyckhoff and Lengrand do embrace it, but use non-standard sequent calculi and complex sets of rewriting rules. Gallier (1993) revisits standard proof theoretical concepts under the influence of linear logic. Cerrito and Kesner (2004) develop a Curry-Howard for pattern matching. Ohori’s (1999) aim is to show a connection between proof theory and Sabry and Felleisen’s A-normal forms [32, 56]. This paper can be seen as a re-elaboration of Ohori’s work, where the focus is a minimalistic logical foundation rather than A-normal forms. Our aim is also similar to Dyckhoff and Lengrand [26] (2007) but the outcome is considerably simpler: they have three notions of cut and 14 rewriting rules, while we have only one cut and one rewriting rule.
2.
The global approach. It amounts to decorate sequent proofs with ordinary \(\lambda \)-terms and endowing them with call-by-name rewriting. It is rooted in Prawitz’s many-to-one translation of sequent calculus to natural deduction [54], it possibly first appears with proof terms in Pottinger [53], and it is nicely presented by Barendregt and Ghilezan using the vanilla sequent calculus [15]. The idea is to decorate rules \((\texttt{cut})\) and \((\Rightarrow _l)\) using meta-level substitution, as follows:
The serious drawback of the global approach is the potential size mismatch between a sequent calculus proof \(\pi \) and the \(\lambda \)-term \(u_\pi \) decorating \(\pi \), stemming from the fact that in the sequent calculus the formula \(B\) in \((\Rightarrow _l)\) can be treated non-linearly, that is, it can be weakened or contracted, leading to duplications/erasures of \(ys\). The non-linear use of \(B\) is referred to as the root of all evil by Danos et al. [21], in their study of representations of System F in linear sequent calculi.
3.
The stoup approach. A third approach departs from the vanilla sequent calculus, adopting a form of enriched sequent or adding further judgments to the deductive system. Typically, at the logical level it uses two judgments \(\Gamma ;\vdash A\) and \(\Gamma ;B\vdash A\), where the space between the semicolon and \(\vdash \) is called stoup—terminology due to Girard [36]—and it is either empty or contains a single, distinguished formula. The non-decorated version of rule \((\Rightarrow _l)\) then becomes:
The key point is that the rules of the system (which can be defined in various ways) treat the stoup linearly, that is, the stoup formula is never weakened nor contracted. This fact is what circumvents the size mismatch of the global approach, and thus allows for a good match between sequent proofs with stoup and ordinary \(\lambda \)-terms. It is usually associated with CbN evaluation.
The stoup approach is first studied by Danos et al. [21], building on Girard [36]. It then became the basis for Herbelin [39], who studies the intuitionistic CbN case, and then Curien and Herbelin [18], who study the classical case in both CbN and CbV, with three judgments and stoup on both sides of the sequent. From [18], it is easy to extract a CbV intuitionistic fragment (as done for instance by Accattoli and Guerrieri [6]), but one obtains a sequent calculus with stoup, not the vanilla one. A different presentation of essentially the same system is the mentioned approach to LJQ by Dyckhoff and Lengrand [25, 26], who use two distinct judgments—with one dedicated to values and connected to focalization—rather than the stoup.
Nowadays, a number of works have built over Curien and Herbelin’s work, for instance [14, 17, 22‐24, 28, 29, 45, 48, 60], to the point that it became the standard computational interpretation of sequent calculi.
Our work is orthogonal, and somewhat more basic, as it looks at the intuitionistic case without any form of stoup, focalization, or separate judgment.
Non-Canonicity vs Sharing. In the proof theoretical literature, the vanilla sequent calculus is often criticized as non-canonical because (CbN) normal \(\lambda \)-terms correspond to more than one cut-free proof, when one embraces the global approach—this is another face of Danos et al.’s root of all evil mentioned above.
A key point of our fresh perspective is that this is a feature rather than a drawback: it is simply the fact that CbV normal terms such as \(\textsf{let}\ x=yz\ \textsf{in}\ (wxxx)\) can be seen as shared representations of CbN normal forms such as \(w(yz)(yz)(yz)\), and that a term can be shared in various ways—another one is \(\textsf{let}\ x=yz\ \textsf{in}\ (wxx(yz))\). Therefore, the vanilla sequent calculus gives a first-class status to sub-term sharing for normal forms.
More precisely, \(\textsf{let}\)-expressions annotate cuts and give a first-class status to sub-term sharing independently of the proof system. The concept of value induces a dynamic / static refinement of sub-term sharing. Dynamically, only values are unshared (that is, duplicated or erased). Non-values are never unshared, thus end up being statically shared in normal forms, as in \(\textsf{let}\ x=yz\ \textsf{in}\ (wxxx)\), making sub-term sharing visible denotationally. These two roles are entangled in natural deduction for MIL while they are handled separately in sequent calculus via its two left rules, namely cut captures dynamic sharing and subtraction captures static sharing. Therefore, the left rules of the sequent calculus for MIL encapsulate the sharing features of values.
For an extensive informal discussion about the deep relationship between sharing and CbV see Accattoli’s dissemination paper [2].
Proofs Omitted proofs are in the associated technical report on arXiv [3].
2 Natural Deduction, Call-by-Name, and Rewriting at a Distance
In this section, we give our presentation of Howard’s standard correspondence between natural deduction for minimal intuitionistic logic and the simply typed (call-by-name) \(\lambda \)-calculus [41], here also referred to as the natural\(\lambda \)-calculus, to distinguish it from the one that shall be associated to the sequent calculus. The correspondence is in Fig. 2. Curiously, in [41] Howard mentions that his work stems from Tait’s "discovery of the close correspondence between cut elimination and reduction of \(\lambda \)-terms" [59].
Fig. 2.
\(\lambda \)-calculus and natural deduction \(\vdash _{\texttt{N}}\).
Routine Definitions: Terms and Contexts. We assume given a countable set of variables \(\mathcal {V}_{\texttt{N}}\), where \(\texttt{N}\) stresses that they are for the natural \(\lambda \)-calculus. The meta-level capture-avoiding substitution of \(s\) for \(x\) in \(t\) is denoted with
.
Contexts are terms with exactly one occurrence of the hole\(\langle \cdot \rangle \), an additional constant, standing for a removed sub-term. We shall use various notions of contexts. For the \(\lambda \)-calculus, the most general ones are (general) contexts\(C\), which simply allow the hole to be anywhere. The main operation about contexts is plugging\(C\langle t\rangle \) where the hole \(\langle \cdot \rangle \) in context \(C\) is replaced by \(t\). Plugging, as usual with contexts, can capture variables—for instance \((\lambda x.\langle \cdot \rangle t)\langle x\rangle = \lambda x.xt\).
Routine Definitions: Types and Derivations. Types are built out of an unspecified atomic type \(X\) and the implication \(\cdot \Rightarrow \cdot \) connective. Type contexts \(\Gamma \) are implicitly considered modulo exchange, that is, \(\Gamma \) is a partial function from variables to formulas such that \(\texttt{dom}(\Gamma ) :=\{x\mid \Gamma (x) \text{ is } \text{ defined }\}\) is finite, usually written as \(x_1 \,{:}\,A_1, \dots , x_n \,{:}\,A_n\) (with \(n \in \mathbb {N}\)) if \(\texttt{dom}(\Gamma ) = \{x_1, \dots , x_n\}\) and \(\Gamma (x_i) = A_{i}\) for \(1 \le i \le n\). As it is standard, writing \(\Gamma , x\,{:}\,A\) implicitly assumes that \(x\notin \texttt{dom}(\Gamma )\).
We write \(\pi \,\triangleright \Gamma \vdash _{\texttt{N}}t\,{:}\,A\) if \(\pi \) is a (type) derivation, that is, a tree constructed using the rules for \(\vdash _{\texttt{N}}\), having axioms as leaves, and of final judgment \(\Gamma \vdash _{\texttt{N}}t\,{:}\,A\).
Left and Right Rules. The typing rule \((\Rightarrow _r)\) for abstraction carries a right r subscript, to later distinguish it from the left rule for implication of the sequent calculus. We shall constantly refer to left and right rules, and yet we shall dodge abstract definitions of these notions. Rules \(\texttt{ax}\), \(\Rightarrow _r\), and @ are right rules.
Detours. The logical analogues of \(\beta \)-redexes are detours, which are simply given by a \(\Rightarrow _r\) rule followed by a @ rule, that is exactly what is required to type a \(\beta \)-redex—see Fig. 2. \(\lambda \)-terms in normal form are exactly those typed by proofs of \(\vdash _{\texttt{N}}\) without detours.
Fig. 3.
Substitution Calculus (SC).
Explicit Substitutions. In Fig. 3, the \(\lambda \)-calculus is extended with an explicit substitution (shortened to ES) constructor
, which binds \(x\) in \(t\). It can be thought as a more compact notation for \(\textsf{let}\ x=s\ \textsf{in}\ t\), with the slight difference that the evaluation order is not fixed in
. At the logical level, ESs are decorations for cuts, as shown in Fig. 3. Note that in the literature about \(\lambda \)-calculi at a distance, ESs are usually rather written using the mirrored construct
. We here prefer to use
because it more faithfully reflects the structure of type derivations.
A point of view underlying our study is that ESs are a form of sub-term sharing, meaning that
is a version of \(tt\) where \(t\) is shared.
In this paper, cut shall be considered as a left rule (for its right premise), according to the view outlined at the end of the introduction that left rules account for sharing.
Rewriting Rules. We endow natural \(\lambda \)-terms with ESs with small-step rewriting rules, that is, rules based on meta-level substitution, obtaining Accattoli and Kesner’s substitution calculus (SC) [11], of rewriting relation \(\rightarrow _{\texttt{SC}}\). It is composed of two rewriting rules, namely the standard substitution rule \(\rightarrow _{\texttt{s}}\), and the perhaps less standard \(\beta \)at a distance rule \(\rightarrow _{\texttt{dB}}\). Rule \(\rightarrow _{\texttt{dB}}\) generalizes \(\beta \)-redexes as to fire even when there are some ESs (i.e. left rules) in between the abstraction and the argument, fact that is formalized in the definition of the rule via the (possibly empty) substitution context \(L\) (mnemonic: \(L\) stands for List of substitutions). For instance,
(1)
This kind of rule circumvents the need of having commuting rewriting rules such as
or
in order to expose the \(\beta \)-redex in (1). The rewriting theory of ESs at a distance has simpler proofs and stronger properties (e.g. residuals) than for commuting-based ESs, see Accattoli and Kesner [4, 10, 11].
Note that ESs can always be reduced, thus there are no ESs in \(\rightarrow _{\texttt{SC}}\)-normal forms. In other words, normal forms are sharing-free.
Clearly, the substitution calculus simulates \(\beta \), since
.
3 The Natural \(\lambda \)-Calculus By Value
In this section, we discuss the presentation of CbV in a natural deduction calculus, first in Plotkin’s style and then with cuts / ESs. In particular, we shall see the advantages and the limits of ESs for CbV.
Fig. 4.
Plotkin’s (natural) CbV \(\lambda \)-calculus.
Plotkin’s Call-by-Value and Open Terms. The definition of CbV à la Plotkin following the modern presentation by Dal Lago and Martini [20] is in Fig. 4. Values \(v\) are defined as variables and abstraction, and the \(\beta _v\)-rule is obtained by restricting \(\beta \)-redexes to fire only when the argument is a value. Strong evaluation allows one to reduce \(\beta _v\)-redexes everywhere in a term, and weak evaluation instead forbids \(\beta _v\)-redexes under abstraction.
It is well-known that Plotkin’s approach works smoothly only in the important and yet limited case of weak evaluation of closed terms. Open terms are an issue, and even more so is strong evaluation, because they cause stuck\(\beta \)-redexes such as \((\lambda x.t) (yz)\) where the argument is \(\rightarrow _{\beta _v}\)-normal and not a value, thus the \(\beta _v\)-rule cannot fire. These stuck configurations are problematic, as first noticed by Paolini and Ronchi della Rocca [50, 51, 55]. The easiest way of stating the problem is that the paradigmatic looping term \(\Omega :=\delta \delta \), where \(\delta :=\lambda x.xx\), and its variant \(\Omega _{\texttt{stuck}} :=(\lambda x.\delta )(yz)\delta \) are contextual equivalent and yet \(\Omega \) loops while \(\Omega _{\texttt{stuck}}\) is normal in Plotkin’s approach. Terms such as \(\Omega _{\texttt{stuck}}\) are sometimes called premature normal forms, and break expected properties of Plotkin’s calculus with respect to denotational models, see Accattoli and Guerrieri [7].
Logically, the issue is that not all detours can be eliminated using Plotkin’s \(\beta _v\)-rule.
Fig. 5.
Value Substitution Calculus (VSC).
Substitutions by Value. The issue with open terms has been studied at length by Accattoli and Guerrieri and co-authors [6‐8, 12, 38], who in [6] study and compare various ways of circumventing it. One of the most flexible and studied solutions amounts to add ESs at a distance. The framework is Accattoli and Paolini’s value substitution calculus (VSC) [13], defined in Fig. 5, which is the variant of the substitution calculus (of the previous section) modelled over the CbV translation of \(\lambda \)-calculus in linear logic proof nets. The VSC has the same \(\beta \) at a distance rule \(\rightarrow _{\texttt{dB}}\) of the SC, which does not require the argument to be a value. It has instead a different substitution rule, which is where the value restriction takes place. Its value substitution rule \(\rightarrow _{\texttt{vs}}\) uses distance (i.e. the substitution context \(L\) around the value \(v\)). For instance,
. Distance allows one to avoid commuting rules such as
which are often found in CbV calculi with \(\textsf{let}\)-expressions, for instance in Moggi’s calculus [46, 47], where that rule is called assoc.
Advantages of ESs by Value. The VSC handles open terms correctly thanks to distance and having moved the value restrictions from \(\beta \)-redexes to substitution redexes. As evidence of correct behavior, let’s have a look at the variant \(\Omega _{\texttt{stuck}}\) of \(\Omega \) that is a premature normal form in Plotkin’s calculus. It now (correctly) diverges in the VSC:
The VSC has a number of operational and denotational good properties, as shown by Accattoli and co-authors in various recent works [5, 8, 12], essentially providing a CbV calculus that mimics in CbV most of the good properties of the CbN \(\lambda \)-calculus, considerably improving over Plotkin’s presentation. At the same time, the VSC and Plotkin’s calculus induce the same contextual equivalence on closed terms (see [8]), thus the VSC is a conservative refinement of Plotkin’s calculus.
Limits of ESs by Value in Natural Deduction. The VSC, however, is not free from glitches. In contrast to the CbN case, in the VSC not all ESs are eliminable, because of the value constraint. Namely, an ES such as
cannot be eliminated, since \(yz\) is normal and not a value. It might seem that this is the same issue that we pointed out for Plotkin’s approach, for which some detours are not eliminable. The situation however is different: in Plotkin’s case, ineliminable detours break operational and denotational properties, while ineliminable ESs do not cause similar problems in the VSC.
It is important to stress that—in itself—the presence of ineliminable ESs is not a drawback. They actually are a feature of CbV and of the VSC. The fact that some ESs are ineliminable, indeed, means that sub-term sharing ends up in normal forms, and thus becomes denotationally visible, which is a good thing, since it opens the way to a mathematical understanding of sharing and efficiency. In Ehrhard’s CbV relational denotational model [27], for instance,
and \(w(yz)(yz)\) have different interpretations; they instead have the same interpretation in the CbN relational model. An extensive high-level discussion of the relationship between sharing and CbV can be found in Accattoli’s dissemination paper [2].
The glitch of the VSC is the fact that its ESs are still typed with cuts, as in the SC. Therefore, if some ESs are ineliminable then some cuts are ineliminable, in the CbV interpretation of natural deduction with cuts. This clearly goes against the expected property of the cut rule, which is admissibility, that is, that all cuts are eliminable. What happens in the VSC is that only cuts containing values are eliminable.
Ideally, one would like to have two separate constructors, one for eliminable cuts and one for ineliminable cuts. This does not seem to be naturally achievable in natural deduction, where the two are entangled. The aim of this paper is to show that, instead, it is exactly what naturally happens in the sequent calculus.
4 Proof Terms for the Vanilla Sequent Calculus
Here, we present the sequent calculus for minimal intuitionistic logic (MIL). We adopt an additive presentation of the MIL fragment of Gentzen’s original one [34] (which was multiplicative), mimicking the nowadays standard use of additive natural deduction for Howard’s correspondence with the \(\lambda \)-calculus (see e.g. Sørensen and Urzyczyn [58]), despite the fact that Howard’s original presentation was multiplicative [41]. The rules are in Fig. 6, which we refer to as vanilla, to stress that we do not considered distinguished formulas (also called stoup) on the left of sequent symbol \(\vdash _{\texttt{S}}\), nor any other tweak.
Fig. 6.
Vanilla \(\lambda \)-terms and how they decorate the vanilla sequent calculus \(\vdash _{\texttt{S}}\) for MIL.
The main difference with natural deduction is that the application rule (@) is replaced by the left rule \((\Rightarrow _l)\) for \(\Rightarrow \) (see Fig. 6, the notation \(\Gamma \cup \texttt{y}\,{:}\,A\Rightarrow B\) is explained below), beyond having the cut rule from the start (while in natural deduction we added it only at a later moment). For the sequent calculus, we shall re-use most basic concepts introduced for natural deduction without re-defining them.
Vanilla\(\lambda \)-Terms and the Left Rule for\(\Rightarrow \). We adopt what Mint calls the local approach [44], followed also, for instance, by Gallier [33, Section 10], Dyckhoff and Lengrand [25, 26], Ohori [49], and Cerrito and Kesner [16], introducing a language \(\Lambda _{\texttt{S}}\) of vanilla\(\lambda \)-terms faithfully coding the structure of sequent proofs. We write the terms of \(\Lambda _{\texttt{S}}\) using a different font \(\texttt{t},\texttt{s},\texttt{u}\) (with respect to the one used for natural \(\lambda \)-terms), also for the variables \(\texttt{x},\texttt{y},\texttt{z},\texttt{w}\), whose set is noted \(\mathcal {V}_{\texttt{S}}\). The main point of \(\Lambda _{\texttt{S}}\) is that there are no applications (which decorate (@) rules). They are replaced by a new constructor
, dubbed here subtraction (following Accattoli [1]), and which binds \(\texttt{x}\) in \(\texttt{t}\) and adds a free occurrence of \(\texttt{y}\). Intuitively, subtraction can be thought of as \(\textsf{let}\ \texttt{x}=\texttt{y}\texttt{s}\ \textsf{in}\ \texttt{t}\) (which is the notation used by Gallier [33]) but we prefer to avoid such a notation, for various reasons. Firstly, writing \(\texttt{y}\texttt{s}\) we would still be resting on application, while we want to stress that application is not part of the new language, since there is no (@) rule at the logical level. Secondly, in \(\textsf{let}\ \texttt{x}=\texttt{y}\texttt{s}\ \textsf{in}\ \texttt{t}\) the two active premises \(\texttt{x}\) and \(\texttt{s}\) of the \((\Rightarrow _l)\) logical rule are given asymmetric roles, while in
their roles are symmetric. Thirdly, \(\textsf{let}\)-expressions are verbose, thus we adopt a bracket notation.
Note that the typing rule for subtractions uses a new notation \(\Gamma \cup \texttt{x}\,{:}\,A\), defined as:
and it is undefined if \(\texttt{x}\in \Gamma \) and \(\Gamma (\texttt{x}) \ne A\). The notation is needed because the additive presentation might have to do on-the-fly contractions on the newly introduced formula \(A\Rightarrow B\), as for instance in the following case, where the free variable occurrence introduced by rule \((\Rightarrow _l)\) is immediately identified with the already existing variable \(\texttt{y}\):
This phenomenon is not present in natural deduction because therein formulas and variables are introduced on the left of \(\vdash _{\texttt{N}}\) only by axioms.
Given that weakenings are freely available (in axioms), rule \((\Rightarrow _l)\) can alternatively be formulated without using \(\cup \), as follows:
This approach is adopted for instance by Herbelin [40] and Dyckhoff and Lengrand [26]. We preferred to avoid rule \((\Rightarrow _l')\), however, as we find it counter-intuitive. Yet another equivalent approach is adopting a mixed multiplicative-additive presentation: having the simpler rule \((\Rightarrow _l)\) of Fig. 1 that does not use \(\cup \) and adding a stand-alone contraction rule (which is multiplicative) for the left-hand side of \(\vdash _{\texttt{S}}\).
Different Decoration for Cuts. Another difference between \(\Lambda _{\texttt{N}}\) and \(\Lambda _{\texttt{S}}\) is that, since in \(\Lambda _{\texttt{S}}\) cuts shall play a slightly different role than in the VSC / natural deduction by value, for the sake of clarity we decorate them differently, with
rather than with
.
Fig. 7.
Translations between the natural \(\lambda \)-terms (with ESs) and the vanilla \(\lambda \)-terms.
Translations. Translations from the natural \(\lambda \)-calculus to the vanilla one and vice-versa are given in Fig. 7. They induce translations of the related logical systems, whose key ingredients are highlighted in Fig. 7, namely the simulation of the (@) rule by \(\vdash _{\texttt{S}}\) and the simulation of the \((\Rightarrow _l)\) rule by \(\vdash _{\texttt{N}}\). Both translations are obtained by introducing axioms and cuts, and are standard. For instance, Girard’s CbN and CbV translations of natural deduction to linear logic [35] are modal decorations of \(\overline{\cdot }^{\texttt{S}}\), and the cuts used in the translation of applications are called correction cuts by Danos et al. [21]. Note that the translations preserve (and reflect) values.
Translation of Cut-Free Vanilla Terms. We have not yet introduced rewriting rules for vanilla \(\lambda \)-terms (that is, cut elimination), but there are no doubts about the expected notion of normal vanilla terms: they must be the cut-free ones. The next proposition states the starting observation of this work, that is, the fact that cut-free vanilla terms are mapped to natural terms that are CbV normal, but not necessarily CbN normal.
Proposition 4.1
Let \(\texttt{t}\in \Lambda _{\texttt{S}}\) be cut-free. Then
is \(\rightarrow _{\texttt{VSC}}\)-normal but not necessarily \(\rightarrow _{\texttt{SC}}\)-normal.
Proof
By induction on \(\texttt{t}\). For \(\rightarrow _{\texttt{VSC}}\), simply note that, for cut-free vanilla terms, ESs and applications (which form \(\rightarrow _{\texttt{VSC}}\) redexes) are only introduced by the translation of subtractions, and they receive as left sub-terms the application of a free variable to a term: thus the introduced application is not a \(\rightarrow _{\texttt{dB}}\)-redex, nor it is a value (nor can reduce to one) thus the introduced ES is not a \(\rightarrow _{\texttt{vs}}\)-redex. For \(\rightarrow _{\texttt{SC}}\), the translation of subtraction instead introduces \(\rightarrow _{\texttt{s}}\) redexes. \(\square \)
In the other direction, \(\rightarrow _{\texttt{VSC}}\)-normal natural terms are not mapped by \(\overline{\cdot }^{\texttt{S}}\) to cut-free vanilla terms, because the translation of applications adds cuts. It is possible to optimize the translation as to avoid this mismatch, but the optimized translations would considerably complicate the translation of contexts (introduced and used in the next sections), which is why we refrain from it. At the same time, we shall show that the translation of normal natural terms are almost cut-free, in a suitable harmless way.
5 Defining Cut Elimination for the Vanilla \(\lambda \)-Calculus
In this section, we define cut elimination on vanilla \(\lambda \)-terms, obtaining the vanilla\(\lambda \)-calculus. Our cut elimination shall be based on meta-level substitution. The notion of value shall emerge naturally, and rules at a distance shall play a role.
Left Variable Occurrences. At first sight, defining small-step cut elimination for vanilla terms is conceptually easy, since one would simply define it as follows:
for a notion of meta-level substitution
for vanilla \(\lambda \)-terms. The problem however is that the definition of
cannot be the same as for natural terms.
In natural deduction, the free occurrences of a variable are introduced by axioms, and axioms can always be replaced by proofs having the same ending sequent. Since we consider axiom as a right rule, let us say that variables have only right occurrences, and that on right occurrences one can always define meta-level substitution
simply as the replacement of \(x\) by \(u\) in \(t\).
On vanilla terms, subtractions
introduce left occurrences of \(y\). In contrast to right occurrences, the left ones cannot be simply replaced by a vanilla term \(\texttt{u}\), because
does not belong to the grammar of vanilla terms. Therefore, the definition of meta-level substitution
on vanilla terms is a bit tricky on subtractions.
Easy Cases and Values. To define
, we have to inspect the shape of \(\texttt{u}\). The simplest case is when \(\texttt{u}\) is a variable \(\texttt{y}\), since in that case it is possible to simply replace \(\texttt{x}\) by \(\texttt{y}\). A second clear case is when \(\texttt{u}\) is an abstraction \(\lambda \texttt{y}.\texttt{s}\). Then, we can set:
This complex definition amounts to do the expected elimination of the principal cut between the abstraction and the subtraction (roughly, corresponding to the \(\rightarrow _{\texttt{dB}}\) step
of the (V)SC) plus putting the resulting term in a second created cut on \(\texttt{z}\)and propagating the substitution
to the sub-terms \(\texttt{r}\) and \(\texttt{t}\) of the subtraction. Note that the two clear cases \(\texttt{u}=\texttt{y}\) and \(\texttt{u}= \lambda \texttt{y}.\texttt{s}\) are exactly those for values, which correspond to the right rules of \(\vdash _{\texttt{S}}\). The full definition of meta-level substitution
for values is in Fig. 8. The following property is proved by induction on \(\texttt{t}\).
Lemma 5.1
Let \(\texttt{x}\notin \texttt{fv}(\texttt{t})\). Then
.
Fig. 8.
The vanilla \(\lambda \)-calculus.
The Vanilla\(\lambda \)-Calculus. For defining small-step cut elimination for all terms, we rely on the crucial observation that every vanilla term \(\texttt{t}\)splits uniquely as \(\texttt{t}= \texttt{L}\langle \texttt{v}\rangle \), where \(\texttt{L}\) is a left context—defined in Fig. 8—and \(\texttt{v}\) is a value. Note that a similar splitting is also used in the value substitution rule \(\rightarrow _{\texttt{vs}}\) of the VSC, but there is a key difference: in the VSC applications cannot be split as \(L\langle v\rangle \) (because application is not a left rule), which is why some ESs cannot be eliminated, while all vanilla terms can be split (because application is replaced by subtraction, which is a left rule).
We know how to substitute \(\texttt{v}\), and we are left to define what to do with \(\texttt{L}\). There are two options, namely mimicking the substitution rules by name (namely \(\rightarrow _{\texttt{s}}\)) and by value (\(\rightarrow _{\texttt{vs}}\)) for natural terms: either we carry \(\texttt{L}\) along with \(\texttt{v}\) in the propagation of the substitution, possibly duplicating or erasing it, as in the CbN rule \(\rightarrow _{\texttt{s}}\) of the SC, or we commute it out, as in the CbV rule \(\rightarrow _{\texttt{vs}}\) of the VSC. While in principle both are valid choices, the latter seems more natural because—even if we adopt the CbN approach—cut-free vanilla terms map to CbV normal natural terms, as shown by Proposition 4.1, and not to the CbN ones. Essentially, to catch a CbN semantics we should also modify something about cut-free proofs, but that goes against the starting point of our work, namely that vanilla cut-free proofs are a good representation of CbV normal forms.
The cut elimination rule \(\leadsto _{\texttt{cut}}\) is then defined in Fig. 8 by commuting out the left context \(\texttt{L}\), completing the definition of the vanilla \(\lambda \)-calculus. Equivalently, one can also set
and
.
Subject Reduction. The standard check for the definition of \(\leadsto _{\texttt{cut}}\) is subject reduction.
Proposition 5.1
(Subject reduction). Let \(\texttt{t}\in \Lambda _{\texttt{S}}\) and \(\pi \,\triangleright \Gamma \vdash _{\texttt{S}}\texttt{t}\,{:}\,A\) be a derivation. If \(\texttt{t}\leadsto _{\texttt{cut}}\texttt{s}\) then there exists a derivation \(\rho \,\triangleright \Gamma \vdash _{\texttt{S}}\texttt{s}\,{:}\,A\).
Proof
Let
. The proof is by induction on \(\texttt{u}\), \(\texttt{L}\), and \(\texttt{C}\). Details are in the Appendix of the technical report [3]. \(\square \)
6 Simulating the Vanilla \(\lambda \)-calculus in the VSC
To simulate the vanilla \(\lambda \)-calculus in the VSC, we need to look at how the \(\overline{\cdot }^{\texttt{S}}\) translation relates the respective notions of meta-level substitution. On vanilla terms, substitution on left variable occurrences does also the work that is done by rule \(\rightarrow _{\texttt{dB}}\) on the VSC. Unsurprisingly, then, the translation commutes with substitution only up to \(\rightarrow _{\texttt{dB}}\).
Lemma 6.1
(Substitution andcommute up to\(\rightarrow _{\texttt{dB}}\)).
.
To establish the simulation, we need a lemma about the commutation of contexts and of the translation. Technicality: the translations are extended to contexts by setting
and \(\overline{\langle \cdot \rangle }^{\texttt{S}}:=\langle \cdot \rangle \), and defining them as for terms on the other cases.
Lemma 6.2
(Contexts andtranslation).
1.
is a \(L\) context and
.
2.
is a \(C\) context and
.
Proposition 6.1
(VSC simulates vanilla). If \(\texttt{t}\leadsto _{\texttt{cut}}\texttt{s}\) then
.
Proof
For a root step
, we have:
For steps in contexts, the simulation follows from the root case and Lemma 6.2.2. \(\square \)
Putting together the simulation of cut elimination with the translation of cut-free terms, we obtain the following property.
Lemma 6.3
(Preservation of VSC termination). Let \(\texttt{t}\leadsto _{\texttt{cut}}^* \texttt{s}\) with \(\texttt{s}\) cut-free. Then
with
is \(\rightarrow _{\texttt{VSC}}\)-normal.
Proof
By Proposition 6.1, we obtain
. By Proposition 4.1,
is a \(\rightarrow _{\texttt{VSC}}\)-normal form. \(\square \)
7 Simulating the VSC in the Vanilla \(\lambda \)-Calculus
In the other direction, the translation and meta-level substitution commute neatly.
Lemma 7.1
(Substitution andcommute).
.
As before, for the simulation we need a lemma about contexts.
\(\overline{L}^{\texttt{S}}\) is an \(\texttt{L}\) context and \(\overline{L\langle t\rangle }^{\texttt{S}} = \overline{L}^{\texttt{S}}\langle \overline{t}^{\texttt{S}}\rangle \).
2.
\(\overline{C}^{\texttt{S}}\) is a \(\texttt{C}\) context and \(\overline{C\langle t\rangle }^{\texttt{S}} = \overline{C}^{\texttt{S}}\langle \overline{t}^{\texttt{S}}\rangle \).
Proposition 7.1
(Vanilla simulates VSC).
1.
If \(t\rightarrow _{\texttt{dB}}s\) then \(\overline{t}^{\texttt{S}}\leadsto _{\texttt{cut}}\leadsto _{\texttt{cut}}\overline{s}^{\texttt{S}}\).
2.
If \(t\rightarrow _{\texttt{vs}}s\) then \(\overline{t}^{\texttt{S}}\leadsto _{\texttt{cut}}\overline{s}^{\texttt{S}}\).
Proof
For root steps:
1.
\(\beta \)at a distance, i.e.
. With \(\texttt{y}\) and \(\texttt{z}\) fresh:
Where step \((\star )\) is given by the general fact that
, since \(\texttt{t}= \texttt{L}\langle \texttt{v}\rangle \) for some \(\texttt{L}\) and \(\texttt{v}\), thus
.
2.
Value substitution, i.e.
. Then:
For steps in contexts, the simulation follows from the root case and Lemma 7.2.2. \(\square \)
Translation of Normal Natural Terms. As anticipated in Sect. 5, the translation of normal VSC terms does not give cut-free vanilla terms, because the translation of applications introduces cuts. Here we show that nonetheless the obtained terms are almost cut-free, since they are cut-free up to some trivial cut elimination steps, dubbed renaming steps. In particular, they strictly reduce the size of a vanilla term.
Definition 1
(Renaming Cut Elimination Steps). A step
is a renaming step, noted \(\texttt{t}\leadsto _{\texttt{ren}\text{- }\texttt{cut}}\texttt{s}\), if \(\texttt{v}\) is a variable.
Proposition 7.2
(The\(\overline{\cdot }^{\texttt{S}}\)translation of VSC normal forms is almost cut-free). Let \(t\in \Lambda _{\texttt{N}}^{\texttt{ES}}\) be \(\rightarrow _{\texttt{VSC}}\)-normal. Then there exists \(\texttt{t}\) cut-free such that \(\overline{t}^{\texttt{S}}\leadsto _{\texttt{ren}\text{- }\texttt{cut}}^k \texttt{t}\) with \(k\le |t|\), where \(|t|\) is the size (i.e. number of constructors) in \(t\).
As for the other direction, we can put together the simulation and the translation of normal forms, obtaining the preservation of termination by \(\overline{\cdot }^{\texttt{S}}\).
Lemma 7.3
(Preservation of termination). Let \(\texttt{t}\rightarrow _{\texttt{VSC}}^* s\) with \(s\)\(\rightarrow _{\texttt{VSC}}\)-normal. Then there exists a cut-free term \(\texttt{s}\) such that \(\overline{t}^{\texttt{S}}\leadsto _{\texttt{cut}}^* \texttt{s}\).
Proof
By Proposition 7.1, we obtain \(\overline{t}^{\texttt{S}}\leadsto _{\texttt{cut}}^* \overline{s}^{\texttt{S}}\). By Proposition 7.2, there exists \(\texttt{s}\) cut-free such that \(\overline{s}^{\texttt{S}}\leadsto _{\texttt{cut}}^* \texttt{s}\). \(\square \)
8 Strong Normalization
The typical theorem for Curry-Howard correspondences is that the logical system ensures strong normalization of the typed terms. We provide such a result for our new correspondence between the vanilla \(\lambda \)-calculus and the vanilla sequent calculus.
In this section, we give only the statement, since the proof is too technical for a fresh perspective paper. The proof is developed in sections D and E of the Appendix of the technical report [3], and is based on the bi-orthogonal reducibility method, adapting and slightly simplifying its presentation in Accattoli [1].
Definition 2
(Strong normalization). A vanilla term \(\texttt{t}\) is strongly normalizing, also noted \(\texttt{t}\in \textrm{SN}_{\texttt{cut}}\), if \(\texttt{t}\leadsto _{\texttt{cut}}\texttt{s}\) implies \(\texttt{s}\in \textrm{SN}_{\texttt{cut}}\).
Theorem 1
(Typable terms are SN). Let \(\texttt{t}\in \Lambda _{\texttt{S}}\) and \(\Gamma \vdash _{\texttt{S}}\texttt{t}\,{:}\,A\). Then \(\texttt{t}\in \textrm{SN}_{\texttt{cut}}\).
9 Conclusions
We introduced the vanilla\(\lambda \)-calculus, a computational interpretation of the simplest sequent calculus, and showed that it simulates and it is simulated by call-by-value evaluation. Technically, the simulations are clean and compact, thanks to the use of rewriting rules at a distance for both the new cut elimination rule for the vanilla \(\lambda \)-calculus and the presentation of call-by-value evaluation that we adopt from the literature.
Our study nicely complements the two famous cornerstones by Curry and Howard about minimal intuitionistic logic resting only on basic logical concepts:
1.
Curry 1958 [19]: Hilbert’s system matches combinatory logic;
2.
Howard 1969 (but published only in 1980) [41]: Gentzen’s natural deduction mirrors the (call-by-name) \(\lambda \)-calculus;
We believe that our work provides a fresh perspective over the sequent calculus. Its modern computational interpretation is usually defined starting from sequent calculi with stoups for classical logic, following Curien and Herbelin [18]. The basic, vanilla presentation of the intuitionistic case seems to have fallen into a blind spot of the literature. This work shows that it is far from being unworthy of attention.
Future Work. Maraist et al. [43] propose a Curry-Howard correspondence for call-by-need using an affine logic with a duplication modality, tweaking the linear logic one for call-by-value. In ongoing work, we are using the results of this paper as the starting point for a Curry-Howard for call-by-need that is not based on linear/affine concepts.
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.
.
, which binds \(x\) in \(t\). It can be thought as a more compact notation for \(\textsf{let}\ x=s\ \textsf{in}\ t\), with the slight difference that the evaluation order is not fixed in
. At the logical level, ESs are decorations for cuts, as shown in Fig. 3. Note that in the literature about \(\lambda \)-calculi at a distance, ESs are usually rather written using the mirrored construct
. We here prefer to use
because it more faithfully reflects the structure of type derivations.
is a version of \(tt\) where \(t\) is shared.
This kind of rule circumvents the need of having commuting rewriting rules such as
or
in order to expose the \(\beta \)-redex in (1). The rewriting theory of ESs at a distance has simpler proofs and stronger properties (e.g. residuals) than for commuting-based ESs, see Accattoli and Kesner [4, 10, 11].
.
. Distance allows one to avoid commuting rules such as
which are often found in CbV calculi with \(\textsf{let}\)-expressions, for instance in Moggi’s calculus [46, 47], where that rule is called assoc.
cannot be eliminated, since \(yz\) is normal and not a value. It might seem that this is the same issue that we pointed out for Plotkin’s approach, for which some detours are not eliminable. The situation however is different: in Plotkin’s case, ineliminable detours break operational and denotational properties, while ineliminable ESs do not cause similar problems in the VSC.
and \(w(yz)(yz)\) have different interpretations; they instead have the same interpretation in the CbN relational model. An extensive high-level discussion of the relationship between sharing and CbV can be found in Accattoli’s dissemination paper [2].
, dubbed here subtraction (following Accattoli [1]), and which binds \(\texttt{x}\) in \(\texttt{t}\) and adds a free occurrence of \(\texttt{y}\). Intuitively, subtraction can be thought of as \(\textsf{let}\ \texttt{x}=\texttt{y}\texttt{s}\ \textsf{in}\ \texttt{t}\) (which is the notation used by Gallier [33]) but we prefer to avoid such a notation, for various reasons. Firstly, writing \(\texttt{y}\texttt{s}\) we would still be resting on application, while we want to stress that application is not part of the new language, since there is no (@) rule at the logical level. Secondly, in \(\textsf{let}\ \texttt{x}=\texttt{y}\texttt{s}\ \textsf{in}\ \texttt{t}\) the two active premises \(\texttt{x}\) and \(\texttt{s}\) of the \((\Rightarrow _l)\) logical rule are given asymmetric roles, while in
their roles are symmetric. Thirdly, \(\textsf{let}\)-expressions are verbose, thus we adopt a bracket notation.
rather than with
.
is \(\rightarrow _{\texttt{VSC}}\)-normal but not necessarily \(\rightarrow _{\texttt{SC}}\)-normal.
for vanilla \(\lambda \)-terms. The problem however is that the definition of
cannot be the same as for natural terms.
simply as the replacement of \(x\) by \(u\) in \(t\).
introduce left occurrences of \(y\). In contrast to right occurrences, the left ones cannot be simply replaced by a vanilla term \(\texttt{u}\), because
does not belong to the grammar of vanilla terms. Therefore, the definition of meta-level substitution
on vanilla terms is a bit tricky on subtractions.
, we have to inspect the shape of \(\texttt{u}\). The simplest case is when \(\texttt{u}\) is a variable \(\texttt{y}\), since in that case it is possible to simply replace \(\texttt{x}\) by \(\texttt{y}\). A second clear case is when \(\texttt{u}\) is an abstraction \(\lambda \texttt{y}.\texttt{s}\). Then, we can set: 
of the (V)SC) plus putting the resulting term in a second created cut on \(\texttt{z}\) and propagating the substitution
to the sub-terms \(\texttt{r}\) and \(\texttt{t}\) of the subtraction. Note that the two clear cases \(\texttt{u}=\texttt{y}\) and \(\texttt{u}= \lambda \texttt{y}.\texttt{s}\) are exactly those for values, which correspond to the right rules of \(\vdash _{\texttt{S}}\). The full definition of meta-level substitution
for values is in Fig. 8. The following property is proved by induction on \(\texttt{t}\).
.
and
.
. The proof is by induction on \(\texttt{u}\), \(\texttt{L}\), and \(\texttt{C}\). Details are in the Appendix of the technical report [3]. \(\square \)
commute up to \(\rightarrow _{\texttt{dB}}\)).
.
and \(\overline{\langle \cdot \rangle }^{\texttt{S}}:=\langle \cdot \rangle \), and defining them as for terms on the other cases.
translation).
is a \(L\) context and
.
is a \(C\) context and
.
.
, we have: 
with
is \(\rightarrow _{\texttt{VSC}}\)-normal.
. By Proposition 
is a 
commute).
.
. With \(\texttt{y}\) and \(\texttt{z}\) fresh: 
, since \(\texttt{t}= \texttt{L}\langle \texttt{v}\rangle \) for some \(\texttt{L}\) and \(\texttt{v}\), thus
.
. Then: 
is a renaming step, noted \(\texttt{t}\leadsto _{\texttt{ren}\text{- }\texttt{cut}}\texttt{s}\), if \(\texttt{v}\) is a variable.
