Searcharxiv⌕ Search

arXiv subjects

Sam Staton

Publications and source records attributed to Sam Staton.

45 records · Page 3Linked to original sources
arXiv2019

Quantum channels as a categorical completion

We propose a categorical foundation for the connection between pure and mixed states in quantum information and quantum computation. The foundation is based on distributive monoidal categories. First, we prove that the category of all quantum channels is a canonical completion of the category of pure quantum operations (with ancilla preparations). More precisely, we prove that the category of completely positive trace-preserving maps between finite-dimensional C*-algebras is a canonical completion of the category of finite-dimensional vector spaces and isometries. Second, we extend our result to give a foundation to the topological relationships between quantum channels. We do this by generalizing our categorical foundation to the topologically-enriched setting. In particular, we show that the operator norm topology on quantum channels is the canonical topology induced by the norm topology on isometries.

cs.LO↗
arXiv2019

Universal Properties in Quantum Theory

We argue that notions in quantum theory should have universal properties in the sense of category theory. We consider the completely positive trace preserving (CPTP) maps, the basic notion of quantum channel. Physically, quantum channels are derived from pure quantum theory by allowing discarding. We phrase this in category theoretic terms by showing that the category of CPTP maps is the universal monoidal category with a terminal unit that has a functor from the category of isometries. In other words, the CPTP maps are the affine reflection of the isometries.

quant-ph↗
arXiv2018

The Beta-Bernoulli process and algebraic effects

In this paper we use the framework of algebraic effects from programming language theory to analyze the Beta-Bernoulli process, a standard building block in Bayesian models. Our analysis reveals the importance of abstract data types, and two types of program equations, called commutativity and discardability. We develop an equational theory of terms that use the Beta-Bernoulli process, and show that the theory is complete with respect to the measure-theoretic semantics, and also in the syntactic sense of Post. Our analysis has a potential for being generalized to other stochastic processes relevant to Bayesian modelling, yielding new understanding of these processes from the perspective of programming.

cs.PL↗
arXiv2017

Denotational validation of higher-order Bayesian inference

We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics. Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as function application. We overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions. We define a class of semantic structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. We develop a collection of building blocks for composing representations. We use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To emphasize the connection between the semantic manipulation and its traditional measure theoretic origins, we use Kock's synthetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.

cs.PL↗
arXiv2017

A monad for full ground reference cells

We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.

cs.PL↗
arXiv2016

Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints

We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.

cs.PL↗
arXiv2014

Linear usage of state

We investigate the phenomenon that "every monad is a linear state monad". We do this by studying a fully-complete state-passing translation from an impure call-by-value language to a new linear type theory: the enriched call-by-value calculus. The results are not specific to store, but can be applied to any computational effect expressible using algebraic operations, even to effects that are not usually thought of as stateful. There is a bijective correspondence between generic effects in the source language and state access operations in the enriched call-by-value calculus. From the perspective of categorical models, the enriched call-by-value calculus suggests a refinement of the traditional Kleisli models of effectful call-by-value languages. The new models can be understood as enriched adjunctions.

cs.PL↗
arXiv2011

Relating coalgebraic notions of bisimulation

The theory of coalgebras, for an endofunctor on a category, has been proposed as a general theory of transition systems. We investigate and relate four generalizations of bisimulation to this setting, providing conditions under which the four different generalizations coincide. We study transfinite sequences whose limits are the greatest bisimulations.

cs.LO↗