ABSTRACT. This paper presents a wp-style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one- and two-sided bounds for such expectations, and show the soundness of our wp-calculus with respect to a probabilistic pushdown automaton semantics. We also give a wp-style calculus for obtaining bounds on the expected runtime of recursive programs that can be used to determine the (possibly infinite) time until termination of such programs.

ABSTRACT. \emph{Healthiness} is a good old question in program logics that dates back to Dijkstra. It asks for an intrinsic characterization of those predicate transformers which arise as the (backward) interpretation of a certain class of programs. There are several results known for healthiness conditions: for deterministic programs, nondeterministic ones, probabilistic ones, etc. Building upon our previous works on so-called \emph{state-and-effect triangles}, we contribute a unified categorical framework for investigating healthiness conditions. We find the framework to be centered around a \emph{dual adjunction} induced by a dualizing object, together with our notion of \emph{relative Eilenberg-Moore algebra} playing fundamental roles too. The latter notion seems interesting in its own right in the context of monads, Lawvere theories and enriched categories.

ABSTRACT. We show that the Kolmogorov extension theorem and the Doob martingale convergence theorem are two aspects of a common generalization, namely a colimit-like construction in a category of Radon spaces and reversible Markov kernels. The construction provides a compositional denotational semantics for iteration operators in probabilistic programming languages as a limit of finite approximants, even in the absence of a natural partial order.

ABSTRACT. We develop a quantitative analogue of equational reasoning which we call quantitative algebra. We define an equality relation indexed by rationals: a = b which we think of as saying that “a is approximately equal to b up to an error of e”. We have 4 interesting examples where we have a quantitative equational theory whose free algebras correspond to well-known structures. In each case we have finitary and continuous versions. The four cases are: Hausdorff metrics from quantitive semilattices; Kantorovich metrics from barycentric algebras and also from pointed barycentric algebras; total variation from a variant of barycentric algebras.

ABSTRACT. String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs), an algebraic structure that features sequential and parallel composition. They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory.

An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. This paper lays a comprehensive foundation of this form of rewriting. We interpret diagrams combinatorially as typed hypergraphs and establish the precise correspondence between diagram rewriting modulo the laws of SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs, subject to a soundness condition, on the other. This result rests on a more general characterisation theorem in which we show that typed hypergraph DPO rewriting amounts to diagram rewriting modulo the laws of SMCs with a chosen special Frobenius monoid.

We illustrate our approach with a proof of termination for the theory of non-commutative bimonoids.

ABSTRACT. Brenier's theorem is a landmark result in Optimal Transport. It postulates existence, monotonicity and uniqueness of an optimal, with respect to the quadratic cost function, map between two given probability measures. We prove an effective version of Brenier's theorem: for any two computable absolutely continuous measures on R^n, \mu and nu, with some conditions on their support, there exists a computable convex function \phi, whose gradient is the optimal transport map between \mu and \nu.

The main insight of the paper is the idea that an effective Brenier's theorem can be used to construct effective monotone maps with desired (non-)differentiability properties. We use it to solve several problems at the interface of algorithmic randomness and computable analysis. In particular, we show that z\in\R^n is computably random if and only if every computable monotone function on \R^n is differentiable at z. Furthermore, we prove the converse of the effective Aleksandrov's theorem: we show that if z\in\R^n is not computably random, there exists a computable convex function that is not twice differentiable at z. Finally, we prove several new characterisations of computable randomness in \R^n: in terms of differentiability of computable measures, in terms of a particular Monge-Amp\'ere equation and in terms of critical values of computable Lipschitz functions.

ABSTRACT. An operation f on the domain of an algebra A is definable if there is a first order logic formula F(x,y) with parameters from A such that for all x from A^n and bin A we have f(a)=b if and only if A satisfies F(a, b). The goal of this paper is to study definability of operations by quantifier-free formulas on countable infinite algebras from view points of computability and model-theoretic definability.

ABSTRACT. We propose an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.

ABSTRACT. Over the last decade, differential privacy has achieved widespread adoption within the privacy community. Moreover, it has attracted significant attention from the verification community, resulting in several successful tools for formally proving differential privacy. Although their technical approaches vary greatly, all existing tools rely on reasoning principles derived from the composition theorem of differential privacy. While this suffices to verify most common private algorithms, there are several important algorithms whose privacy analysis does not rely solely on the composition theorem. Their proofs are significantly more complex, and are currently beyond the reach of verification tools.

In this paper, we formally verify differential privacy for two such algorithms: the Exponential mechanism and the Above Threshold routine, the critical component of the famous Sparse Vector algorithm. We identify a deep connection between differential privacy and (approximate) probabilistic couplings, an established mathematical tool for reasoning about stochastic processes. Even when the composition theorem is not helpful, we can often prove privacy by constructing an approximate coupling.

We verify our examples in a relational program logic apRHL+, which can construct approximate couplings. This logic extends the existing apRHLlogic with more general rules for the Laplace mechanism, inspired by the connection with coupling, and new structural rules enabling pointwise reasoning about privacy. While our paper is presented from a formal verification perspective, we believe that its main insight is of independent interest for the differential privacy community.

