An Algebraic Extension of Intuitionistic Linear Logic: The $L_{!}^S$-Calculus and Its Categorical Model

Abstract

We introduce the $L_{!}^S$-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic (ILL). These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the $L_{!}^S$-calculus as an extension of the $L^S$-calculus with the $!$ modality. We prove key meta-theoretical properties--subject reduction, confluence, strong normalisation, and an introduction property--as well as preserve the expressiveness of the original $L^S$-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.

arXiv admin note: substantial text overlap with arXiv:2310.08517

References in corpus (3)

• A New Connective in Natural Deduction, and its Application to Quantum Computing
• A linear linear lambda-calculus
• A linear proof language for second-order intuitionistic linear logic