Thomas Ehrhard

Claudia Faggian

Michele Pagani

The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic

Keywords: 2012 ACM Subject Classification Theory of computation → Linear logic, Theory of computation → Denotational semantics, Mathematics of computing → Variable elimination Keywords and phrases Linear Logic, Proof-Nets, Denotational Semantics, Probabilistic Programming Digital Object Identifier 10.4230/LIPIcs.FSCD.2023.8

We consider an extension of multiplicative linear logic which encompasses bayesian networks and expresses samples sharing and marginalisation with the polarised rules of contraction and weakening. We introduce the necessary formalism to import exact inference algorithms from bayesian networks, giving the sum-product algorithm as an example of calculating the weighted relational semantics of a multiplicative proof-net improving runtime performance by storing intermediate results.

Introduction

Linear logic [START_REF] Girard | Linear logic[END_REF] provides a linear algebra flavour to logic, associating linear algebra operations with logical connectives, e.g. tensor ⊗ is seen as a form of conjunction, direct sum ⊕ as a disjunction and duality as an involutive negation (•) ⊥ . This perspective has given many insights. In denotational semantics, we have quantitative semantics, e.g. [START_REF] Lamarche | Quantitative domains and infinitary algebras[END_REF][START_REF] Girard | Between logic and quantic: a tract[END_REF][START_REF] Ehrhard | On Köthe sequence spaces and linear logic[END_REF][START_REF] Ehrhard | Finiteness spaces[END_REF][START_REF] Danos | Probabilistic coherence spaces as a model of higher-order probabilistic computation[END_REF][START_REF] Laird | Weighted relational models of typed lambda-calculi[END_REF]: a family of models denoting λ-terms and functional programs with some notion of analytic maps or power series that can be locally approximated by multilinear functions, these latter denoting linear logic proofs. In proof-theory, we have proof-nets: a representation of proofs and programs expressing the interdependences of these algebraic operations in a graph-theoretical fashion.