ABSTRACT. This is the first paper to propose a pure event structures model of relaxed memory. We propose confusion-free event structures over an alphabet with a justification relation as a model. Executions are modeled by justified configurations, where every read event has a justifying write event. Justification alone is too weak a criterion, since it allows cycles of the kind that result in so-called thin-air reads. Acyclic justification forbids such cycles, but also invalidates event reorderings that result from compiler optimizations and dynamic instruction scheduling. We propose a notion well-justification, based on a game-like model, which strikes a middle ground. We show that well-justified configurations satisfy the DRF theorem: in any data-race free program, all well-justified configurations are sequentially consistent. We also show that rely-guarantee reasoning is sound for well-justified configurations, but not for justified configurations. For example, well-justified configurations are type-safe. Well-justification allows many, but not all reorderings performed by relaxed memory. In particular, it fails to validate the commutation of memory access on different variables. We discuss variations that may address these shortcomings.

ABSTRACT. Feedback is an essential composition operator in many classes of reactive and other systems. This paper studies feedback in the context of compositional theories with refinement. Such theories allow to reason about systems on a component-by-component basis, and to characterize substitutability as a refinement relation. Although compositional theories of feedback do exist, they are limited either to deterministic systems (functions) or input-receptive systems (total relations). In this work we propose a compositional theory of feedback which applies to non-deterministic and non-input-receptive systems (e.g., partial relations). To achieve this, we use the semantic frameworks of predicate and property transformers, and relations with fail and unknown values. We show how to define instantaneous feedback for stateless systems and feedback with unit delay for stateful systems. Both operations preserve the refinement relation, and both can be applied to non-deterministic and non-input-receptive systems.

ABSTRACT. Fokkink, van Glabbeek and de Wind (2012) presented a method to decompose modal formulas for processes with the internal action tau; congruence formats for branching and eta-bisimilarity were derived on the basis of this decomposition method. The idea is that a congruence format for a semantics must ensure that formulas in the modal characterisation of this semantics are always decomposed into formulas in this modal characterisation. Here the decomposition method is enhanced to deal with modal characterisations that contain a modality phi, to derive congruence formats for delay and weak bisimilarity.

ABSTRACT. We study the strength of set-theoretic axioms needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. We first show that the complementation theorem for non-deterministic tree automata is equivalent to the determinacy of all Gale-Stewart games given by Bool(Sigma^0_2) sets over the moderately strong second-order arithmetic theory ACA_0. It follows that the complementation theorem is provable from Pi^1_3- but not Delta^1_3-comprehension.

We then use results due to MedSalem-Tanaka, Möllerfeld and Heinatsch-Möllerfeld to prove that - the complementation theorem for non-deterministic tree automata, - the decidability of the Pi^1_3 fragment of MSO on the infinite binary tree, - the positional determinacy of parity games, and - the determinacy of Bool(\Sigma^0_2) Gale-Stewart games are all equivalent over Pi^1_2-comprehension. It follows in particular that Rabin's decidability theorem is not provable from Delta^1_3-comprehension.

ABSTRACT. We consider a continuous analogue of Cai et al. and Babai et al.'s problem of solving multiplicative matrix equations. Given k+1 square matrices A_1, ..., A_k, C, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals t_1, ..., t_k such that exp(A_1*t_1)*...*exp(A_k*t_k) = C.

We show that this problem is undecidable in general, but decidable under the assumption that the matrices A_1, ..., A_k commute. Our results have applications to reachability problems for linear hybrid automata.

Our decidability proof relies on a number of theorems from algebraic and transcendental number theory, most notably those of Baker, Kronecker, Lindemann, and Masser, as well as some useful geometric and linear-algebraic results, including the Minkowski-Weyl theorem and a new (to the best of our knowledge) result about the uniqueness of strictly upper triangular matrix logarithms of upper unitriangular matrices. On the other hand, our undecidability result is shown by reduction from Hilbert's Tenth Problem.

ABSTRACT. It is shown that order-invariance and successor-invariance of two-variable first-logic are decidable in the finite. This is an immediate consequence of decision procedures obtained for the finite satisfiability problem for existential second-order logic with two first-order variables ($\esotwo$) on structures with (1) two linear orders and one induced successor, and (2) two successors and one induced linear order. Previously decidability was only known for monadic $\esotwo$ on those structures. In addition, the finite satisfiability problem for $\esotwo$ on structures with one linear order and its induced successor relation is shown to be complete for non-deterministic exponential time.

ABSTRACT. Guardedness restrictions are one of the principal means to obtain decidable logics --- operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.

