Searcharxiv⌕ Search

arXiv subjects

Claudia Faggian

Publications and source records attributed to Claudia Faggian.

At least 19 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

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

A Rewriting Theory for Quantum Lambda-Calculus

Quantum lambda calculus has been studied mainly as an idealized programming language -- the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus is standardization and normalization results.

cs.LO↗
arXiv2025

Variable Elimination as Rewriting in a Linear Lambda Calculus

Variable Elimination (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, here expressed in an idealized probabilistic functional language -- a linear simply-typed $λ$-calculus suffices for our purpose. Precisely, we express 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.

cs.LO↗
arXiv2023

Higher-Order Bayesian Networks, Exactly (Extended version)

Bayesian networks (BNs) are graphical \emph{first-order} probabilistic models that allow for a compact representation of large probability distributions, and for efficient inference, both exact and approximate. We introduce a \emph{higher-order} programming language -- in the idealized form of a $λ$-calculus -- which we prove \emph{sound and complete} w.r.t. BNs: each BN can be encoded as a term, and conversely each (possibly higher-order and recursive) program of ground type \emph{compiles} into a BN. The language allows for the specification of recursive probability models and hierarchical structures. Moreover, we provide a \emph{compositional} and \emph{cost-aware} semantics which is based on factors, the standard mathematical tool used in Bayesian inference. Our results rely on advanced techniques rooted into linear logic, intersection types, rewriting theory, and Girard's geometry of interaction, which are here combined in a novel way.

cs.LO↗
arXiv2023

Normal Form Bisimulations By Value

Normal form bisimilarities are a natural form of program equivalence resting on open terms, first introduced by Sangiorgi in call-by-name. The literature contains a normal form bisimilarity for Plotkin's call-by-value $λ$-calculus, Lassen's \emph{enf bisimilarity}, which validates all of Moggi's monadic laws and can be extended to validate $η$. It does not validate, however, other relevant principles, such as the identification of meaningless terms -- validated instead by Sangiorgi's bisimilarity -- or the commutation of $\letexp$s. These shortcomings are due to issues with open terms of Plotkin's calculus. We introduce a new call-by-value normal form bisimilarity, deemed \emph{net bisimilarity}, closer in spirit to Sangiorgi's and satisfying the additional principles. We develop it on top of an existing formalism designed for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are \emph{incomparable}, as net bisimilarity does not validate Moggi's laws nor $η$. Moreover, there is no easy way to merge them. To better understand the situation, we provide an analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard's relational model.

cs.LO↗
arXiv2022

On reduction and normalization in the computational core

We study the reduction in a lambda-calculus derived from Moggi's computational one, that we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form, and address the question of normalizing strategies. Our analysis relies on factorization results.

cs.LO↗
arXiv2022

Strategies for Asymptotic Normalization

We present a technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit, as opposite to reaching a normal form in a finite number of steps. Asymptotic termination occurs in several settings, such as effectful, and in particular probabilistic computation -- where the limits are distributions over the possible outputs -- or infinitary lambda-calculi -- where the limits are infinitary normal forms such as Boehm trees. As a concrete application, we obtain a result which is of independent interest: a normalization theorem for Call-by-Value (and -- in a uniform way -- for Call-by-Name) probabilistic lambda-calculus.

cs.LO↗
arXiv2022

Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms

While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. In this paper we study the question of uniqueness of the result (unique limit distribution), and develop a set of proof techniques to analyze and compare reduction strategies. The goal is to have tools to support the operational analysis of probabilistic calculi (such as probabilistic lambda-calculi) where evaluation allows for different reduction choices (hence different reduction paths).

cs.LO↗
arXiv2021

Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)

In each variant of the lambda-calculus, factorization and normalization are two key-properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the lambda-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV. The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.

cs.LO↗
arXiv2020

Factorize Factorization

Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our technique is well adapted to deal with extensions of the call-by-name and call-by-value lambda-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with beta-reduction. We then closely analyze some common factorization schemas for the lambda-calculus. Concretely, we apply our technique to diverse extensions of the lambda-calculus, among which de' Liguoro and Piperno's non-deterministic lambda-calculus and -- for call-by-value -- Carraro and Guerrieri's shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.

cs.LO↗
arXiv2020

Intersection Types and (Positive) Almost-Sure Termination

Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of obtaining any given result, rather than the possibility or the necessity of obtaining it, like in (non)deterministic computation. Termination, arguably the simplest kind of reachability problem, can be spelled out in at least two ways, depending on whether it talks about the probability of convergence or about the expected evaluation time, the second one providing a stronger guarantee. In this paper, we show that intersection types are capable of precisely characterizing both notions of termination inside a single system of types: the probability of convergence of any lambda-term can be underapproximated by its type, while the underlying derivation's weight gives a lower bound to the term's expected number of steps to normal form. Noticeably, both approximations are tight -- not only soundness but also completeness holds. The crucial ingredient is non-idempotency, without which it would be impossible to reason on the expected number of reduction steps which are necessary to completely evaluate any term. Besides, the kind of approximation we obtain is proved to be optimal recursion theoretically: no recursively enumerable formal system can do better than that.

cs.LO↗
arXiv2019

Factorization and Normalization, Essentially

Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or normalization theorems. In this paper we provide simple proof techniques for these theorems. Our starting point is a revisitation of Takahashi's technique to prove factorization for head reduction. Our technique is both simpler and more powerful, as it works in cases where Takahishi's does not. We then pair factorization with two other abstract properties, defining \emph{essential systems}, and show that normalization follows. Concretely, we apply the technique to four case studies, two classic ones, head and the leftmost-outermost reductions, and two less classic ones, non-deterministic weak call-by-value and least-level reductions.

cs.LO↗
arXiv2019

Lambda Calculus and Probabilistic Computation

We introduce two extensions of the $λ$-calculus with a probabilistic choice operator, $Λ_\oplus^{cbv}$ and $Λ_\oplus^{cbn}$, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, $Λ_\oplus^!$, which allows for a fine control of the interaction between choice and copying, and which allows us to develop a unified, modular approach.

cs.LO↗
arXiv2017

The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects

We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a full quantum programming language in which entanglement, duplication, and recursion are all available. Our model comes with a multi-token machine, a proof net system, and a PCF-style language. The approach we develop is not specific to quantum computation, and our model is an instance of a new framework whose main feature is the ability to model commutative effects in a parallel setting. Being based on a multi-token machine equipped with a memory, it has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages.

cs.LO↗
arXiv2015

Parallelism and Synchronization in an Infinitary Context (Long Version)

We study multitoken interaction machines in the context of a very expressive logical system with exponentials, fixpoints and synchronization. The advantage of such machines is to provide models in the style of the Geometry of Interaction, i.e., an interactive semantics which is close to low-level implementation. On the one hand, we prove that despite the inherent complexity of the framework, interaction is guaranteed to be deadlock free. On the other hand, the resulting logical system is powerful enough to embed PCF and to adequately model its behaviour, both when call-by-name and when call-by-value evaluation are considered. This is not the case for single-token stateless interactive machines.

cs.LO↗
arXiv2014

The Geometry of Synchronization (Long Version)

We graft synchronization onto Girard's Geometry of Interaction in its most concrete form, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling synchronization points, and of a multi-token abstract machine model for it. Interestingly, the correctness criterion ensures the absence of deadlocks along reduction and in the underlying machine, this way linking logical and operational properties.

cs.LO↗