Quantitative semantics turns out to be particularly suitable for probabilistic programming, giving fully abstract semantics [START_REF] Ehrhard | Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF[END_REF][START_REF] Ehrhard | Full abstraction for probabilistic pcf[END_REF][START_REF] Ehrhard | Probabilistic call by push value[END_REF], denoting probabilistic programs with very regular functions (absolutely monotone) even on "continuous" datatypes (e.g. real numbers) [START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[END_REF][START_REF] Crubillé | Probabilistic stable functions on discrete cones are power series[END_REF][START_REF] Ehrhard | Cones as a model of intuitionistic linear logic[END_REF], giving a compositional analysis of various operational behaviours, such as runtime or liveness [START_REF] Laird | Weighted relational models of typed lambda-calculi[END_REF], providing suitable notions of program metrics [START_REF] Ehrhard | Differentials and distances in probabilistic coherence spaces[END_REF]. Due to this expressivity, calculating the quantitative denotations for a Turing complete programming language is obviously non-computable, but we can fix on relevant fragments supporting an effective procedure. Effectiveness is a relevant feature for a denotational model, as it can provide automatic tools for verifying program correctness, as well as the other mentioned operational properties.

Let us focus our attention to one of the simplest fragments of linear logic: the multiplicative fragment (MLL), which has the ⊗ conjunction, its unit 1 and their respective duals, the par (a disjunction different from ⊕) and ⊥ = 1 ⊥ . From a programming perspective, this fragment contains (although it is not restricted to) an exponential-free fragment of the linear λ-calculus 8:2 Sum-Product for MLL with tuples, e.g. [START_REF] Benton | Linear lambda-calculus and categorical models revisited[END_REF]: the linear functional type F ⊸ G is in fact represented by F ⊥ `G. Although very simple, this fragment is already surprisingly expressive on probabilistic data. First, positive types (i.e. combinations of 1, ⊕ and ⊗) express linear combinations of the values of a finite data-type. For example, the quantitative denotation of 1 ⊕ 1 contains linear combinations of booleans and can be used to model boolean random variables 1 . Moreover, it is known since the inception of polarised linear logic that positive formulas are endowed with a polarised version of the structural rules of weakening and contraction ( [START_REF] Girard | A new constructive logic: classical logic[END_REF] and Remark 3), so one can represent λ-terms having multiple occurrences of a same boolean variable without breaking the linearity features of MLL. In probabilistic programming, these occurrences duplicate the samples from a random variable, but not the random variable itself. Finally, we can allow semantical boxes expressing matrices indexed by finite data-types, which can express conditional probabilities. We call this system quantitative MLL (Section 2).

As for the semantics, let us focus on the R ≥0 -weighted relation semantics (see Section 3 and [24]), which is one of the most basic examples of quantitative semantics, allowing to model probabilistic programs over countable data-types. The denotation of a proof-net is then a vector of dimension equal to the number of the possible samples of a probabilistic distribution computed by the proof-net. This vector is computable for quantitative MLL and the standard semantical definitions yield a recursive procedure (Figure 1c) to compute it. In practice, this procedure is unfeasible, as it is exponential in time and in space with respect to the size of the proof-net. The goal of this paper is to inaugurate a new approach for improving it by taking inspiration from bayesian networks, which have partially a similar graph-theoretical structure as proof-nets.

For example, the R ≥0 -weighted denotation of a proof-net describing a probabilistic distribution over a tuple of n booleans is a vector of dimension 2 n (the number of the possible outcomes of a random variable over n booleans), independently whether the values of some of these booleans depend each other or not (Example 9). The proof-net carries very clearly these interdependences via paths over boolean edges: may we reduce the dimension of its denotation by following such a structure? On a different note, the composition of two proof-nets on a tuple of n booleans yields a sum of 2 n terms (Example 11). However, this composition can be ordered by following the switching paths over the corresponding cuts. May we refactor the sum according to this order and gain in efficiency by memorising some intermediate factors?

Similar questions are typical of the research on Bayesian networks ( [START_REF] Pearl | Probabilistic reasoning in intelligent systems -networks of plausible inference[END_REF], see as reference [START_REF] Darwiche | Modeling and Reasoning with Bayesian Networks[END_REF]), these latter being directed graphs expressing the conditional dependences between different random variables. The benefit of this approach is to provide a battery of algorithms computing, e.g., marginal distributions in a quite efficient way by taking advantage of the graph-theoretical structure of a network. Our general goal is to inaugurate a new approach to quantitative semantics which pays attention to the cost of computing the semantics, and we do so by exploiting techniques form Bayesian inference. One paradigmatic example is the sum-product variable elimination algorithm [START_REF] Zhang | A simple approach to bayesian network computations[END_REF]: we propose here a formalism for computing the semantics of a quantitative MLL proof-net by adapting this algorithm (here Algorithm 1).

Related works.

Bayesian networks form, mutatis mutandis, a strict subset of quantitative MLL proof-nets (Remark 1), morally the set of those proof-nets which do not contain formulas alternating polarities, e.g. alternation of ⊗ and `connectives. This correspondence has been already acknowledged, with a slight different terminology, by the recent literature about the semantical foundations of Bayesian programming. We mention in particular [START_REF] Cho | Disintegration and bayesian inversion via string diagrams[END_REF][START_REF] Jacobs | Causal inference by string diagram surgery[END_REF] which represent Bayesian networks as string diagrams and analyse the notion of disintegration. The paper [START_REF] Paquet | Bayesian strategies: probabilistic programs as generalised graphical models[END_REF] proposes a game semantics based on event structures for a variant of the linear λ-calculus underlined by quantitative MLL. The paper [START_REF] Stein | Compositional semantics for probabilistic programs with exact conditioning[END_REF] studies an equational theory and provides a denotational semantics based on matrices for this calculus when restricted to ground data-types. However, to our knowledge, our paper is the first time that the efficiency of computing the semantics is taken into consideration. Moreover, we show that the techniques of Bayesian networks can be adapted to the more general framework of quantitative MLL without so much effort.

Paper outline. Section 2 introduces quantitative MLL proof-nets and Section 3 its associated R ≥0 -weighted relational semantics. Section 4 revisits the standard notion of factor in Bayesian inference so to apply it to atomic proof-nets in Section 5 and to general proof-nets in Section 6. Section 7 concludes by mentioning some future developments.

Quantitative Multiplicative Linear Logic

Metavariables X, Y, Z will vary over a countable set of propositional variables. The grammar of the formulas of MLL is given by (together with its metavariables):

F, G, H ::= X + | X -| 1 | ⊥ | F ⊗ G | F `G. (1)
We call X + (resp. X -) a positive atomic formula (resp. negative atomic formula) over the variable X, the superscript symbol + (resp. -) being its polarity. We will write X • for a generic atomic formula over X, if we do not want to precise its polarity. The linear logic negation is introduced as syntactical sugar: (X + ) ⊥ ::= X -, 1 ⊥ ::= ⊥, (F ⊗G) ⊥ ::= F ⊥ `G⊥ , and for the dual cases (X -, ⊥, `), (F ⊥ ) ⊥ ::= F . A sequent is a finite sequence F 1 , . . . , F n of MLL formulas. Capital Greek letters Γ, ∆, . . . will vary over sequents. Given a sequent Γ = F 1 , . . . , F n , we write Γ ⊥ for the sequent F ⊥ 1 , . . . , F ⊥ n . Moreover, if n > 0, we write `Γ (resp. ⊗Γ) for the formula

F 1 `(• • • `Fn ) (resp. F 1 ⊗ (• • • ⊗ F n )). If Γ is empty (i.e. n = 0), `Γ (resp. ⊗Γ) will mean ⊥ (resp. 1).
As accustomed in linear logic, sequent proofs are represented by special graphs, called proof-nets. Figure 1e gives an example of two proof-nets: N at the left side of the arrow * -→, and N 0 at the right side. A proof-net is a labelled directed acyclic graph2 (DAG for short) such that the edges are labelled by MLL formulas and the nodes by deduction rules of our extended MLL, i.e. by a symbol among: ax (axiom), cut (cut), 1 (one), ⊗ (tensor), ⊥ (bottom), `(par), w (weakening), c (contraction), b (semantical box or simply box). The nodes of the proof-nets in Figure 1e are represented just by their labels, except for the box which is depicted as a rectangular and labeled by an enumerated occurrence of b. The label of a node determines the number of incoming edges (called premises of the node) and the number of outgoing edges (called conclusions of the node), as well as the type of formulas labelling these edges, according to the rules sketched in Figure 1a. The edges will be oriented top-bottom, so that axioms, ones, bottoms, weakenings and boxes have no premises, while cuts have no conclusions. Figure 1e does not explicit all formulas labelling the edges of N and N 0 , in fact these formulas can be recovered by the axioms and boxes labelling and the rules sketched in Figure 1a. Proof-nets have edges without targets which are called the conclusions of the proof-net. Both N and N 0 have one single conclusion, labelled by X + 4 ⊗ X + 5 . Not all DAGs of MLL nodes are proof-nets: the set of proof-nets is the subset of the set of all DAGs which can be generated inductively by the rules sketched in Figure 1b. We call atomic a proof-net whose edges are only labelled with atomic formulas. Notice that atomic proof-nets can contain only axioms, cuts, weakening, contractions and semantical boxes.

▶ Example 1. The (atomic) proof-net N 0 in Figure 1e is mutatis mutandis an example of a Bayesian network as expressed by quantitative MLL. The propositional variables X 1 , . . . , X 5 are place-holders for (sets of the possible outcomes of) random variables and the semantical boxes are place-holders for their associated "conditional probabilistic tables" (we borrow here the terminology of [START_REF] Darwiche | Modeling and Reasoning with Bayesian Networks[END_REF]). For example, the box b 4 is a place-holder for a probabilistic distribution over the variable X 4 conditioned by the outcomes of the variables X 2 and X 3 . The polarities discriminate between input and output occurrences in a conditional probabilistic table. These place-holders will be instantiated with concrete conditional distributions by the semantics, as detailed in Section 3.

The acquainted reader in Bayesian graphs should be convinced that these latter are depicted plainly in this syntax just by adding cuts transforming outputs into inputs. Notice that by inverting the orientation of the edges labelled by negative atoms, we get exactly the same directed paths between the nodes of the corresponding Bayesian network. Of course, MLL allows for more nets than Bayesian graphs, for example the proof-net N at left of the * -→ arrow is not bayesian, namely it has par nodes. But yet, Remark 54 will allude to a correspondence between N and a run of the sum-product algorithm over N 0 . Our goal is to show how Bayesian graph algorithms can be imported in this more general setting. ▶ Remark 2. Some papers, e.g. [START_REF] Cho | Disintegration and bayesian inversion via string diagrams[END_REF][START_REF] Jacobs | Causal inference by string diagram surgery[END_REF], represent Bayesian graphs as string diagrams, which is a graphical syntax omitting the axiom and cut nodes. Although one can present MLL in a similar way by using Lafont's interaction nets [START_REF] Lafont | From proof nets to interaction nets[END_REF], we prefer to keep axioms and cuts explicit as they condense the main threats to an efficient computation of the semantics which is a core topic of this paper. ▶ Remark 3. We allow for structural rules (weakening and contraction) on negative atomic formulas. In fact, as it will be clear in Section 3, negative atoms will be interpreted by finite products of bottoms ˘x∈S ⊥ (although we do not detail here the additive connectives & and ⊕ and the exponential modalities ? and !). It is well-known since the inception of polarized linear logic [START_REF] Girard | A new constructive logic: classical logic[END_REF] that ⊥ is isomorphic to the exponential formula ?0, so that the structural rules of ? can be lifted to ˘x∈S ⊥, extending the expressivity of MLL. One might even allow the structural rules to all formulas of negative polarity, but we preferred to restrict to atomic formulas to ease the presentation, namely cut reduction. ▶ Remark 4. A less standard extension is given by the semantical boxes b, which are place holders for conditional distributions or, more generally, matrices. For technical convenience, we restrict their conclusions (as well as those of MLL axioms) to be atomic formulas with exactly one occurrence of a positive formula. The structural rules of contractions and weakenings take then a precise operational meaning: a cut between the positive conclusion of a box and a contraction duplicates the samples of the probabilistic distribution associated with . . .

X - 1 ⊗ F G 1 1 F cut F ⊥ ax X - X + F G ⊥ ⊥ c X - X - w X - X - n Y + b X - F `G F ⊗ G
⊥ (N ) = ⊥ ⊥ . . . N ∆ b = . . . X1 - Xn - Y + b ax X = ax X - X + `(N F,G ) = F G . . . ∆ N F `G N F ⊗ N ′ F ′ = ⊗ F G F ⊗ G . . . ∆ . . . ∆ N N cut(N F , N ′ F ⊥ ) = cut F F ⊥ . . . ∆ . . . ∆ N N w(N X -) = w X - . . . N ∆ c(N X -,X -) = c X - X - . . . ∆ N X - mix(N , N ′ ) = . . . ∆ . . . ∆ N N (b)
Sequent rules generating the set of proof-nets. The notation N Γ in the subscript of a rule stands for the pair of a proof-net N and a sequence Γ of conclusions of N , which will be "active" in the rule.

empty ⋆ = one ⋆ = 1 ⊥ (N ) ( ⃗ d,⋆) = N ⃗ d b (⃗ x,y) = ι(b) (⃗ x,y) ax X x,x ′ = δ x,x ′ `(N ) ( ⃗ d,(x,y)) = N ( ⃗ d,x,y) N ⊗ N ′ ( ⃗ d, ⃗ d ′ ,(x,y)) = N ( ⃗ d,x) N ′ ( ⃗ d ′ ,y) cut(N , N ′ ) ⃗ d, ⃗ d ′ = x∈ F N ⃗ d,x N ′ ⃗ d ′ ,x w(N ) ( ⃗ d,x) = N ⃗ d c(N ) ( ⃗ d,x) = N ( ⃗ d,x,x) mix(N , N ′ ) ( ⃗ d, ⃗ d ′ ) = N ⃗ d N ′ ⃗ d ′
(c) Inductive definition of the interpretation N ι by induction on a sequence of sequent rules giving N , we omit to explicit the valuation ι as well as the active sequent in the sequent rule.

ax cut ax cut 1 ⊥ 1/⊥ graph ⊗ F G G ⊥ `F cut cut cut G G ⊥ F ⊥ F ⊥ ⊗/è mpty (d) MLL cut-reduction rewriting steps. c X + 2 X - 1 X - 1 X + 1 X - 2 X - 3 X + 3 X - 2 ⊗ X + 4 X + 5 X + 4 ⊗ X + 5 b 1 b 5 b 4 b 2 b 3 cut `⊗ c ax ax c ⊗ `ax ⊗ cut cut X - 2 X + 2 ⊗ X + 4 X + 2 ⊗ (X - 2 `X+ 3 ) X - 1 * -→ X + 1 c c X + 5 X - 3 ⊗ X - 2 X + 3 X - 1 X + 2 X - 1 X + 4 X - 2 X + 4 ⊗ X + 5 b 5 b 4 b 3 b 2 b 1 c cut X - 2 cut X - 2 cut (e) Example of two proof-nets of conclusion X + 4 ⊗ X + 5 such that N * -→ N0.
The labelling of some edges is omitted.

