arXiv subjects

Rémi Di Guardia

Publications and source records attributed to Rémi Di Guardia.

4 recordsLinked to original sources

arXiv2026

Quantum Bayesian Networks: Compositionality and Typing via Linear Logic

Quantum Bayesian networks provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. They generalize Pearl's Bayesian networks -- prominent graphical models for classical probabilistic reasoning and inference. The goal of this paper is to bring compositional principles and a typing discipline into this setting. A key feature of our compositional semantics is that when all causes are classical, it coincides with the standard factor-based semantics of Bayesian networks, while in the purely quantum case it reduces to tensor networks. We then propose a typed formalism based on linear logic proof-nets, where types ensure well-behaved composition of systems, and which we prove sound and complete with respect to quantum Bayesian networks.

cs.LO↗

arXiv2026

Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic

We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting vertex, which we can impose to be a par-vertex, or a terminal vertex, or a non-axiom vertex, etc., in a modular way. This approach applies in presence of the mix-rules as well as for proof nets of unit-free multiplicative-additive linear logic (through an appropriate further generalization of Yeo's theorem). The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) -- similar results from the literature required more involved encodings.

cs.LO↗

arXiv2026

Bayesian Networks and Proof-Nets: the proof-theory of Bayesian Inference

We study the correspondence between Bayesian Networks and graphical representation of proofs in linear logic. The goal of this paper is threefold: to develop a proof-theoretical account of Bayesian inference (in the spirit of the Curry-Howard correspondence between proofs and programs), to provide compositional graphical methods, and to take into account computational efficiency. We exploit the fact that the decomposition of a graph is more flexible than that of a proof-tree, or of a type-derivation, even if compositionality becomes more challenging.

cs.LO↗

arXiv2025

Type Isomorphisms for Multiplicative-Additive Linear Logic

We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus in *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and cancellation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We use the sequent calculus to extend our results to full MALL, including all units, thanks to a study of cut-elimination and rule commutations.

cs.LO↗