arXiv subjects

Sam Staton

Publications and source records attributed to Sam Staton.

At least 37 records · Page 2Linked to original sources

arXiv2023

Proceedings of the Sixth International Conference on Applied Category Theory 2023

The Sixth International Conference on Applied Category Theory took place at the University of Maryland, 31 July -- 4 August 2023. This conference follows the previous meetings at Leiden (2018), Oxford (2019), MIT (2020, fully online), Cambridge (2021) and Glasgow (2022). The conference comprised contributed talks, a poster session, an industry showcase session, and a session where junior researchers who had attended the Adjoint School presented the results of their research at the school. Information regarding the conference may be found at (https://act2023.github.io/). The contributions to ACT2023 ranged from pure to applied and included contributions in a wide range of disciplines in science and engineering. Submission to ACT 2023 had three tracks: extended abstracts, software demonstrations, and proceedings. Only papers submitted to the proceedings track were considered for publication in this volume.

cs.LO↗

arXiv2023

A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories

Stochastic memoization is a higher-order construct of probabilistic programming languages that is key in Bayesian nonparametrics, a modular approach that allows us to extend models beyond their parametric limitations and compose them in an elegant and principled manner. Stochastic memoization is simple and useful in practice, but semantically elusive, particularly regarding dataflow transformations. As the naive implementation resorts to the state monad, which is not commutative, it is not clear if stochastic memoization preserves the dataflow property -- i.e., whether we can reorder the lines of a program without changing its semantics, provided the dataflow graph is preserved. In this paper, we give an operational and categorical semantics to stochastic memoization and name generation in the context of a minimal probabilistic programming language, for a restricted class of functions. Our contribution is a first model of stochastic memoization of constant Bernoulli functions with a non-enumerable type, which validates data flow transformations, bridging the gap between traditional probability theory and higher-order probability models. Our model uses a presheaf category and a novel probability monad on it.

cs.PL↗

arXiv2023

Quantum de Finetti Theorems as Categorical Limits, and Limits of State Spaces of C*-algebras

De Finetti theorems tell us that if we expect the likelihood of outcomes to be independent of their order, then these sequences of outcomes could be equivalently generated by drawing an experiment at random from a distribution, and repeating it over and over. In particular, the quantum de Finetti theorem says that exchangeable sequences of quantum states are always represented by distributions over a single state produced over and over. The main result of this paper is that this quantum de Finetti construction has a universal property as a categorical limit. This allows us to pass canonically between categorical treatments of finite dimensional quantum theory and the infinite dimensional. The treatment here is through understanding properties of (co)limits with respect to the contravariant functor which takes a C*-algebra describing a physical system to its convex, compact space of states, and through discussion of the Radon probability monad. We also show that the same categorical analysis also justifies a continuous de Finetti theorem for classical probability.

quant-ph↗

arXiv2023

$ω$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs

We introduce a new setting, the category of $ω$PAP spaces, for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to most practical probabilistic and differentiable programs, including those that use general recursion, higher-order functions, discontinuous primitives, and both discrete and continuous sampling. But crucially, it is also specific enough to exclude many pathological denotations, enabling us to establish new results about both deterministic differentiable programs and probabilistic programs. In the deterministic setting, we prove very general correctness theorems for automatic differentiation and its use within gradient descent. In the probabilistic setting, we establish the almost-everywhere differentiability of probabilistic programs' trace density functions, and the existence of convenient base measures for density computation in Monte Carlo inference. In some cases these results were previously known, but required detailed proofs with an operational flavor; by contrast, all our proofs work directly with programs' denotations.

cs.PL↗

arXiv2022

Affine Monads and Lazy Structures for Bayesian Programming

We show that streams and lazy data structures are a natural idiom for programming with infinite-dimensional Bayesian methods such as Poisson processes, Gaussian processes, jump processes, Dirichlet processes, and Beta processes. The crucial semantic idea, inspired by developments in synthetic probability theory, is to work with two separate monads: an affine monad of probability, which supports laziness, and a commutative, non-affine monad of measures, which does not. (Affine means that $T(1)\cong 1$.) We show that the separation is important from a decidability perspective, and that the recent model of quasi-Borel spaces supports these two monads. To perform Bayesian inference with these examples, we introduce new inference methods that are specially adapted to laziness; they are proven correct by reference to the Metropolis-Hastings-Green method. Our theoretical development is implemented as a Haskell library, LazyPPL.

cs.PL↗

arXiv2022

ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs

Optimizing the expected values of probabilistic processes is a central problem in computer science and its applications, arising in fields ranging from artificial intelligence to operations research to statistical computing. Unfortunately, automatic differentiation techniques developed for deterministic programs do not in general compute the correct gradients needed for widely used solutions based on gradient-based optimization. In this paper, we present ADEV, an extension to forward-mode AD that correctly differentiates the expectations of probabilistic processes represented as programs that make random choices. Our algorithm is a source-to-source program transformation on an expressive, higher-order language for probabilistic computation, with both discrete and continuous probability distributions. The result of our transformation is a new probabilistic program, whose expected return value is the derivative of the original program's expectation. This output program can be run to generate unbiased Monte Carlo estimates of the desired gradient, which can then be used within the inner loop of stochastic gradient descent. We prove ADEV correct using logical relations over the denotations of the source and target probabilistic programs. Because it modularly extends forward-mode AD, our algorithm lends itself to a concise implementation strategy, which we exploit to develop a prototype in just a few dozen lines of Haskell (https://github.com/probcomp/adev).

cs.PL↗

arXiv2022

Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)