Figure 1

The proof-net syntax and weighted-relational semantics of quantitative MLL.

F S C D 2 0 2 3 8:6

Sum-Product for MLL the box, while weakenings maginalise out this distribution. These operations are categorically axiomatised by the so-called CD-structure, for "copier" and "discarder", e.g. [START_REF] Jacobs | Causal inference by string diagram surgery[END_REF][START_REF] Stein | Compositional semantics for probabilistic programs with exact conditioning[END_REF]. We explicit here how the structural polarised linear logic rules perfectly fulfil this rôle, showing a natural Curry-Howard correspondence with Bayesian programming.

Given a proof-net N and an edge e of N , we write by e : F whenever e is labelled by the formula F . By ease of notation, we often write the sequent F 1 , . . . , F n synonymously for an enumeration e 1 : F 1 , . . . , e n : F n of labelled edges, if the edges e 1 , . . . , e n are clear from the context or inessential. We write N : ∆ whenever the sequent ∆ enumerates the (formulas labelling the) conclusions of N , also speaking about ∆ as simply the conclusions of N .

Cut-reduction is defined as a graph-rewriting, replacing a subgraph containing a cut (the redex) with a new subgraph (the contractum) having the same pending edges. Figure 1d sketches the three different kinds of MLL redexes: ax, 1/⊥, ⊗/`. We will write N -→ N ′ if N rewrites into N ′ by one single rewriting step. The fact that N ′ is still a proof-net is proven by using the so-called correctness criteria (see [START_REF] Girard | Linear logic[END_REF] for details). We denote by * -→ the reflexive and transitive closure of -→. A normal form is a proof-net which contains no redex of any kind {ax, 1/⊥, ⊗/`}. Cut-reduction is confluent and strong normalising [START_REF] Girard | Linear logic[END_REF].

▶ Example 5. Figure 1e gives an example of a proof-net N that rewrites into the normal form N 0 . Notice that cuts between structural nodes (weakening and contraction) and boxes are not reduced (see Remark 6) so that the normal form N 0 yet contains some cuts. Notice also that different sequences of rewriting steps may start from N but all of them can be eventually completed into N 0 , in accordance with the confluence property.

▶ Remark 6. Weakening and contraction do not erase nor duplicate semantical boxes as this rewriting would break the correspondence with Bayesian networks mentioned in Example 1. In fact, if we rewrote a cut between a contraction and a box b into two distinct copies of b, then this would correspond to create two independent and identically distributed random variables out of a single one and not to duplicate a sample of this latter. The sharing nodes in bayesian networks share samples of random variables but do not duplicate random variables (see [START_REF] Darwiche | Bayesian networks[END_REF]). We will discuss this point also in Example 8 using the weighted relational semantics.

Weighted Relational Semantics

The quantitative semantics of linear logic refers to a family of denotational models based on linear algebra constructions (tensors, linear functions, direct sums, dual spaces, etc.). Many examples are known in the literature, such as finiteness and Koethe spaces [START_REF] Ehrhard | Finiteness spaces[END_REF][START_REF] Ehrhard | On Köthe sequence spaces and linear logic[END_REF], weighted relations [START_REF] Laird | Weighted relational models of typed lambda-calculi[END_REF], probabilistic coherence spaces [START_REF] Danos | Probabilistic coherence spaces as a model of higher-order probabilistic computation[END_REF], coherent Banach spaces [START_REF] Girard | Coherent banach spaces: a continuous denotational semantics[END_REF] etc. The common idea is to associate types with a mathematical structure underlying a notion of vector space (or a module) and the poofs with linear maps represented by matrices, or simply vectors in case of proof-nets. We consider here one of the most basic examples of quantitative semantics, the "relations" weighted by non-negative real numbers, but the results of this paper can be adapted trivially to any quantitative semantics mentioned above. The model of R ≥0 -weighted relations is a variant of the relational semantics of linear logic (see e.g. [START_REF] Bucciarelli | On phase semantics and denotational semantics: the exponentials[END_REF]), where the notion of a subset of a set S, seen as a vector (b x ) x∈S of booleans expliciting whether an element x ∈ S belongs or not to the subset, is generalised to a vector of non-negative real numbers. This model is known and we thus just sketch here the interpretation of quantitative MLL proof-nets, referring the reader to [START_REF] Laird | Weighted relational models of typed lambda-calculi[END_REF] for more details.

Let us fix some basic notation. Metavariables S, T, U range over finite sets 3 . We denote by R ≥0 the cone of the non-negative real numbers. Metavariables ϕ, ψ, ξ will range over vectors in R S ≥0 , ϕ x denoting the scalar associated with x ∈ S by ϕ ∈ R S ≥0 . The identity matrix over a set S, also called diagonal matrix or Kronecker delta, is denoted δ ∈ R S×S ≥0 and defined by δ a,a ′ = 1 if a = a ′ , otherwise δ a,a ′ = 0. ▶ Example 7. The simplest example we consider is the singleton set {⋆}, for some irrelevant element ⋆. The singleton will be associated with multiplicative units 1 and ⊥ and it induces the module of scalars, as R ≥0 {⋆} ≃ R ≥0 . The module of couples of non-negative real numbers is instead induced by any set of cardinality 2, like the set of booleans {t, f}: R {t,f} ≥0

