Date: Tuesday, Janary 7th 2025 – 13h00
Place: A008
Title: Sup, Sum, and Scalars: In Linear Logic and in Non-Linear Logic
In [1], we introduced a new connective, called “sup”, to intuitionistic propositional logic to model information erasure, non-reversibility, and non-determinism, as observed in quantum measurement, among other contexts. This connective features the introduction rule of conjunction and the elimination rule of disjunction, resulting in a non-deterministic cut-elimination process. To enrich its proof terms, we added a sum operator, which allows for recovering the determinism of the connective. Additionally, since one of our goals was to express quantum programs, we introduced a scalar product. These rules may occupy the space between the introduction and elimination of a given connective, forcing us to include commuting cuts to establish a proper introduction theorem.
The next step toward transforming this calculus into a quantum calculus was to adopt a linear logic framework. Thus, in [2], we considered the full intuitionistic multiplicative-additive linear logic (IMALL). We proved that, when removing the sup connective, the system–augmented with sums and scalar multiplication–is linear in the algebraic sense. Specifically, any term t applied to a linear combination a⋅r+b⋅s is observationally equivalent to a⋅(tr)+b⋅(ts).
In [3], we provided an abstract characterization of the sup connective in IMALL, showing that any symmetric monoidal closed category with biproducts and a monomorphism from the semiring of scalars to the semiring Hom(I,I) is a suitable model. By leveraging the binary biproducts, we defined a weighted codiagonal map, which serves as the core of the sup connective.
Finally, in [4], we considered two non-linear systems: first, with the sum operator alone as a parallel operator, and second, with the combination of the sum and scalar operators as an algebraic lambda calculus. We proposed two categorical models for these calculi. In particular, we explored the role of disjunction within the calculus, which has rarely been studied in conjunction with the parallel (or sum) construct. For the parallel lambda calculus, we employed the category MagSet, whose objects are magmas and whose morphisms are functions from the category Set. For the algebraic lambda calculus, we used the category AMagSSet, whose objects are action magmas, with morphisms similarly drawn from Set. Our approach diverges from conventional interpretations, which typically handle disjunctions via coproducts. Instead, we proposed handling them through a combination of disjoint unions and Cartesian products.
References:
[1] A. Díaz-Caro and G. Dowek. A new connective in natural deduction, and its application to quantum computing. TCS 957:113840, 2023.
[2] A. Díaz-Caro and G. Dowek. A linear linear lambda-calculus. MSCS FirstView:1-15, 2024.
[3] A. Díaz-Caro and O. Malherbe. The Sup Connective in IMALL: A Categorical Semantics. arXiv:2205.02142, 2024.
[4] A. Díaz-Caro and O. Malherbe. Parallel and algebraic lambda-calculi in intuitionistic propositional logic. arXiv:2408.16102, 2024.
