Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A linear proof language for second-order intuitionistic linear logic

Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe

TL;DR

This work extends the ${\mathcal{L}}^{\mathcal{S}}$-calculus to a second-order, polymorphic linear language ${\mathcal{L}}_2^{\mathcal{S}}$ for intuitionistic linear logic by adding the exponential connective and universal quantification. It proves key correctness properties—Subject Reduction, Confluence, Strong Normalisation, and Introduction Property—using Girard's ultra-reduction and reducibility candidates, while preserving existing encodings for vectors and matrices. The paper then demonstrates that vectors and matrices can be faithfully represented as proof-terms and extends this with a matrix-iterator to simulate iterative matrix applications, enabling a natural encoding of numerical linear algebra within the logic. A central result is the Linearity theorem: for closed terms $t:A\to B$ and $u_1,u_2:A$, the term behaves linearly in its argument up to observational equivalence, supporting a rigorous algebraic treatment of linear maps in the proof-language and paving the way for second-order, linear-semantics frameworks applicable to quantum and probabilistic programming.

Abstract

We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.

A linear proof language for second-order intuitionistic linear logic

TL;DR

This work extends the -calculus to a second-order, polymorphic linear language for intuitionistic linear logic by adding the exponential connective and universal quantification. It proves key correctness properties—Subject Reduction, Confluence, Strong Normalisation, and Introduction Property—using Girard's ultra-reduction and reducibility candidates, while preserving existing encodings for vectors and matrices. The paper then demonstrates that vectors and matrices can be faithfully represented as proof-terms and extends this with a matrix-iterator to simulate iterative matrix applications, enabling a natural encoding of numerical linear algebra within the logic. A central result is the Linearity theorem: for closed terms and , the term behaves linearly in its argument up to observational equivalence, supporting a rigorous algebraic treatment of linear maps in the proof-language and paving the way for second-order, linear-semantics frameworks applicable to quantum and probabilistic programming.

Abstract

We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.
Paper Structure (22 sections, 49 theorems, 34 equations, 3 figures)

This paper contains 22 sections, 49 theorems, 34 equations, 3 figures.

Table of Contents

  1. Introduction
  2. The LS2-calculus
  3. Correctness
  4. Subject reduction
  5. Confluence
  6. Strong normalisation
  7. Introduction property
  8. Encodings
  9. Vectors
  10. Matrices
  11. Matrix iterator
  12. Linearity
  13. Observational equivalence
  14. Measure of a proof-term
  15. Elimination contexts
  16. ...and 7 more sections

Key Result

theorem 1

If $\Xi; \Gamma \vdash t:A$ and $t \longrightarrow u$, then $\Xi; \Gamma \vdash u:A$.

Figures (3)

  • Figure 1: The proof-terms of the ${\mathcal{L}}_2^{\mathcal{S}}$-calculus.
  • Figure 2: The deduction rules of the ${\mathcal{L}}_2^{\mathcal{S}}$-calculus.
  • Figure 3: The reduction rules of the ${\mathcal{L}}_2^{\mathcal{S}}$-calculus.

Theorems & Definitions (107)

  • theorem 1: Subject reduction
  • proof
  • theorem 2: Confluence
  • proof
  • definition 1: Ultra-reduction
  • definition 2
  • definition 3: Reducibility candidates
  • definition 4
  • definition 5
  • lemma 1
  • ...and 97 more