≃ R 2 ≥0 . In all the examples of this paper, we will in fact associate the propositional variables with the set {t, f}, so that a proof-net with only one atomic conclusion will be interpreted with a vector (λ t , λ f ), giving a "score" to the two booleans. Notice that R 2 ≥0 = R ≥0 ⊕ R ≥0 , with ⊕ denoting the direct sum over modules. This is reflected in linear logic by encoding the type of booleans with the formula 1 ⊕ 1, where ⊕ refers to the additive disjunction. We however avoid this notation as we do not consider the full additive connectives here.

More in general, the interpretation of a MLL formula F is a finite set F ι defined once we have fixed a valuation ι as a function mapping the propositional variables to finite sets. The definition of F ι is by induction on F , as follows:

X + ι = X -ι ::= ι(X), 1 ι = ⊥ ι ::= {⋆}, F ⊗ G ι = F `G ι ::= F ι × G ι .
It is easy to check that the usual isomorphisms of linear logic (like associativity and commutativity of the binary connectives) are validated by set isomorphisms. In particular, we can use tuples (x 1 , . . . , x n ) for denoting elements in the interpretation of a n-fold connective, e.g.

F 1 `(• • • `Fn ) ι ≃ {(x 1 , . . . , x n ) | ∀i ≤ n, x i ∈ F i ι }.
Weighted relational semantics equates much more than just linear logic isomorphisms, as for example F ι = F ⊥ ι for any formula F . More precisely, this semantics has the structure of a compact closed category. There are more refined examples of quantitative semantics which are not compact closed, e.g. probabilistic coherence spaces. Let us stress that our results do not suppose compact closeness.

The interpretation N ι of a proof-net N of conclusions Γ is a vector in R

`Γ ι ≥0
, which can be equivalently seen as a multidimensional matrix indexed by the tuples in `Γ ι . The interpretation can be given inductively as sketched by Figure 1c, once we have associated with

each box b of conclusions X - 1 , . . . , X - n , Y + a vector ι(b) ∈ R (`iX - i )`Y + ι ≥0
. This interpretation is invariant under the cut-reduction rules of Figure 1d `X+ 3 ). Notice that there is only one sequence of the generating rules of Figure 1b producing this proof-net: one first applies a par rule under the b 3 conclusions X - 2 and X + 3 , then a tensor between the resulting proof-net and b 2 , then a contraction between the two X - 1 conclusions and finally a cut between the conclusion of this contraction and b 1 . Figure 1c applied to this sequence of rules gives:

