Homotopy span model simplifies proofs in linear logic with shuffles
An explicit shuffle construction of the homotopy span model of differential linear logic
Logic in Computer Science
Summary
Linear logic uses mathematical structures to represent how information flows and combines. The authors build on a way to represent logical proofs using categories and homotopy theory, which studies shapes and their transformations. By relaxing some technical conditions, they create a simpler model where key proof components are represented more intuitively, and certain symmetries are captured by a 'shuffle' operation. This work clarifies the mathematical foundations connecting logic, category theory, and algebraic structures.
What this means in practice
- •For programming language designers: Use the homotopy span model to develop more modular and compositional semantics for resource-sensitive languages.
- •For formal verification engineers: Apply the simplified model of linear logic proofs to improve formal reasoning tools handling concurrency and resource usage.
A theory result. No direct application yet.
Authors
Paul-André Melliès, Federico Olimpieri, Lionel Vaux Auclair
Abstract
We give a direct and explicit construction of the homotopy span model of linear logic originally formulated by Melliès using abstract homotopy theory in the Quillen category Cat of small categories equipped with its natural model structure. Following the principles of homotopy theory, the formulas and proofs of linear logic are interpreted in the model as small categories up to categorical equivalence, the notion of weak homotopy equivalence underlying the natural Quillen model structure on Cat. Here, we explain how the original interpretation of proofs as fibrant spans can be replaced by a more liberal interpretation of proofs as separately fibrant spans. This relaxation from fibrant spans to separately fibrant spans enables us to give a simple and intuitive description of the homotopy span model, where the axiom and cut links are interpreted as identity spans, and where the symmetries of the exponential modality are captured by a shuffle structure on the interpretation of proofs.