Quantum Bayesian networks [Henson et al., 2014] 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 [Pearl, 2009] - 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.

Abstract Variable Elimination ( $$\textsf{VE}$$ VE ) is a classical exact inference algorithm for probabilistic graphical models such as Bayesian Networks, computing the marginal distribution of a subset of the random variables in the model. Our goal is to understand Variable Elimination as an algorithm acting on programs in an idealized probabilistic functional language—a linear simply-typed $$\lambda $$ λ -calculus suffices for our purpose. Precisely, we express $$\textsf{VE}$$ VE as a term rewriting process, which transforms a global definition of a variable into a local definition, by swapping and nesting let-in expressions. We exploit in an essential way linear types.

This paper investigates the denotational invariants of non-wellfounded and circular proofs of linear logic with least and greatest fixed points, μLL, by providing a categorical semantics. More precisely the paper successively introduces semantics for (i) non-wellfounded pre-proofs, be they valid or not, (ii) valid pre-proofs exploiting their validity condition by considering an orthogonality construction on the given categorical model and finally (iii) circular strongly valid pre-proofs, exploiting both validity and regularity in order to define inductively the interpretation. Then the paper investigates the semantical content of the translation from finitary proofs to non-wellfounded proofs and, conversely, from (strongly valid) circular proofs to finitary proofs, showing that both translations preserve the interpretation.

Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates "continuous data types" such as the real line. So far however, they lacked a major feature to make them a model of more general probabilistic programming languages (notably call-by-value and call-by-push-value languages): a theory of integration for functions whose codomain is a cone, which is the key ingredient for interpreting the sampling programming primitives. The goal of this paper is to develop such a theory: our definition of integrals is an adaptation to cones of Pettis integrals in topological vector spaces. We prove that such integrable cones, with integral-preserving linear maps as morphisms, form a model of Linear Logic for which we develop two exponential comonads: the first based on a notion of stable and measurable functions introduced in earlier work and the second based on a new notion of integrable analytic function on cones.

Abstract We extend the recently introduced setting of coherent differentiation by taking into account not only differentiation but also Taylor expansion in categories which are not necessarily (left) additive. The main idea consists in extending summability into an infinitary functor which intuitively maps any object to the object of its countable summable families. This functor is endowed with a canonical structure of a bimonad. In a linear logical categorical setting, Taylor expansion is then axiomatized as a distributive law between this summability functor and the resource comonad (aka. exponential). This distributive law allows to extend the summability functor into a bimonad on the coKleisli category of the resource comonad: this extended functor computes the Taylor expansion of the (nonlinear) morphisms of the coKleisli category. We also show how this categorical axiomatization of Taylor expansion can be generalized to arbitrary cartesian categories, leading to a general theory of Taylor expansion formally similar to that of cartesian differential categories, although it does not require the underlying cartesian category to be left additive. We provide several examples of concrete categories that arise in denotational semantics and feature such analytic structures.

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.

We extend to general cartesian categories the idea of Coherent Differentiation recently introduced by Ehrhard in the setting of categorical models of Linear Logic. The first ingredient is a summability structure which induces a partial left-additive structure on the category. Additional functoriality and naturality assumptions on this summability structure implement a differential calculus which can also be presented in a formalism close to Blute, Cockett and Seely’s cartesian differential categories. We show that a simple term language equipped with a natural notion of differentiation can easily be interpreted in such a category.

The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite non-determinism and indeed these languages are essentially non-deterministic. In a previous paper we introduced a categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces. Based on this semantics we develop a syntax of a deterministic version of the differential lambda-calculus. One nice feature of this new approach to differentiation is that it is compatible with general fixpoints of terms, so our language is actually a differential extension of PCF for which we provide a fully deterministic operational semantics.

Abstract The categorical models of differential linear logic (LL) are additive categories and those of the differential lambda-calculus are left-additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential LL are concerned, these models feature finite nondeterminism and indeed these languages are essentially non-deterministic. We introduce a categorical framework for differentiation which does not require additivity and is compatible with deterministic models such as coherence spaces and probabilistic models such as probabilistic coherence spaces.

In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.

We develop a categorical semantics of μLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baelde's propositional μMALL with exponentials. Our general categorical setting is based on Seely categories and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of sets and relations, least and greatest fixed points are interpreted in the same way. In the second one, based on a category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving it, least and greatest fixed points have distinct interpretations. This latter model shows that μLL enjoys a denotational form of normalization of proofs.

For overcoming the limitations of probabilistic coherence spaces which do not seem to provide natural interpretations of continuous data types such as the real line, we introduced with Pagani and Tasson a model of probabilistic higher order computation based on (positive) cones, and a class of totally monotone functions that we called "stable". Then Crubillé proved that this model is a conservative extension of the earlier probabilistic coherence space model. We continue these investigations by showing that the category of cones and linear and Scott-continuous functions is a model of intuitionistic linear logic. To define the tensor product, we use the special adjoint functor theorem, and we prove that this operation is an extension of the standard tensor product of probabilistic coherence spaces. We also show that these latter are dense in cones, thus allowing to lift the main properties of the tensor product of probabilistic coherence spaces to general cones. Finally we define in the same way an exponential of cones and extend measurability to these new operations.