, i.e. N - → N ′ implies N = N ′ . ▶ Example 8. Consider the proof-net N ′ of conclusion X + 2 ⊗ (X - 2 `X+ 3 ) contained in the proof-net N depicted at left of
N ′ ι (x ′ ,(x ′′ ,x ′′ )) = y∈ X + 1 ι ι(b 1 ) y ι(b 2 ) (y,x ′ ) ι(b 3 ) (y,(x ′′ ,x ′′ )) .
3 This kind of denotational semantics are defined for countable sets S in general. Infinite sets are necessary to model linear logic exponential modality as well as the full λ-calculus. Since we focus here to only MLL, we can restrict to finite sets. . Notice also that the contraction imposes that the same index y is shared between the two different boxes (b 2 and b 3 ): contraction duplicates the indexes of the vectors, but it does not yield different copies of the vectors themselves. This is in accordance with Remarks 4 and 6: sharing of sampled values corresponds here to sharing vector indices, which is different from duplicating whole vectors. If we consider in fact the proof-net N ′′ ι given by a tensor between b 2 and b 3 and two distinct copies of b 1 , one cut with the X - 1 conclusion of b 2 and the other one with that of b 3 , then we would have:

N ′′ ι (x ′ ,(x ′′ ,x ′′ )) = y,y ′ ∈ X + 1 ι ι(b 1 ) y ι(b 2 ) (y ′ ,x ′ ) ι(b 1 ) y ′ ι(b 3 ) (y ′ ,(x ′′ ,x ′′ )) .
▶ Example 9. Let us consider a proof-net N which is a bunch of n + 1 axioms over a tree of n contractions, of which edges are labelled by X -, so that N has conclusions X -, X + , . . . , X + . The denotation N ι is then a vector indexed by the (n + 2)-tuples of elements in ι(X).

In fact, by using Figure 1c, one can check that N ι is a very sparse vector, having zero everywhere but on the tuples of equal elements, i.e. (x, x, . . . , x) for x ∈ ι(X), in which case N ι returns 1. We have here a first source of inefficiency of this kind of semantics, representing the denotation of a proof-net with a vector of dimension exponential in the number of its conclusions, where it would suffice a much more compact structure to store the same information. Section 5 will provide this structure with the notion of component factor.

If N has several cuts, the computation of N ι can be considerably simplified by using the following lemma, which is reminiscent of the notion of experiment introduced in [START_REF] Girard | Linear logic[END_REF].

▶ Lemma 10 (Cut bundles). Let Cut Γ (N ) be a proof-net of conclusions ∆ that can be decomposed into a proof-net N of conclusions ∆, Γ, Γ ⊥ and a bundle of cuts between the formulas in Γ and Γ ⊥ . Then, for every ⃗ d ∈ ∆ ι , we have:

Cut Γ (N ) ι ⃗ d = ⃗ c∈ Γ N ι ( ⃗ d,⃗ c,⃗ c) .
▶ Example 11. Let us compute the semantics of the proof-net N 0 in Figure 1e, by using Lemma 10 and Figure 1c. We have that, for any (x 4 , x 5 ) ∈ X + 4 ⊗ X + 5 ι :

N 0 ι (x4,x5) = xi∈ι(X + i ) for i ∈ {1, 2, 3} ι(b 1 ) x1 ι(b 2 ) (x1,x2) ι(b 3 ) (x1,x2,x3) ι(b 4 ) (x2,x3,x4) ι(b 5 ) (x2,x5)
With a bit more of effort (due to the presence of axioms) also N ι can be associated with the above summation. If we suppose that for every i, ι(X i ) = {t, f}, this summation has a total of 2 3 terms, so that computing the whole vector N 0 ι requires ∼ 2 5 basic operations4 , i.e. a quantity exponential in the number of the semantical boxes.

By carefully inspecting the summation, one can however realise that it can be refactored so to split factors over independent variables, getting for example the expression:

x3 x2 x1 ι(b 1 ) x1 ι(b 2 ) (x1,x2) ι(b 3 ) (x1,x2,x3) ι(b 4 ) (x2,x3,x4) ι(b 5 ) (x2,x5)
which, by memorising the intermediate sums, performs the same computation of N ι in just ∼ 2 3 operations.This kind of refactoring is at the core of many algorithms for exact inference in Bayesian graphs and the next sections will show how to import these methods. Factors

We adapt from Bayesian networks (e.g. [START_REF] Darwiche | Modeling and Reasoning with Bayesian Networks[END_REF]) the notion of factor (Definition 18) and of product and projection of factors. A factor carries both a vector and a "sharing structure" about what entries of this vector will be shared with possibly other factors so that we avoid the dimension explosion which is the source of inefficiency in Example 9. Bayesian networks use random variables for expressing such a "sharing structure", while we reduce this latter into the very basic definition of set-family, which encompasses the former (Example 15) and generalises to whole quantitative MLL. The terminology "factor" is standard in Bayesian networks, in fact this notion refers to the terms in the multiplication giving a joint distribution as the outcome of the variable elimination algorithm (Algorithm 1). We introduce also a notion of renaming (Definition 29) and of factor renaming (Definition 34) necessary to follow the compositional structure of MLL (see discussion in Example 41).

▶ Definition 12 (Set-family). We call set-family a finite, indexed family of finite sets, i.e. a map X from a finite set I(X) of indices to a set Sets(X) of finite sets. We denote by X(a) the set associated with index a ∈ I(X) in X. Meta-variables X, Y, Z will range over such set-families. Two families X and Y are compatible whenever for all a ∈ I(X) ∩ I(Y), X(a) = Y(a). Set-theoretical operations lift to compatible set-families by applying the former to the graph of these latter, e.g. the intersection X ∩ Y is the set-family defined by I(X ∩ Y) ::= I(X) ∩ I(Y) and (X ∩ Y)(a) ::= X(a) = Y(a) for every a ∈ I(X ∩ Y). Similarly, we will consider the union X ∪ Y and the set-theoretical difference X \ Y. In the same spirit, we write Y ⊆ X, for I(Y) ⊆ I(X) and for every a ∈ I(Y), Y(a) = X(a).

Given a set-family X, we denote by X the cartesian product a∈I(X) X(a) of the sets in Sets(X), where the same set in Sets(X) can appear multiple times in the product if associated with multiple indices. We denote the elements of X with the vectorial notation ⃗ x, to underline that it is an element in a cartesian product rather than in a simple set. ▶ Notation 13. Any element ⃗ x ∈ X can be seen as a collection (x a ) a∈I(X) of elements in Sets(X). In particular, given Y ⊆ X, we denote by ⃗ x| Y the projected element (x a ) a∈I(Y) ∈ Y . Similarly, given two set-families X, Y having disjoint sets of indexes, so clearly compatible, the elements of X ⊎ Y can be written as (⃗ x, ⃗ y), for ⃗ x ∈ X and ⃗ y ∈ Y .

Notice that if X is empty, then X is the singleton set {()}.

▶ Notation 14. Since finite, set-families can be given by enumerating their graph, like in X = {(a 1 , S 1 ), . . . , (a n , S n )}. In this case we have: I(X) = {a 1 , . . . , a n } and Sets(X) = {S 1 , . . . , S n }. In this latter set, the possible repetitions are equated, so Sets(X) might have less than n elements.

▶ Example 15.

A finite set {X 1 , . . . , X n } of finite random variables defines the set-family X = {(X 1 , X 1 ), . . . , (X n , X n )}, where X i denotes the finite set of the possible outcomes taken by the random variable X i . Notice that X is then the set of samples of the joint distribution over X 1 , . . . , X n . To be more explicit, suppose that each random variable X i is boolean, i.e. X i = {t, f} for all i ≤ n, then Sets(X) = {{t, f}}, while

X = {(b 1 , . . . , b n ) | b i ∈ {t, f}}.
▶ Example 16. Consider a sequent Γ = X • 1 , . . . , X • n of atomic formulas. A natural set-family that can be associated with Γ and a valuation ι, has indices the sequent positions {1, . . . , n} and it maps a position i to the set ι(X i ). This set-family however is not the only possible one: for example, one may take as indices the propositional variables X 1 , . . . , X n , where F S C D 2 0 2 3 multiple occurrences of the same variable are equated, and map X i to ι(X i ). The two set-families are quite different if Γ contains repetitions. Namely, let Γ = X + , X, + X -, Y -, with X = Y = {t, f}. The two set-families are: ▶ Remark 17. Notice that Z, Y ⊆ X implies that both Z and Y are compatible. Henceforth we will always consider families which are subset of a fixed "universal" family (underlined by a proof-net), so that the compatibility condition in Definition 12 is not an issue and hence will be often not mentioned.

X = {(1, {t, f}),
▶ Definition 18 (Factor). A generalised factor, or simply factor, ϕ is a pair (Fam(ϕ), Fun(ϕ)) of a set-family Fam(ϕ) and a function Fun(ϕ) from the set Fam(ϕ) to R ≥0 . We will short the notation Fun(ϕ) by writing just ϕ when it is clear from the context that we are considering the function associated with a factor and not the whole pair (Fam(ϕ), Fun(ϕ)). We often consider Fun(ϕ) as a vector indexed by the elements of its domain, so that ϕ ⃗ x stands Fun(ϕ)(⃗ x), for every ⃗ x ∈ Fam(ϕ) .

{(t X , t Y ) → 0.2, (t X , f Y ) → 0.25, (f X , t Y ) → 0.25, (f X , f Y ) → 0.3}. The pair ϕ = (Y, Fun(ϕ)
) is an example of factor. Intuitively, ϕ can be seen as the presentation 0.2e

(t X ,t Y ) + 0.25e (t X ,f Y ) + 0.25e (f X ,t Y ) + 0.3e (f X ,f Y ) of a vector in R 4 ≥0 with respect to a set of basis vectors e (b X ,b Y ) associated with the elements in (b X , b Y ) ∈ Y .
▶ Definition 20 (Factor projection). Let ϕ be a factor and let X be a set-family compatible with Fam(ϕ), the projection of ϕ to X is the factor π X (ϕ) defined by:

Fam(π X (ϕ)) ::= X, π X (ϕ) ⃗ x ::= ⃗ y∈ Fam(ϕ)\X ϕ (⃗ x| Fam(ϕ) ,⃗ y) , for ⃗ x ∈ X .
▶ Example 21. Recall the set-family Y and the factor Fun(ϕ) given in Example 19, let

X = {(X, {t, f})} ⊆ Y. We have that π X (ϕ) = {t X → 0.45, f X → 0.55}. Let now Z = X ⊎ {(Z, {t, f})}, we have that π Z (ϕ) = {(t X , t Z ) → 0.45, (t X , f Z ) → 0.45, (f X , t Z ) → 0.55, (f X , f Z ) → 0.55}.
Notice in particular that the factor projection to a set-family Z does not preserve in general the property of being a probability mass function, unless Z ⊆ Fam(ϕ).

▶ Remark 22. With the notations of Definition 20, if X ⊆ Fam(ϕ), then π X (ϕ) corresponds to what is called in Bayesian programming summing out Fam(ϕ) \ X, which gives the marginal distribution over X. Suppose on the contrary that X and Fam(ϕ) are disjoint, then for every ⃗ x ∈ X , π X (ϕ) ⃗ x is the total mass of ϕ, i.e. ⃗ y∈ Fam(ϕ) ϕ ⃗ y .

▶ Remark 23. Suppose that Fam(ϕ) has n indices and that k is the maximum cardinality of a set in Sets(Fam(ϕ)), then the computation of the whole vector π

X (ϕ) is in O(k n ).
▶ Definition 24 (Binary factor product). Given two factors ϕ and ψ, such that Fam(ϕ) and Fam(ψ) are compatible, we define their factor product as the factor ϕ ⊙ ψ given by:

Fam(ϕ ⊙ ψ) ::= Fam(ϕ) ∪ Fam(ψ), (ϕ ⊙ ψ) ⃗ z ::= ϕ ⃗ z| Fam(ϕ) ψ ⃗ z| Fam(ψ) , for ⃗ z ∈ Fam(ϕ ⊙ ψ) .
▶ Remark 25. If Fam(ϕ) ∪ Fam(ψ) has n indices and k is the maximum cardinality of a set in Sets(Fam(ϕ) ∪ Fam(ψ)), then the computation of the whole vector

ϕ ⊙ ψ is in O(k n ).
▶ Example 26. In terms of MLL operations, factor products correspond to a ⊗ product plus a bunch of contractions on the common indexes. For example, let us take as indexes the propositional variables and as sets just {t, f} (recall Example 16) and consider Fam(ϕ) = {X 2 , X 3 , X 4 } and Fam(ψ) = {X 2 , X 5 } (this choice is reminiscent of the variables in the proof-nets in Figure 1e, in fact ϕ and ψ can be associated with the boxes, respectively, b 4 and b 5 ). Then, Fun(ϕ ⊙ ψ) is over {X 2 , X 3 , X 4 , X 5 }, so of dimension 2 4 , while Fun(ϕ) ⊗ Fun(ψ) is a vector indexed by tuples of 5 booleans, so of dimension 2 5 .

The next proposition states expected properties of factor projection and product that are fundamental in the sequel.

▶ Proposition 27. Factor product is associative and commutative, with neutral element the empty factor (∅, 1). Moreover:

1. π X∪Z (π X∪Y (ϕ)) = π X∪Z (ϕ), whenever Y ⊆ Fam(ϕ) and Z ∩ Fam(ϕ) = ∅; 2. π X (ϕ ⊙ ψ) = π X (ϕ) ⊙ ψ, whenever Fam(ψ) ⊆ X.
▶ Definition 28 (n-factor product). Let I be a finite set. Given a collection of pairwise compatible factors (ϕ i ) i∈I , we define their factor product as the factor i∈I ϕ i ::= ϕ i1 ⊙ • • • ⊙ ϕ in , for some enumeration of I. This is well-defined independently from the chosen enumeration because of Proposition 27.

Section 5 will associate factors to MLL proof-nets and in order to make this association compositional (Theorem 48) we introduce the following notion of renaming, as the contraction and cut rules of Figure 1b may change the sharing structure associated with a proof-net.

▶ Definition 29 (Renaming). A renaming f from a set-family X to a set-family Y is a map from I(X) to I(Y) such that for all a ∈ I(X), we have X(a) = Y(f (a)). Any such renaming f induces the map f • from Y to X by:

for ⃗ y ∈ Y , f • (⃗ y) ::= (y f (a) ) a∈I(X) ∈ X . ( 2
)
Moreover, we say that a point ⃗ x ∈ X agrees on f whenever, for every a, a ′ ∈ I(X),

f (a) = f (a ′ ) implies that x a = x a ′ .
▶ Remark 30. The notion of "agreeing on a renaming f " generalises the notion in Bayesian programming of a set of samples that "agrees on the same random variables" as used in e.g. [START_REF] Darwiche | Modeling and Reasoning with Bayesian Networks[END_REF].

▶ Notation 31. Given a renaming f from X to Y, and a set-family X ′ ⊆ X, we denote by f (X ′ ) the set-family having as indices the set f (I(X ′ )) ⊆ I(Y) and that it associates with

any b ∈ f (I(X ′ )) the set Y(b). Notice that f (X ′ ) ⊆ Y.
▶ Proposition 32. Given a renaming from X to Y, the image set of f • is the subset of X of the elements which agree on f . If, moreover, f is surjective over

I(Y), then f • is an injective map from Y to X , hence a bijection from Y to {⃗ x ∈ X | ⃗ x agrees on f }.
In this case, we denote its inversion by f • .

▶ Example 33. Recall the set-families X and Y in Example 16, associated with the sequent Γ = X + , X, + X -, Y -. Let us consider the following two specific renamings from X to Y:

f = 1, 2, 3 → X 4 → Y , g = 1, 2, 3, 4 → X .
F S C D 2 0 2 3

8:12

Sum-Product for MLL and take for example ⃗ y = (t X , f Y ) ∈ Y . We have (we use the natural order (1,2,3,4) to represent elements in X ):

f • (⃗ y) = (t, t, t, f), g • (⃗ y) = (t, t, t, t).
Notice in fact that f • (⃗ y) agrees on f but not on g, while g • (⃗ y) agrees on both f and g. Also notice that f is surjective and in fact f • is an injection, while g is not surjective and in fact g • is not a injection, for example:

g • (t X , f Y ) = g • (t X , t Y ).
▶ Definition 34 (Factor renaming). Let f be a renaming from Fam(ϕ) to a set-family X. The renaming of ϕ along f is the factor f (ϕ) defined by:

Fam(f (ϕ)) ::= f (Fam(ϕ)), f (ϕ) ⃗ x ::= ϕ f ⋆ (⃗ x) , for ⃗ x ∈ f (Fam(ϕ)) .
▶ Example 35. Recall the renaming f of Example 33 between the set-families X and Y given in Example 16. Consider the factor ϕ over X defined by ϕ (b1,b2,b3,b4

) ::= 1 if b 1 = b 2 = b 3 , 0
otherwise. This factor corresponds to the interpretation of the proof-net having a weakening producing Y -and the axiom on top of a contraction giving X + , X + , X -. Then f (ϕ) is over Y and its map is the constant function giving 1.

▶ Remark 36. Notice that one can formalise the notions of this section in a categorical way, considering a category of renamings as morphisms between set-families. We did not develop this more abstract presentation as not needed in the sequel.

Weighted Semantics by Factors, Atomic Case

We apply to MLL the notions introduced in Section 4. It is convenient to restrict to atomic proof-nets and then to extend the results to the non-atomic case in Section 6. Definitions 37 and 45 associate two different set-families with an atomic proof-net N , the edge and the component set-families. The edge set-family permits to consider the standard weighted interpretation N as a factor (Definition 39), while the component set-family yields a more compressed representation of N , the component factor (Definition 40), which has a form of compositionality (Theorem 48) and hence can be computed directly (Theorem 49) without using the rules of Figure 1c. Henceforth, this section fixes a valuation ι and considers only atomic proof-nets. We recall that an atomic proof-net can contain only axioms, cuts, weakening, contractions and semantical boxes.

▶ Definition 37 (Edge set-family). Let N be an atomic proof-net and ι be a valuation. The edge set-family of N , written by Fam ι e (N ), has the edges of N as indices and associates with an edge e : X • the set ι(X). Given a sequence Γ of edges e 1 : X • 1 , . . . , e n : X • n , we extend the metavariable Γ to denote also the edge set-family {(e 1 , ι(X 1 )), . . . , (e n , ι(X n ))} ⊆ Fam ι e (N ).

▶ Remark 38. Let Γ be e 1 : X • 1 , . . . , e n : X • n . The convention of denoting by Γ both the underlined sequent X • 1 , . . . , X • n and the edge set-family {(e 1 , ι(X 1 )), . . . , (e n , ι(X n ))} is coherent because the cartesian product Γ associated with the edge set-family is the same set as the weighted denotation Γ ι , this latter also denoted simply by Γ . This ease of notation is necessary to avoid a formalism overkill.

▶ Definition 39. Given a valuation ι, the edge factor of an atomic proof-net N has as set-family the edge-set family induced by the conclusions of N and as function the weighted interpretation N ι . We take the liberty to denote this edge factor also by N ι .

▶ Definition 40 (Component set-family and renaming). Let N ¬b denote the graph obtained from an atomic proof-net N by removing all its semantical boxes, so keeping their conclusions as pending edges of the graph. Given an undirected connected component M of N ¬b , one can remark that all edges of M are atomic formulas over a unique variable, let us denote it X M . The component set-family of N , written Fam ι c (N ), has as indices the undirected connected components of N ¬b and associates with a component M the set ι(X M ). The component renaming of N , written ℓ N , is the renaming from Fam ι e (N ) to Fam ι c (N ) mapping the edges of N to the connected component of N ¬b they belong to.

▶ Example 41. Consider the atomic proof-net N a obtained from the proof-net N 0 in Figure 1e by removing the tensor node, so that N a has conclusions X + 4 , X + 5 . Notice that N a ¬b has five connected components which correspond to the five propositional variables X 1 , . . . , X 5 .

If however we consider the sub proof-net N ′ a obtained from N a by removing the cut and the contraction insisting on the edges typed by, e.g., X - 1 , we have that N ′ a ¬b has now seven connected components, in particular three of them supports the same variable X 1 . This example shows that the generating rules of MLL (Figure 1b) require not to mix up the component set-family with the variables labelling the edges (see also Remark 55).

▶ Remark 42. The ℓ N information can be memorised once and for all by adding a further labelling over the edges of N giving the same index to the edges belonging to the same connected component of N ¬b . This labelling can be computed in linear time with respect to the size of N , by adapting one of the many connected component algorithms.

▶ Notation 43. Let Γ = e 1 : X • 1 , . . . , e n : X • n be a set of edges of N , so that Γ is also the set-family {(e 1 , ι(X 1 )), . . . , (e n , ι(X n ))} contained in Fam ι e (N ). By Notation 31, the writing ℓ N (Γ) denotes the set-family {(ℓ N (e 1 ), ι(X 1 )), . . . , (ℓ N (e n ), ι(X n ))} ⊆ Fam ι c (N ). Notice that ℓ N is surjective on I(ℓ N (Γ)), so we can apply Proposition 32, getting the two maps:

ℓ • N from ℓ N (Γ) to Γ , its inverse ℓ • N from { ⃗ d ∈ Γ | ⃗ d agrees on ℓ N } to ℓ N (Γ) .
▶ Remark 44. In general, given a set of edges Γ of an atomic proof-net N , we have that: ℓ N (Γ) = Γ if, and only if, all edges in Γ belong to pairwise different connected components of N ¬b . Moreover, if ℓ N (Γ) = Γ , then every ⃗ d ∈ Γ agrees on ℓ N .

▶ Definition 45. Given a valuation ι, the component factor of an atomic proof-net N is the renaming ℓ N ( N ι ) of its edge factor, i.e. if ∆ are the conclusions of N , Fam(ℓ

N ( N ι )) = ℓ N (∆) and for ⃗ d ∈ ℓ N (∆) , Fun(ℓ N ( N ι ) ⃗ d = N ι ℓ • N ( ⃗ d) .
▶ Example 46. Recall the proof-net N and the valuation ι of Example 9. Notice that Fam(ℓ N ( N ι )) is a singleton as the n + 2 conclusions of N belong to the same component, and Fun(ℓ N ( N ι )) = (1 t , 1 f ), which is a more parsimonious object than N ι , this latter of dimension exponential in n.

Proposition 47 details how to recover the original denotation of N out of its component factor.

▶ Proposition 47. Let N be an atomic proof-net of conclusions ∆. For every ⃗ d ∈ ∆ , we have that:

N ι ⃗ d = ℓ N ( N ι ) ℓ • N ( ⃗ d)
if ⃗ d agrees on ℓ N , 0 otherwise.

(

F S C D 2 0 2 3 8:14

Sum-Product for MLL

The following is the core theorem of this paper: MLL cuts correspond to a factor product plus a projection.

▶ Theorem 48. Let N = Cut Γ (N ′ , N ′′ ) be an atomic proof-net of conclusions ∆ obtained by connecting by a bunch of cuts over a sequent Γ a sub proof-net N ′ , of conclusions Γ, ∆ ′ , and N ′′ , of conclusions Γ ⊥ , ∆ ′′ , so that ∆ = ∆ ′ , ∆ ′′ . We have:

ℓ N ( N ι ) = π ℓ N (∆) (ℓ N ( N ′ ι ) ⊙ ℓ N ( N ′′ ι )) (4)
As a consequence, we can compute the component factor of N without passing via N ι :

▶ Theorem 49. Let N be an atomic proof-net with conclusions ∆. We have:

ℓ N ( N ι ) = π ℓ N (∆) ( b∈b(N ) ℓ N (ι(b))).
▶ Example 50. Consider an atomic proof-net N of conclusions ∆ such that no edge in ∆ is connected in N ¬b with a conclusion of a box of N . By Remark 22, π ℓ N (∆) ( b∈b(N ) ι(b)) is the constant function giving the total mass of the vectors associated with the boxes of N .

Consider the atomic proof-net N a obtained by removing the tensor node from the proof-net N 0 of Figure 1e. If we apply Theorem 49 to N a , we will obtain exactly the same summation given in Example 11, in fact the edge and component set-families of the conclusions of N a are the same. However, we have now the correct formalism to apply exact inference algorithms to refactor the expression π ℓ N (∆) ( b∈b(N ) ℓ N (ι(b))), by taking advantage of the distributivity law of factor product over the projection (Proposition 27). We adapt here one among the simplest such algorithms, called the sum-product variable elimination algorithm, first introduced in [START_REF] Zhang | A simple approach to bayesian network computations[END_REF], see [START_REF] Darwiche | Modeling and Reasoning with Bayesian Networks[END_REF] as a reference. The terminology "variable elimination" is because this procedure infers from a Bayesian network the marginal distribution of a random variable X out of a family5 X of variables containing X, by "eliminating" all the other variables in X. In our case, what we "eliminate" are the N ¬b components of the conclusions of the box factors containing no conclusion of the proof-net.

Algorithm 1 MLL Sum-Product Algorithm.

input:

1: N ▷ an atomic proof-net of conclusions ∆ 2: ι ▷ a valuation map 3: ω ▷ A linear order on the components in Fam ι c (N ) not having a conclusion in ∆ output: the factor ℓ

N ( N ι ) 4: F ← {ℓ N (ι(b)) | b ∈ b(N )} ▷ Factors of b(N ) 5: for C in ω do 6: F c ← {ϕ ∈ F | C ∈ I(Fam(ϕ))} 7: ψ ← ϕ∈Fc ϕ ▷ Product 8: ρ ← π Fam(ψ)\{C} (ψ) ▷ Sum-out 9: F ← {ρ} ∪ (F \ F c ) return ϕ∈F ϕ
Algorithm 1 is our adaptation of the sum-product algorithm. Given a linear order ω over the connected components of N ¬b which contains no conclusion of N , the algorithm proceeds as follows: line 4 initialises a variable F with the set of factors to compute; line 5 takes from ω the next connected component C to process; line 6 gathers in a variable F c all factors in F which have C as an index (i.e. a conclusion in C); line 7 computes the product of these factors and line 8 projects it on the components different from C (a.k.a. summing out C); line 9 updates F by replacing the processed factors with the result of this projection and then it jumps back to line 5. At the end of this loop, F contains a set of factors indexed over the components of N ¬b connected with the conclusions in N and then it returns their product.

Soundness follows from Proposition 27 and Theorem 49: The components to eliminate are 1, 2, 3. By taking the order ω = 1 < 2 < 3, Algorithm 1 will calculate the following intermediate factors: In general, Algorithm 1 is in O(nk w ), where n is the length of ω (i.e. the number of components to eliminate), k is the maximal cardinality of a set interpreting an atomic variable (in our examples we always suppose k = 2, for the two booleans) and w is the maximal cardinality of Fam(ϕ), for ϕ a factor created/used by the algorithm (this parameter depends on the chosen order ω).

▶ Theorem 51. Algorithm 1 returns ℓ N ( N ι ) if
ρ 1 = π {2,3} (ι(b 1 ) ⊙ ι(b 2 ) ⊙ ι(b 3 )), ρ 2 = π {2,4} (ρ 1 ⊙ ι(b 4 )), ρ 3 = π {4,5} (ρ 2 ⊙ ι(b 5 )),
The quest for optimal orders is a major topic in Bayesian networks, which is however known to be a NP-hard problem [START_REF] Cooper | The computational complexity of probabilistic inference using bayesian belief networks[END_REF]. Since probabilistic MLL contain Bayesian networks, we should focus on heuristics that yield good performances in most cases.

▶ Remark 54. Recall the proof-net N in Figure 1e which cut reduces to N 0 . Notice that this proof-net does not resemble to a Bayesian network, e.g. it alternates par and tensor nodes. However, the reader may recognise the intermediate factors ρ 1 , ρ 2 and ρ 3 computed by Algorithm 1 in Example 52 as the nested sub proof-nets of N of conclusions, respectively, X + 2 ⊗ (X - 2 `X+ 3 ), X + 2 ⊗ X + 4 and X + 4 ⊗ X + 5 . This is far from being a coincidence, as any run of Algorithm 1 can in fact be associated with a MLL proof-net, although this latter might need formulas with an arbitrary number of alternations between tensors and pars. We will investigate this point in a forthcoming paper. Sum-Product for MLL If (⋆) holds (e.g. as for the proof-net N a discussed in Example 52), then ℓ N is equivalent to the renaming from the edge set-family to the variable set-family, an instance being given by the renaming f mentioned in Example 33. Such a shortcut is however misleading in our setting, as the rules generating MLL proof-nets (Figure 1b) are more "granular" than the ones for Bayesian networks, in particular (⋆) is not preserved by the c(N X -,X -) rule (Example 41). A better alternative would be to introduce "term" variables, like the variables of simply typed λ-calculus, decorating edges.

