Interactions between logic and computer science have been deeply investigated in the last century, but, surprisingly, the study of probabilistic computation was only marginally touched by such fruitful interchanges. The goal of my doctoral project was precisely that of start bridging this gap by developing logical systems corresponding to specific aspects of randomized computation and, thus, by generalizing standard achievements to the probabilistic realm. To do so, the key ingredient is the introduction of new, measure-sensitive quantifiers associated with quantitative interpretations. Concretely, the dissertation is tripartite. The first part concerns counting complexity and its main result is the proof that classical counting propositional logic provides a purely logical characterization of Wagner's hierarchy [1]. In the second part, which focusses on programming language theory, we present a probabilistic CurryHoward correspondence [2] between the intuitionistic version of our counting propositional logic and the typed probabilistic -calculus with counting quantifiers. Finally, we consider the relationship between arithmetic and computation by introducing a quantitative extension of the language of Peano arithmetic able to formalize basic results from probability theory. This language is also our starting point to define randomized bounded arithmetic and, so, to generalize canonical results by Buss [3].
Historically, determinacy was certainly one of the defining features of standard computational models: given an algorithm and an input, the sequence of computation steps is uniquely determined. In the second half of the XX century, this assumption started to be relaxed in diferent ways and randomized algorithms were introduced for the first time – where a randomized algorithm is a process which can evolve probabilistically so that, given an input, the computation it performs may lead to diferent outcomes, each associated with a certain probability. Such a more flexible design makes this computational model a very eficient and powerful tool, with several applications in computer science (CS, for short) and technology.
Starting from this, my Ph.D. dissertation has been motivated by two main considerations. On the one hand, since its early appearance in the 1950s, probabilistic computation has become ubiquitous in several fast-growing areas of CS and, by now, related, abstract models – as probabilistic Turing machines (PTM, for short), stochastic automata or randomized -calculi – have been deeply investigated in the literature. On the other, there exist deep and mutual interactions linking logic and theoretical computer science (TCS, for short), and, in the past, the development and study of computation theory and models has considerably benefitted from them. Yet, randomized computation was only marginally touched by such fruitful interchanges and, so far, it has not found a precise logical counterpart. Such a missing connection looks even more striking nowadays, due to the increasing pervasiveness of probability in many relevant fields of information technology, from AI and statistical learning to cryptography, approximate computing and robotics. The global purpose of my doctoral thesis consisted in laying the foundation for a uniform approach to bridge the quoted gap. To do so, the key ingredient is the introduction of a family of new logics, the language of which includes nonstandard quantifiers “measuring” the probability of their argument formula, and associated with inherently quantitative semantics.
As said, randomized algorithms are powerful tools with numerous applications in diferent
ifelds and technologies. Generally speaking, these are crucial when dealing with uncertain
information and partial knowledge, namely for all systems acting in realistic contexts – think,
for example, of driverless cars [
On Logical Foundations of Computer Science. The existence of several and deep
interactions between logic and TCS is not accidental, but rooted in the intimate correspondence
connecting these disciplines. In fact, even the formal appearance of the science of computing
was essentially motivated by foundational studies in mathematics and logic, that had defined
the context in which this subject took its first steps. Later on, the back and forth between logic
and CS has strongly influenced the development of both and, today, numerous areas of IT – as
programming language theory [
Probabilistic Computation. Probabilistic computational models have been widely investigated in the last few years, and are nowadays pervasive in almost every areas of CS. As seen, the idea of relaxing the notion of algorithm from purely deterministic to probabilistic appeared early in the history of modern computability theory. Intuitively, as anticipated, a randomized algorithm is nothing but an algorithm involving random processes – typically corresponding to “flipping a coin” – as part of its procedure. While in deterministic computation, for every input, the algorithm produces (at most) one output, in randomized computation, given an input, the algorithm ℛ returns a set of outputs, each associated with a probability:
JK : N ⇀ N ⇝
JℛK : N → DN.
In this way, algorithms have enabled eficient solutions to numerous problems [
The last decade has witnessed a tremendous growth in the area of randomized
algorithms. During this period, randomized algorithms went from being a tool in
computational number theory to finding widespread applications in many types of
algorithms. Two benefits of randomization have spearheaded this growth: simplicity
and speed. [15, p. ix]
Reasoning About Uncertainty. In particular, the use of randomized models have spread in
discipline involving uncertain domain – that is, in all disciplines realistically interacting with
“the world”. For instance, in agent systems (whether artificial or not) reasoning is processed and
decisions are made on the ground of partial information obtained from the environment and the
background knowledge.1 Clearly, in such contexts, simplifications are needed and “probabilistic
thinking” appears as a formidable tool for decision making and learning processing [
Because many artificial intelligence applications require the ability to reason with
uncertain knowledge, it is important to seek appropriate generalizations of logic
from this case. [22, p. 71]
In the following years, new probability logics, inspired by [
As anticipated, interchanges between logic and computation are numerous and well-studied. Yet, in the randomized setting, such a deep correspondence has only been sparsely investigated. One crucial peculiarity, when switching to probabilistic algorithms, is that, in this case, behavioral properties, like termination or equivalence, have an inherently quantitative nature, that is a computation terminates with a given probability and a program might simulate a desired function up to some probability of error – think, for instance, to probabilistic primality tests or learning algorithms. Then, the central question is:
can such quantitative properties be studied within a logical system? In my Ph.D. dissertation a positive answer is given, at least for the specific aspects of the interaction between quantitative logics and randomized computation it focusses on. As we shall briefly see, the turning point of our approach consists in considering new quantitative logics able to express probability in a natural way.
Concretely, we generalized a few standard results linking logic and computation to the probabilistic realm.
Complexity Theory. As it is well-known, classical propositional logic and computational
complexity are strongly connected. Indeed, checking the satisfiability of PL-formulas is the
paradigmatic NP-complete problem [
Programming Language Theory. Traditionally, the Curry-Howard correspondence (CHC,
for short) relates intuitionistic PL and the simply-typed -calculus, but in the last fifty years
this correspondence was shown to hold in other and more sophisticated contexts too.
Meanwhile, randomized -calculi [
Arithmetic and Computation Theory. The theory of (deterministic) computation and
arithmetic are linked by deep results coming from logic and recursion theory – for example,
Gödel’s arithmetization [
probabilisitic computation : ?
⇐⇒
In the third part of the dissertation, we present a quantitative extension of the language of
PA, called MQPA, which allows us to formalize basic results from probability theory that are
not expressible in PA, for example the so-called infinite monkey theorem or the random walk
theorem. This language is also proved to be actually connected to randomized computation as
we establish the first probabilistic version of Gödel’s arithmetization [
In addition, this language is at the basis of our study of randomized bounded theories [
probabilistic classes : ?
⇐⇒
Inspired by the language MQPA, in the third part of the thesis we also introduce a randomized
bounded theory, called RS12, enabling us to logically capture relevant probabilistic classes, as
BPP [
Counting quantifiers are quantifiers of the form C or D and capable of expressing probabilities within a logical language. These quantifiers not only determine the existence of a satisfying assignment, but rather count how many those assignments are. In this sense, counting quantifiers can be seen as a quantitative generalization of standard propositional ones: (∀), (∃) ⇝
C , D .
Intuitively, the QPL-formula (∃) says that there is an interpretation for making true. On the other hand, the (pseudo-)counting formula C1/2 expresses that has probability greater than 12 of being true, i.e. that is true for at least one half of all possible interpretations of . Dually, D1/2 says that the argument formula has probability strictly smaller than 12 of being true.
Remarkably such a generalization is made possible by switching from a truth-functional to a quantitative semantics, in which formulas are no more interpreted as single truth-values but as measurable sets of models:
J KQPL ∈ {0, 1} ⇝
J KCPL ⊆ 2N.
So, while (the truth of) an existentially-quantified formula of QPL – for instance, (∃)(∃ )( ∧ ) – gives us information about the existence of a model for ∧ , counting-quantified formulas tell us something about the number of these satisfying valuations. For example, the (pseudo)counting formula C1/,4 ( ∧ ) says not only that there is a model for ∧ , but also that at least one out of four possible interpretations of the argument formula is a satisfying one. It is in this way that counting logical systems allow us to formally represent and study quantitative aspects of probabilistic computation in an innovative way.
Notably, our counting propositional logics are natural tools to represent stochastic events in
a straightforward way,3 but, as predictable, their expressive power is still quite limited. This
has led us to the generalization of the notion of counting quantifier and to the definition of the
extended language MQPA, which is nothing but the language of first-order arithmetic endowed
with second-order measure quantifiers and associated with a Borel semantics.
3For further details, see [
The Ph.D. dissertation Towards a Logical Foundation of Randomized Computation [
In Section B.1, we introduce a few standard notions from basic probability theory which are needed to define the semantics of our counting and measure-quantified logics. In Section B.2, we present the language and semantics of univariate CPL0 and of multivariate CPL, while, in Section B.3, we deal with the language and semantics of the more expressive language MQPA.
In probability theory, an outcome or point is the result of a single execution of an experiment, the sample space Ω is the set of all possible outcomes, and an event is a subset of Ω. Two events, say 1 and 2, are disjoint or mutually exclusive when they cannot happen at the same time, that is 1 ∩ 2 = ∅. A class Fof subsets of Ω is said to be a -field or -algebra when (i.) it contains Ω, i.e. Ω ∈ F, (ii) it is closed under complementation, i.e. if ∈ F, then ∈ F, being the complementation of , and (iii) it is closed under countable union (and intersection). The largest -field on Ω is the power class 2Ω, while the smallest one is {∅, Ω}. The -field generated by F, (F), is the smallest -algebra containing F. A measurable space is a pair (Ω, F), where F is a -algebra over Ω.
In the 1930s, Kolmogorov introduced the notion of probability space, together with the axioms for probability. A probability measure on a -field F, Prob(· ), associates each event ∈ F with a number, Prob(), so that: i. for each ∈ F, 0 ≤ Prob() ≤ 1, ii. Prob(∅) = 0 and Prob(Ω) = 1, iii. if 1, 2, ... ∈ F is a sequence of disjoint events, then Prob(︀ ⋃︀∞=1 )︀ = ∑︀∞=1 Prob(). Two events are (stochastically) independent when the occurrence of one does not afect the probability for the other to occur. In particular, given two disjoint events, say 1 and 2, Prob(1 ∪ 2) = Prob(1) + Prob(2), while for two independent events, say 1′ and 2′, Prob(1′ ∩ 2′) = Prob(1′) · Prob(2′). A probability space (Ω, F, Prob) is a mathematical object that provides a formal model for random processes and is made of: • a sample space, Ω, which is the set of all possible outcomes, • a -field , F, which is the set of events, • a probability measure, Prob, which assigns to each event in F a probability, i.e. a number between 0 and 1 satisfying the so-called Kolmogorov axioms.
In the following, we will mostly focus on a specific probability space such that Ω = 2N, namely the set of all infinite sequences of random bits (i.e. coin tosses). Each such sequence is denoted as
= (1)(2) . . . , with ∈ Ω, ∈ N, and () ∈ {0, 1}. Each sequence can be interpreted as the result of infinitely flipping a coin. Definition 1 (Cylinder of Rank ). A cylinder of rank is a set of the form
cyl = { | (1), ..., () ∈ }, with ⊂ { 0, 1}.
Observe that when = {(1, ..., )} is a singleton (︀ for 1, ..., ∈ {0, 1})︀ , an event = { | (1), ..., () = (1, ..., )}, such that the first repetitions of the experiment have outcomes 1, ..., in sequence, is called a thin cylinder. We will be particularly interested in thin cylinders in which the only set defining is made of one element = 1.
Notation 1. For ∈ N, we denote special thin cylinders as follows:
() = { | () = 1}.
The class of cylinders of all ranks, which is a field [ 42, pp. 27-30], is denoted by C, while ( C) indicates the -algebra generated by C. It is thus possible to define a measure on it. Specifically, we use C to denote the unique probability measure over (︀ 2N, ( C))︀ , such that for any ∈ N, C(︀ ())︀ = 21 .
Definition 2 (Canonical Cylinder Measure C). Given ∈ {0, 1}, let denote the (non-negative and summing to 1) probability of getting . Then, for any cylinder cyl , C(cyl ) = ∑︁ 1 · · · , the sum extending over all sequences (1, . . . , ) ∈ .
The core idea to define counting propositional logics is to extend standard languages by measure-sensitive quantifiers and to consider quantitative semantics in which formulas are no more interpreted as single truth values, but as measurable sets of satisfying valuations. When dealing with the most intuitive, univariate fragment CPL0, any formula, say , is interpreted as the set J K ⊆ 2N made of all maps ∈ 2N “making true” (︀ and belonging to the standard Borel algebra over 2N, B(2N))︀ . In particular, atomic propositions are interpreted as special cylinder sets of the form:
() = { ∈ 2N | () = 1},
for ∈ N, while non-atomic expressions are interpreted as standard operations of complementation, finite
intersection and union. Since these sets are all measurable, and B(2N) is endowed with a canonical probability measure,
it makes sense to ask whether “ is true with probability at least q” or “ is true with probability strictly smaller
than q”. This is formalized by the notion of counting quantifier – i.e. by C or D, for ∈ Q ∩ [
Definition 3 (Formulas of CPL0). Formulas of CPL0 are defined by the grammar below:
::= i | ¬ | ∧ | ∨ | C | D,
where ∈ N and ∈ Q ∩ [
The definition of the semantics of CPL0 relies on the standard cylinder space (︀ 2N, ( C), C︀) . Definition 4 (Semantics of CPL0). For each formula of CPL0 its interpretation J K ∈ B(2N) is the measurable set defined as follows: i := ()
J K
J¬K := 2N − JK J ∧ K := JK ∩ JK J ∨ K := JK ∪ JK
J C :=
K J D :=
K {︃2N ∅ if C(︀ JK) ≥ otherwise if C(︀ JK) < otherwise.
Definition 5.
J K = ∅. hEaxvaembpolthe 1m. eLaseut rues 14coannsdidaerreCdi1s/jo2i(nt.∨Hen)c,ew, heCr︀(eJ =∨ 0K∧)︀ ¬= 1 aCn︀( dJK=)︀+¬ 0C∧(︀ 1J.TKh)︀e=m12e,aasnudraJbCle1s/e2t(s,J∨ Ka)nKd=J2NK,.
Observe that counting quantifiers are inter-definable but not dual, in the sense of standard modal operators: C is not equivalent to ¬D¬ .
For any formula of CPL0, call it , is said to be valid when J K = 2N and to be invalid when
Remark 2. By combining counting quantifiers it is possible to easily express that a formula “is true with precisely
a given probability”, see [
B.2.2. Syntax and Semantics of CPL We now introduce the more expressive fragment CPL, in which relations between valuations of diferent groups of variables can be considered. Its language is made of named atomic formulas and named counting quantifiers. The corresponding quantitative semantics is subtler than the one for CPL0 and, in particular, the interpretation of counting-quantified formulas relies on some technical notions.
Notation 2. We use , , ... ∈ A for names and , ... ⊆
Intuitively, named counting quantifiers,
C or D, count the number of valuations of propositional atoms with the corresponding name, here , satisfying the argument formula.
Definition 6 (Formulas of CPL). Formulas of CPL are defined by the grammar below:
::= i | ¬ | ∧ | ∨ | C | D,
where ∈ N, ∈ A, and ∈ Q ∩ [
A named quantifier binds the occurrences of the name in the argument formula and counts models relative to the corresponding bounded variable. The intuitive meaning of C is that is true in at least valuations of the variables with name . technical notion of -projection.
The interpretation of a formula now depends on the choice of a finite set of names ⊇ measurable set J K belonging to the Borel algebra, B︀( (2N) )︀ . To define it formally we need to introduce the FN( ) and is a the -projection of is the set: Definition 7 ( -projection). Let , be two disjoint, finite sets of names, and ∈ (2N) . For all ⊆ (2N)∪ , where Π ( ) := {︀ ∈ (2N) | + ∈ ⊆ (2N) ,
︀} ( + )( ) := {︃ ( ) if ∈ ( ) if ∈ . interpretation J K ⊆ (2N) is defined as follows: Definition 8 (Semantics of CPL). For each formula of CPL and finite set of names such that ⊇ FN( ), the JiK := { | ()() = 1
} J ∧ K := JK ∩ JK J ∨ K := JK ∪ JK
J¬K := (2N) −
J K JDK := {︀ | C(︀ JK∪{}) JCK := {︀ | C(︀ Π (J K∪{})︀) ≥
︀} ︀) < ︀} .
to be true Example 2. Let us consider the formula C1/2
C1/2 , where = (︀ 2 ∧ (¬2 ∧ 3))︀ ∨ ︀( ¬2 ∧ (2 ∧ ¬3))︀ ∨ ︀( (¬2 ∧ 3) ∧ 3)︀ . variables satisfying in at least half of the cases. Let us list all possible cases: The valuations ∈ (2N){} belonging to
J
C1/2 K{} are those which can be extended to valuations of all Boolean 2. ()(2) = 1, ()(3) = 0. Then, has 12 chances of being true, as ¬2 has to be true 1. ()(2) = ()(3) = 1. Then, has 14 chances of being true, as both ¬2 and 3 have to be true 3. ()(2) = 0 and ()(3) = 1. Then, has 34 chances of being true, as either 2 or both ¬2 and 3 have 4. ()(2) = ()(3) = 0. Then, has no chance of being true.
Clearly, C1/2 K{} only contains the valuations which agree with cases 2. and 3. Therefore, qC1/2
J i.e. C
C1/2 is valid, since half of the valuations of has at least 21 chances of being extended to a model of . C1/2 y
= 2N, ∅ The standard model N = (N, +, × ) has nothing probabilistic in itself. To obtain a model for MQPA we extend it to a probability space, obtaining P = (N, +, × , ( C), C). The grammar for terms of MQPA is standard, whereas the syntax for formulas is obtained by endowing the language of PA with special flipcoin formulas of the form Flip() and measure-quantified formulas , such as C/ and D/ . Specifically, Flip(· ) is a special unary predicate with an intuitive computational meaning: it provides an infinite sequence of independently and randomly distributed bits. Given a closed term , Flip() holds if and only if the -th tossing returns 1, where denotes + 1. Definition 9 (Terms and Formulas of MQPA). Let be a denumerable set of ground variables, whose elements are indicated by metavariables such as , , .... The terms of MQPA, denoted by , , ..., are defined by the grammar below:
::= Flip() | ( = ) | ¬ | ∨ | ∧ | ∃. | ∀. | C/ | D/. Given an environment : → N, the interpretation of a term is defined as usual. Instead, the interpretation
J K of formulas requires a little care, being it inherently quantitative; indeed, any formula of MQPA, say , is associated with a measurable set, J K ∈ ( C).
Definition 10 (Semantics for Formulas of MQPA). Given a formula and an environment , the interpretation of in , J K ∈ ( C), is the measurable set of sequences inductively defined as follows:
JFlip()K := {︀ | (︀ JK ︀) = 1}︀
{︃2N
∅ J¬K := 2N − JK ∅ if JK > 0 and C(JK ) ≥ JK /JK otherwise if JK = 0 or C(JK ) < JK /JK otherwise