Emmy-Noether-Seminar: Tensors of Computational Effects and a Logic for Probabilistic Traces

Tensors of Computational Effects and a Logic for Probabilistic Traces

Sergey Goncharov (FAU)

Abstract: Computational effects is a pivotal aspect that distinguishes functions in the mathematical sense from those, one uses in programming. Examples of computational effects are: non-termination, non-determinism, background memory, input/output, but also probability, which is computationally sensible in the context of probabilistic programming. An established way to formally capture computational effects is to associate them with (strong) monads in the corresponding semantic categories, in the simplest case — in the category of sets and functions. In this category, monads are known to be equivalent to algebraic theories (possibly over operations of infinite arities). Combining monads, and the corresponding theories in a canonical way is an important subject in semantics of programming languages. In this context, tensors of monads on the one hand correspond to a practically relevant, universal, commutative combination of effects, and on the other hand tend to yield highly non-trivial mathematical challenges. In my talk, I will concentrate on the special case of tensoring countable probability distributions with free theories, and present recent results on completeness and definability in the corresponding equational logic w.r.t. a natural model of probabilistic traces.

[This is a joint work with Paul Blain Levy and Nathan Bowler]