ABSTRACT. The Cook-Levin theorem (the statement that SAT is NP-complete) is a central result in structural complexity theory.  Is it possible to prove it using the lambda-calculus instead of Turing machines?  We address this question via the notion of affine approximation, which offers the possibility of using order-theoretic arguments, in contrast to the machine-level arguments employed in standard proofs.  However, due to the size explosion problem in the lambda-calculus (a linear number of reduction steps may generate exponentially big terms), a naive transliteration of the proof of the Cook-Levin theorem fails.  We propose to fix this mismatch using the author's recently introduced parsimonious lambda-calculus, reproving the Cook-Levin theorem and several related results in this higher-order framework.  We also present an interesting relationship between approximations and intersection types, and discuss potential applications.

ABSTRACT. We promote the theory of computational complexity on metric spaces: as natural common generalization of (i) the classical discrete setting of integers, binary strings, graphs etc. as well as of (ii) the bit-complexity theory on the spaces of real numbers and continuous functions according to Friedman, Ko (1982ff), Cook, Braverman et al.; as (iii) resource-bounded refinement of the theories of computability on, and representations of, continuous universes by Pour-El&Richards (1989) and Weihrauch (1993ff) and as (iv) recursion-theoretic refinement of quantitative concepts from classical Analysis: Our main results relate (i.e. upper and lower bound) Kolmogorov's entropy of a compact metric space X polynomially to the uniform relativized computational complexity of various families of continuous functions on X. The upper bounds are attained by carefully designed oracles and bit-cost analyses of algorithms perusing them. They all employ the same representation (i.e. encoding, as infinite binary sequences, of the elements) of such spaces, which thus may be of own interest. The lower bounds adapt adversary arguments from unit-cost Information-Based Complexity to the bit model. They extend to, and indicate perhaps surprising limitations in this worst-case sense even of, encodings via binary string functions (rather than sequences) as introduced by Kawamura&Cook (SToC'2010,§3.4). These insights offer some guidance towards suitable notions of complexity for higher types.

ABSTRACT. The evaluation problem for Conjunctive Queries (CQ) is known to be NP-complete in combined complexity and W[1]-complete in parameterized complexity. However, acyclic CQs and more generally CQs of bounded tree-width can be evaluated in polynomial time in combined complexity and they are fixed-parameter tractable.

We study the problem of whether a CQ can be rewritten into an equivalent CQ of bounded tree-width, in the presence of unary functional dependencies. We show that this problem is decidable in doubly exponential time, or in exponential time for a restricted class of queries. When it exists, the algorithm also yields a witness query.

ABSTRACT. Weighted automata (WA) extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. Recently, cost register automata (CRA) have been introduced as an alternative model to describe any function realised by a WA by means of a deterministic machine. Unambiguous WA over a monoid (M, ⊗) can equivalently be described by cost register automata whose registers take their values in M, and are up- dated by operations of the form x := y⊗c, with c ∈ M. This class is denoted by CRA⊗c(M). We introduce a twinning property and a bounded variation property parametrised by an integer k, such that the corresponding notions introduced originally by Choffrut for finite-state transducers are obtained for k = 1. Given an unambiguous weighted automaton W over an infinitary group (G,⊗) realizing some function f, we prove that the three following properties are equivalent: i) W satisfies the twinning property of order k, ii) f satisfies the k-bounded variation property, and iii) f can be described by a CRA⊗c(G) with at most k registers. In the spirit of tranducers, we actually prove this result in a more general setting by considering machines over the semiring of finite sets of elements from (G,⊗): the three properties are still equivalent for such finite-valued weighted automata, that is the ones associating with words subsets of G of cardinality at most l, for some natural l. Moreover, we show that if the operation ⊗ of G is commutative and computable, then one can decide whether a WA satisfies the twinning property of order k. As a corollary, this allows to decide the register minimisation problem for the class CRA⊗c(G). Last, we prove that a similar result holds for finite-valued finite- state transducers, and that the register minimisation problem for the class CRA·c(B∗) is PSPACE-complete.

ABSTRACT. Context free languages allow one to express data with hierarchical structure, at the cost of losing some of the useful properties of languages recognized by finite automata on words. However, it is possible to restore some of these properties by making the structure of the tree visible, such as is done by visibly pushdown languages, or finite automata on trees. In this paper, we show that the structure given by such approaches remains invisible when it is read by a finite automaton (on word). In particular, we show that separability with a regular language is undecidable for visibly pushdown languages, just as it is undecidable for general context free languages.

ABSTRACT. Symbolic tree automata allow transitions to carry predicates over rich alphabet theories, such as linear arithmetic, and therefore extend finite tree automata to operate over infinite alphabets, such as the set of rational numbers. Existing tree automata algorithms rely on the alphabet being finite, and generalizing them to the symbolic setting is not a trivial task. In this paper we study the problem of minimizing symbolic tree automata. First, we formally define and prove the basic properties of minimality in the symbolic setting. Second, we lift existing minimization algorithms to symbolic tree automata. Third, we present a new algorithm based on the following idea: the problem of minimizing symbolic tree automata can be reduced to the problem of minimizing symbolic (string) automata by encoding the tree structure as part of the alphabet theory. We implement and evaluate all our algorithms against existing implementations and show that the symbolic algorithms scale to large alphabets and can minimize automata over complex alphabet theories.