We study concrete sheaf models for a call-by-value higher-order language with recursion. Our family of sheaf models is a generalization of many examples from the literature, such as models for probabilistic and differentiable programming, and fully abstract logical relations models. We treat recursion in the spirit of synthetic domain theory. We provide a general construction of a lifting monad starting from a class of admissible monomorphisms in the site of the sheaf category. In this way, we obtain a family of models parametrized by a concrete site and a class of monomorphisms, for which we prove a general computational adequacy theorem.

cs.PL↗

arXiv2021

Monads for Measurable Queries in Probabilistic Databases

We consider a bag (multiset) monad on the category of standard Borel spaces, and show that it gives a free measurable commutative monoid. Firstly, we show that a recent measurability result for probabilistic database queries (Grohe and Lindner, ICDT 2020) follows quickly from the fact that queries can be expressed in monad-based terms. We also extend this measurability result to a fuller query language. Secondly, we discuss a distributive law between probability and bag monads, and we illustrate that this is useful for generating probabilistic databases.

cs.PL↗

arXiv2021

A Domain Theory for Statistical Probabilistic Programming

We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.

cs.LO↗

arXiv2021

Recursion and Sequentiality in Categories of Sheaves

We present a fully abstract model of a call-by-value language with higher-order functions, recursion and natural numbers, as an exponential ideal in a topos. Our model is inspired by the fully abstract models of O'Hearn, Riecke and Sandholm, and Marz and Streicher. In contrast with semantics based on cpo's, we treat recursion as just one feature in a model built by combining a choice of modular components.

cs.PL↗

arXiv2021

Compositional Semantics for Probabilistic Programs with Exact Conditioning

We define a probabilistic programming language for Gaussian random variables with a first-class exact conditioning construct. We give operational, denotational and equational semantics for this language, establishing convenient properties like exchangeability of conditions. Conditioning on equality of continuous random variables is nontrivial, as the exact observation may have probability zero; this is Borel's paradox. Using categorical formulations of conditional probability, we show that the good properties of our language are not particular to Gaussians, but can be derived from universal properties, thus generalizing to wider settings. We define the Cond construction, which internalizes conditioning as a morphism, providing general compositional semantics for probabilistic programming with exact conditioning.

cs.PL↗

arXiv2021

A Monad for Probabilistic Point Processes

A point process on a space is a random bag of elements of that space. In this paper we explore programming with point processes in a monadic style. To this end we identify point processes on a space X with probability measures of bags of elements in X. We describe this view of point processes using the composition of the Giry and bag monads on the category of measurable spaces and functions and prove that this composition also forms a monad using a distributive law for monads. Finally, we define a morphism from a point process to its intensity measure, and show that this is a monad morphism. A special case of this monad morphism gives us Wald's Lemma, an identity used to calculate the expected value of the sum of a random number of random variables. Using our monad we define a range of point processes and point process operations and compositionally compute their corresponding intensity measures using the monad morphism.

cs.PL↗

arXiv2020

Probabilistic Programming Semantics for Name Generation

We make a formal analogy between random sampling and fresh name generation. We show that quasi-Borel spaces, a model for probabilistic programming, can soundly interpret Stark's $ν$-calculus, a calculus for name generation. Moreover, we prove that this semantics is fully abstract up to first-order types. This is surprising for an 'off-the-shelf' model, and requires a novel analysis of probability distributions on function spaces. Our tools are diverse and include descriptive set theory and normal forms for the $ν$-calculus.

cs.PL↗

arXiv2020

A Convenient Category for Higher-Order Probability Theory

Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed. Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.

cs.PL↗

arXiv2020

De Finetti's construction as a categorical limit

This paper reformulates a classical result in probability theory from the 1930s in modern categorical terms: de Finetti's representation theorem is redescribed as limit statement for a chain of finite spaces in the Kleisli category of the Giry monad. This new limit is used to identify among exchangeable coalgebras the final one.

math.CT↗

arXiv2020

A Generalization of Hierarchical Exchangeability on Trees to Directed Acyclic Graphs

Motivated by the problem of designing inference-friendly Bayesian nonparametric models in probabilistic programming languages, we introduce a general class of partially exchangeable random arrays which generalizes the notion of hierarchical exchangeability introduced in Austin and Panchenko (2014). We say that our partially exchangeable arrays are DAG-exchangeable since their partially exchangeable structure is governed by a collection of Directed Acyclic Graphs. More specifically, such a random array is indexed by $\mathbb{N}^{|V|}$ for some DAG $G=(V,E)$, and its exchangeability structure is governed by the edge set $E$. We prove a representation theorem for such arrays which generalizes the Aldous-Hoover and Austin-Panchenko representation theorems.

math.PR↗

arXiv2020

Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing

We present semantic correctness proofs of Automatic Differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Finally, we sketch how the analysis extends to other AD methods by considering a continuation-based method.

cs.PL↗

arXiv2020

Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory

We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.

cs.LO↗