6

The General Case

The results of the previous section can be extended to non-atomic proof-nets by using MLL cut-reduction. We just sketch here the main ideas, giving the details in the appendix. The reader can recall the proof-net N in Figure 1e to follow the reasoning with an example. Given a MLL proof-net N of conclusion ∆: (i) reduce N to its normal form N 0 by using the cut-reduction rules of Figure 1d. (ii) Decompose N 0 into the syntax forest F ∆ of its conclusions and the atomic sub proof-net N a of conclusions the atomic formulas At(∆) appearing in ∆, which are the leaves of F ∆ . Notice that there is a bijection between ∆ and At(∆) , relating an element in ⃗ d ∈ ∆ with a tuple At( ⃗ d) ∈ At(∆) enumerating the atomic components of ⃗ d. (iii) Apply Algorithm 1 in order to compute ℓ N ( N ). We have:

▶ Corollary 56. Let N be a proof-net with conclusions ∆, and let N 0 be the normal form of N and (F ∆ , N a ) be the decomposition of N 0 described above. For every ⃗ d ∈ ∆ , we have:

N ι ⃗ d = ℓ N ( N a ) ℓ • Na (At( ⃗ d)) , (5)
if At( ⃗ d) agrees on ℓ Na , otherwise N ι ⃗ d = 0. The cut-reduction in step (i) is linear in the size of N 0 as MLL cut-reduction shrinks the size of a proof-net. Also the construction of N a out of N 0 , and the read of ℓ • Na (At( ⃗ d)) out of ⃗ d ∈ ∆ are linear. So all the complexity of this procedure is the calculation of ℓ N ( N a ) which has been discussed in the previous section.

