Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials

Daniel Rogozin

TL;DR

This work addresses grounding intuitionistic linear logic with multiple subexponentials in a unified syntactic and semantic framework. It introduces ${\bf SILL}(\lambda)_{\Sigma}$, a typed lambda calculus with a subexponential signature ${\Sigma}$, proves strong normalisation and confluence for $β$-reduction using a Girard-style computability approach, and develops a categorical semantics based on Cocteau categories and ${\Sigma}$-assemblages. The paper further characterises relevant categories via copying, realises resource modalities from adjunctions, and connects these to Lafont categories, providing a robust 2-categorical account of the models. The results lay a foundation for resource-aware programming languages with structured modal policies and give tools for future realisability and dependent-type extensions in linear logic.

Abstract

In this paper, we present a typed lambda calculus ${\bf SILL}(λ)_Σ$, a type-theoretic version of intuitionistic linear logic with subexponentials, that is, we have many resource comonadic modalities with some interconnections between them given by a subexponential signature. We also give proof normalisation rules and prove the strong normalisation and Church-Rosser properties for $β$-reduction by adapting the Tait-Girard method to subexponential modalities. Further, we analyse subexponentials from the point of view of categorical logic. We introduce the concepts of a Cocteau category and a $Σ$-assemblage to characterise models of linear type theories with a single exponential and affine and relevant subexponentials and a more general case respectively. We also generalise several known results from linear logic and show that every Cocteau category and a $Σ$-assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions of a particular kind. In the final section, we give a stronger 2-categorical characterisation of Cocteau categories.

Term Assignment and Categorical Models for Intuitionistic Linear Logic with Subexponentials

TL;DR

This work addresses grounding intuitionistic linear logic with multiple subexponentials in a unified syntactic and semantic framework. It introduces , a typed lambda calculus with a subexponential signature , proves strong normalisation and confluence for -reduction using a Girard-style computability approach, and develops a categorical semantics based on Cocteau categories and -assemblages. The paper further characterises relevant categories via copying, realises resource modalities from adjunctions, and connects these to Lafont categories, providing a robust 2-categorical account of the models. The results lay a foundation for resource-aware programming languages with structured modal policies and give tools for future realisability and dependent-type extensions in linear logic.

Abstract

In this paper, we present a typed lambda calculus , a type-theoretic version of intuitionistic linear logic with subexponentials, that is, we have many resource comonadic modalities with some interconnections between them given by a subexponential signature. We also give proof normalisation rules and prove the strong normalisation and Church-Rosser properties for -reduction by adapting the Tait-Girard method to subexponential modalities. Further, we analyse subexponentials from the point of view of categorical logic. We introduce the concepts of a Cocteau category and a -assemblage to characterise models of linear type theories with a single exponential and affine and relevant subexponentials and a more general case respectively. We also generalise several known results from linear logic and show that every Cocteau category and a -assemblage can be viewed as a symmetric monoidal closed category equipped with a family of monoidal adjunctions of a particular kind. In the final section, we give a stronger 2-categorical characterisation of Cocteau categories.

Paper Structure

This paper contains 19 sections, 29 theorems, 30 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Map of the paper
  3. System ${\bf SILL}(\lambda)$ and its syntactic properties
  4. Proof Normalisation
  5. Strong Normalisation and Confluence for $\beta$-reduction
  6. Category-theoretic Preliminaries
  7. 2-categories
  8. Symmetric Monoidal Categories, Cosemigroups and Comonoids
  9. Assemblages and Semantic Interpretation of ${\bf SILL}(\lambda)_{\Sigma}$
  10. Cocteau Categories and Assemblages
  11. On Soundness and Completeness
  12. Characterising Relevant Categories
  13. Cocteau Categories and Resource Modalities
  14. Modalities from Adjunctions
  15. Constructing a Cocteau adjunction from a Cocteau category
  16. ...and 4 more sections

Key Result

Lemma 2.4

If $\Gamma \vdash M : A$ and $\Delta, x : A \vdash N : B$, then $\Delta, \Gamma \vdash N [x := M] : B$.

Figures (2)

  • Figure 1: System ${\bf SILL}(\lambda)_{\Sigma}$
  • Figure 7: ${\bf SILL}(\lambda)_{\Sigma}$ in $\Sigma$-assemblages

Theorems & Definitions (88)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3: Preterms
  • Lemma 2.4: Substitution Lemma
  • proof
  • Definition 2.5
  • Theorem 2.6: Normalisation
  • proof
  • Theorem 2.7
  • Definition 2.8
  • ...and 78 more