Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Adjoint Natural Deduction (Extended Version)

Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka

TL;DR

The work addresses integrating multiple substructural logics through mode-indexed adjoint modalities and provides a constructive natural deduction formulation that aligns with the adjoint sequent calculus. It delivers verifications as long-normal-form analogues, a bidirectional natural-deduction system, translations to and from sequent proofs, and a dynamics with an abstract machine; recursion and call-by-need are supported via contextual definitions and provisional bindings, together with an algorithmic type checker. The framework yields mode-driven properties such as garbage-freedom for linear modes, strictness, and erasure, and it generalizes graded/subexponential logics to model monads and comonads within a unified proof-theoretic setting. These results offer a robust, mode-aware computational interpretation with substructural guarantees that can inform programming language design and staged computation, beyond prior approaches to adjoint or graded logics.

Abstract

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.

Adjoint Natural Deduction (Extended Version)

TL;DR

The work addresses integrating multiple substructural logics through mode-indexed adjoint modalities and provides a constructive natural deduction formulation that aligns with the adjoint sequent calculus. It delivers verifications as long-normal-form analogues, a bidirectional natural-deduction system, translations to and from sequent proofs, and a dynamics with an abstract machine; recursion and call-by-need are supported via contextual definitions and provisional bindings, together with an algorithmic type checker. The framework yields mode-driven properties such as garbage-freedom for linear modes, strictness, and erasure, and it generalizes graded/subexponential logics to model monads and comonads within a unified proof-theoretic setting. These results offer a robust, mode-aware computational interpretation with substructural guarantees that can inform programming language design and staged computation, beyond prior approaches to adjoint or graded logics.

Abstract

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.
Paper Structure (8 sections, 23 theorems, 19 equations, 6 figures)

This paper contains 8 sections, 23 theorems, 19 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Adjoint Sequent Calculus
  3. Adjoint Natural Deduction
  4. Relating Sequent Calculus and Natural Deduction
  5. Dynamics
  6. Adding Recursion and Call-by-Need
  7. Algorithmic Type Checking
  8. Conclusion

Key Result

theorem 1

The following are admissible:

Figures (6)

  • Figure 1: Implicit Adjoint Sequent Calculus
  • Figure 2: Expressions for Bidirectional Natural Deduction
  • Figure 3: Implicit Bidirectional Natural Deduction
  • Figure 4: Machine States
  • Figure 5: Computation Rules
  • ...and 1 more figures

Theorems & Definitions (39)

  • theorem 1: Admissibility of Weakening and Contraction
  • theorem 2: Admissibility of Cut and Identity
  • theorem 3: Substitution Property
  • proof
  • lemma 1: Substitution Split
  • proof
  • theorem 4: From Sequent Calculus to Natural Deduction
  • proof
  • theorem 5: From Natural Deduction to Sequent Calculus
  • proof
  • ...and 29 more