We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flipping coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotational model of probabilistic coherence spaces, a categorical model of full classical Linear Logic, interpreting data types as coalgebras for the resource comonad. We prove adequacy and full abstraction, generalizing earlier results to a much more realistic and powerful programming language.

We present a probabilistic version of PCF, a well-known simply typed universal functional language. The type hierarchy is based on a single ground type of natural numbers. Even if the language is globally call-by-name, we allow a call-by-value evaluation for ground-type arguments to provide the language with a suitable algorithmic expressiveness. We describe a denotational semantics based on probabilistic coherence spaces, a model of classical Linear Logic developed in previous works. We prove an adequacy and an equational full abstraction theorem showing that equality in the model coincides with a natural notion of observational equivalence.

Differential linear logic enriches linear logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for differential linear logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last, we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.

We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations.

We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of Call-By-Push-Value, subsumes both Call-By-Name and Call-By-Value lambda-calculi, factorizing the Girard's translations of these calculi in Linear Logic. We build a denotational model of the Bang Calculus based on the relational interpretation of Linear Logic and prove an adequacy theorem by means of a resource Bang Calculus whose design is based on Differential Linear Logic.

Probabilistic coherence spaces (PCoh) yield a semantics of higher-order probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in Pcoh characterizes the operational indistinguishability of programs in PCF with a random primitive.

We study the probabilistic coherent spaces - a denotational semantics interpreting programs by power series with non negative real coefficients. We prove that this semantics is adequate for a probabilistic extension of the untyped λ-calculus: the probability that a term reduces to ahead normal form is equal to its denotation computed on a suitable set of values. The result gives, in a probabilistic setting, a quantitative refinement to the adequacy of Scott's model for untyped λ-calculus.

We study the Taylor expansion of lambda-terms in a on-deterministic or algebraic setting, where terms can be added. The target language is a resource lambda calculus based on a differential lambda-calculus that we introduced recently. This operation is not possible in the general untyped case where reduction can produce unbounded coefficients. We endow resource terms with a finiteness structure (in the sense of our earlier work on finiteness spaces) and show that the Taylor expansions of terms typeable in Girard's system F are finitary by a reducibility method.

We investigate a new denotational model of linear logic based on the purely relational model. In this semantics, webs are equipped with a notion of ‘finitary’ subsets satisfying a closure condition and proofs are interpreted as finitary sets. In spite of a formal similarity, this model is quite different from the usual models of linear logic (coherence semantics, hypercoherence semantics, the various existing game semantics…). In particular, the standard fix-point operators used for defining the general recursive functions are not finitary, although the primitive recursion operators are. This model can be considered as a discrete analogue of the Köthe space semantics introduced in a previous paper: we show how, given a field, each finiteness space gives rise to a vector space endowed with a linear topology, a notion introduced by Lefschetz in 1942, and we study the corresponding model where morphisms are linear continuous maps (a version of Girard's quantitative semantics with coefficients in the field). In this way we obtain a new model of the recently introduced differential lambda-calculus.

Abstract. In a previous work with Antonio Bucciarelli, we introduced indexed linear logic as a tool for studying and enlarging the denotational semantics of linear logic. In particular, we showed how to define new denotational models of linear logic using symmetric product phase models (truth-value models) of indexed linear logic. We present here a strict extension of indexed linear logic for which symmetric product phase spaces provide a complete semantics. We study the connection between this new system and indexed linear logic.

We present a category of locally convex topological vector spaces that is a model of propositional classical linear logic and is based on the standard concept of Köthe sequence spaces. In this setting, the ‘of course’ connective of linear logic has a quite simple structure of a commutative Hopf algebra. The co-Kleisli category of this linear category is a cartesian closed category of entire mappings. This work provides a simple setting in which typed λ-calculus and differential calculus can be combined; we give a few examples of computations.

A general category of games is constructed. A subcategory of saturated strategies, closed under all possible codings in copy games, is shown to model reduction in classical linear logic.

Proposes a definition (by reducibility) of sequentiality for the interpretations of higher-order programs and proves the equivalence between this notion and strong stability.>

It is shown that Kahn-Plotkin sequentiality can be expressed by a preservation property similar to stability and that this kind of generalized stability can be extended to higher order. The main result is the construction of a model where all morphisms are functions and, at ground types, these functions are sequential.>

An abstract framework is proposed for the description of the type dependency semantics. It is claimed that the notion of fibration introduced by A. Grothendieck in the 1960s is perfectly adapted to this goal and provides the greatest simplicity and generality. This semantics is extended to higher order, and an explanation is given of what a general definition for the semantics of the theory of constructions could be.>