Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)

Beniamino Accattoli

TL;DR

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.

Abstract

Existing Curry-Howard interpretations of call-by-value evaluation for the $λ$-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.

The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)

TL;DR

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.

Abstract

Existing Curry-Howard interpretations of call-by-value evaluation for the -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.
Paper Structure (52 sections, 34 theorems, 9 equations, 8 figures)

This paper contains 52 sections, 34 theorems, 9 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Call-by-Value and Natural Deduction.
  3. Call-by-Value and Proof Theory.
  4. The Vanilla Sequent Calculus.
  5. Cut Elimination at a Distance: the Vanilla $\lambda$-Calculus.
  6. Results.
  7. How Our Approach Fits in the Literature.
  8. Non-Canonicity vs Sharing.
  9. Proofs
  10. Natural Deduction, Call-by-Name, and Rewriting at a Distance
  11. Routine Definitions: Terms and Contexts.
  12. Routine Definitions: Types and Derivations.
  13. Left and Right Rules.
  14. Detours.
  15. Explicit Substitutions.
  16. ...and 37 more sections

Key Result

proposition 4.1

Let $\mathtt{t}\in\Lambda_{\mathtt{S}}$ be cut-free. Then $\underline{\mathtt{t}}_{\mathtt{N}}$ is $\rightarrow_{\mathtt{VSC}}$-normal but not necessarily $\rightarrow_{\mathtt{SC}}$-normal.

Figures (8)

  • Figure 1: Vanilla sequent calculus for minimal intuitionistic logic (MIL).
  • Figure 2: $\lambda$-calculus and natural deduction $\vdash_{\mathtt{N}}$.
  • Figure 3: Substitution Calculus (SC).
  • Figure 4: Plotkin's (natural) CbV $\lambda$-calculus.
  • Figure 5: Value Substitution Calculus (VSC).
  • ...and 3 more figures

Theorems & Definitions (75)

  • proposition 4.1
  • proof
  • lemma 5.1
  • proposition 5.1: Subject reduction
  • proof
  • lemma 6.1: Substitution and $\underline{\cdot}_{\mathtt{N}}$ commute up to $\rightarrow_{\mathtt{dB}}$
  • lemma 6.2: Contexts and $\underline{\cdot}_{\mathtt{N}}$ translation
  • proposition 6.1: VSC simulates vanilla
  • proof
  • lemma 6.3: Preservation of VSC termination
  • ...and 65 more