Conclusion and Perspectives

We considered weighted relational semantics just as an instance of quantitative semantics, but these techniques can be applied verbatim to other web-based semantics, such as probabilistic coherence spaces [START_REF] Danos | Probabilistic coherence spaces as a model of higher-order probabilistic computation[END_REF] or finiteness or Köthe sequence spaces [START_REF] Ehrhard | Finiteness spaces[END_REF][START_REF] Ehrhard | On Köthe sequence spaces and linear logic[END_REF]. One can wonder whether our results extend to richer linear logic fragments. The additive connectives ⊕ and & can be reasonably added to the picture. In fact, by adopting some form of additive boxes [START_REF] Tortora De Falco | The additive mutilboxes[END_REF], one can revisit the sum-product algorithm as a refactorization of a proof-net modulo commutative additive cuts. The exponential modalities (so encompassing full simply typed probabilistic λ-calculus) are more challenging as they require infinite sets at the semantical level. This will deserve future investigation. Related to the above point is the correspondence alluded to in Remark 54. We will detail in a future work how to map any run ρ of the sum-product algorithm on an atomic proof-net N 0 into a non-atomic proof-net N ρ , which rewrites into N 0 and such that the intermediate factors appearing in ρ correspond to sub-proof-nets of N ρ .

As mentioned by Remark 53, the performance of many exact inference algorithms, such as sum-product, depends on the order of the components to eliminate and the problem of finding optimal orders is known to be NP-hard [START_REF] Cooper | The computational complexity of probabilistic inference using bayesian belief networks[END_REF]. Many heuristics have been given based on the graph-theoretical structure of Bayesian nets. One can wonder whether the additional proof-theoretical structure (e.g. switching paths, empires [START_REF] Girard | Linear logic[END_REF]) can suggest new heuristics.

( a )

 a Labelling of MLL nodes with their incident edges. Edges are oriented top-down.

  Figure 1e and characterised by the three boxes b 1 , b 2 , b 3 and the tensor and par above the cut over X + 2 ⊗ (X - 2

F S C D 2 0 2 3 8: 8 Sum-

 38 Product for MLLNotice that the cut composes the semantics of b 1 with that of the proof-net containing b 2 and b 3 , producing the sum over y ∈ X + 1 ι

( 2 ,

 2 {t, f}), (3, {t, f}), (4, {t, f})}, Y = {(X, {t, f}), (Y, {t, f})}.

▶ Example 19 .

 19 Let us recall the set-family Y = {(X, {t, f}), (Y, {t, f})} of Example 16, and consider the function Fun(ϕ) given by

▶F

  Remark 55. The component renaming ℓ N is omitted in the setting of Bayesian networks as encoded in the formula labelling, by imposing the following type constraint: (⋆) any two edges of N which are supported by the same propositional variable lay in the same connected component of N ¬b .

  fed with an atomic proof-net N , a valuation ι and a linear order on the components in Fam ι c (N ) not containing any conclusion of N . ▶ Example 52. Consider the atomic proof-net N a obtained by removing the tensor node from the proof-net N 0 of Figure 1e (Example 1) and use the numbers 1, 2, 3, 4, 5 to denote the five connected components of N a ¬b such that component i is supported by variable X i .

  the output being ρ 3 . This yields exactly the factored equation in Example 11 and it allows to calculate the whole semantics of N a in O(k 3 ) basic operations, if k is the maximal cardinality of the sets associated with the propositional variables appearing in the proof-net.

▶ Remark 53. A run of Algorithm 1 depends on the chosen order ω. Different orders yield different factorisations and have different performances. For example, by taking the inverse order 3 < 2 < 1 in Example 52 we get a run in O(k 4 ), which is an order of magnitude slower than 1 < 2 < 3, although yet more efficient than the immediate recursive algorithm induced by the standard semantics (Example 11).

It is known that the space of random variables ranging over a finite set of outcomes of cardinality n can be described by the finite additive disjunction i≤n 1 of the tensor unit, see e.g.[START_REF] Ehrhard | Probabilistic call by push value[END_REF]. This formula is not in MLL, as ⊕ is not a multiplicative connective, but it appears in our setting as these spaces of finite random variables are associated with the positive atomic formulas of MLL (seeExample 7).

More formally, a directed graph is a quadruplet (V, E, t, s) of a set V of vertices and a set E of edges, and two maps t, s : E → V associating an edge with a target and a source, respectively. We alllow directed graphs with pending edges, i.e. t and s may be partial partial. The edges not in the domain of t or s are called pending. A directed graph is acyclic (a DAG for short), if there is no directed cycle.F S C D 2 0 2

We are supposing that multiplication, addition and coefficient access are operations of constant cost.

Any resemblance to the notations in Section 4 is purely voluntary.

Funding This work was partially supported by ANR PRC project PPS ANR-19-CE48-0014.