1 Introduction
Among the features historically defining standard computational models there is certainly determinism: given an algorithm and input, the sequence of computation steps is uniquely determined. In the XX century, this assumption started to be relaxed in different 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 different outcomes, each associated with a certain probability.
This more flexible design makes probabilistic models very efficient and powerful tools [33], with several applications in computer science (CS) and technology. Generally speaking, these are often crucial when dealing with uncertain information or partial knowledge, namely for all systems acting in realistic contexts, think for examples of driverless cars [40] or of computer vision modelling [29]. Notably, in some areas probabilistic models have become even more than optional; for instance in cryptography, where secure encryption schemas are probabilistic [25].
Anzeige
1.1 The Dissertation
In this context, my Ph.D. dissertation was driven by two main considerations. On the one hand, since their appearance in the 1950s, probabilistic computational models have become ubiquitous in several fast-growing areas of CS, and, by now, related, abstract machines—as probabilistic Turing machines (PTMs) [19, 22, 36], stochastic automata [13, 18, 34] or randomized \(\lambda\)-calculi [28, 35]—have been massively studied in the literature. On the other, there exist deep and mutual interactions linking logic and theoretical computer science (TCS) and, in the past, the development of computational models and theory has considerably benefitted from them. Surprisingly, 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 probabilistic algorithms in many relevant fields of IT, from AI to statistical learning, from cryptography to approximate computing and robotics.
The global purpose of my doctoral thesis consisted in laying the foundation for a uniform approach to bridge the mentioned gap. To do so, the key ingredient is the introduction of a family of new logics, whose language includes non-standard quantifiers “measuring” the probability for the corresponding argument formula to be true and associated with inherently quantitative semantics.1
Concretely, the dissertation is tripartite. The first part focusses on the relation between logic and counting complexity, and its main result consists in showing that classical counting propositional logic provides a purely logical characterization of Wagner’s hierarchy [43]. The second part of the thesis deals with programming language theory. Here, the Curry–Howard correspondence (CHC) [38] is extended for the first time to the probabilistic setting by relating the intuitionistic version of our counting logic and a counting-typed probabilistic \(\lambda\)-calculus. Finally, we consider the link between arithmetic and computation by introducing a quantitative extension of the language of Peano arithmetic (\(\textsf{\textbf{PA}}\)) able to formalize basic results from probability theory. This language is also our starting point to define randomized bounded arithmetic and to generalize canonical results by Buss [12].
2 Relating Logic and Randomized Computation
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, defining 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—such as programming language theory [38], verification [39] and database theory [15], computational and descriptive complexity [16], just to name a few - have effectively taken advantages from this mutual dialogue. As Siekmann wrote, “[i]n many respects, logic provides computer science with both a unifying foundational framework and a tool for modeling” [37, 14, 16, 27, 41], and by the numerous concrete exchanges between these disciplines: while the growing importance of IT has guided and stimulated advances in logic, logical tools have extensive applications in CS and technology.
Anzeige
On the other hand, when switching to the randomized setting, such a deep correspondence has been investigated only sparsely. One crucial peculiarity of dealing with probabilistic algorithms is that, in this case, behavioral properties, like termination or equivalence, have an inherently quantitative nature, that is a computation terminates with (at least or at most) a given probability, and a program might simulate a 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? My Ph.D. dissertation offers a positive answer at least to the specific aspects of the interaction between quantitative logics and randomized computation it focusses on.
2.1 Counting Complexity Theory
As it is well-known, classical propositional logic and computational complexity are strongly connected. Indeed, checking the satisfiability of \(\textsf{\textbf{PL}}\)-formulas is the paradigmatic \({\textbf{N}}{\textbf{P}}\)-complete problem [16], while the language of classical tautologies is \(\textbf{coNP}\)-complete. In the early 1970s, Meyer and Stockmeyer also showed that, when switching to quantified propositional logic (\({{{{{\textsf {QPL}}}}}}\)), the full polynomial hierarchy can be captured by a single logical system, and that each level in it is characterized by the validity of \({{{{{\textsf {QPL}}}}}}\)-formulas (in PNF), with the corresponding number of quantifier alternations [31, 32]. Nonetheless, when moving to the probabilistic framework, such a plain correspondence seems lost, since no analogous logical counterpart is known to relate in a similar way to the counting classes and hierarchy, introduced by Valiant [42] and Wagner [43]:In the first part of the dissertation, a counting propositional system, called \({{{{{\textsf {CPL}}}}}}\), is introduced. This logic is a generalization of \(\textsf{\textbf{PL}}\) able to express that a formula is true with (at least or at most) a given probability [1, 9]. \({{{{{\textsf {CPL}}}}}}\) is shown to be strongly related to counting computation and classes, being the probabilistic counterpart of \({{{{{\textsf {QPL}}}}}}\) [6, 9, 10]. Indeed, its counting quantifiers can be naturally seen as “quantitative” versions of standard propositional ones, and our main result here is the purely logical characterization of Wagner’s hierarchy via complete problems defined in terms of \({{{{{\textsf {CPL}}}}}}\)-formulas.
$$\begin{aligned} \text {polynomial hierarchy} : {{{{{\textsf {QPL}}}}}}\; \Leftrightarrow \; \text {counting hierarchy} : \; ? \end{aligned}$$
2.2 Programming Language Theory
Traditionally, CHC relates intuitionistic \(\textsf{\textbf{PL}}\) and the simply-typed \(\lambda\)-calculus [38], but in the last fifty years it was shown to hold in other, more sophisticated contexts too. Meanwhile, randomized \(\lambda\)-calculi [35] and associated type systems, sometimes also guaranteeing desirable forms of termination [20], were introduced. Yet, these were not designed having a logical system in mind, and no (probabilistic) CHC is known for them:In the second part of the thesis, two new systems are introduced to define the first probabilistic version of the above correspondence. On the one hand, we consider the intuitionistic counterpart of univariate \({{{{{\textsf {CPL}}}}}}\), called \({{{{{\textsf {iCPL}}}}}}_0\), and show it able to capture quantitative behavioral properties. On the other, we define a “counting-typed” probabilistic \(\lambda\)-calculus. Its untyped part is strongly inspired by the probabilistic event \(\lambda\)-calculus presented in [17], while the type system is defined mimicking counting quantifiers. Finally, we establish a (static and dynamic) correspondence, in the style of Curry and Howard, between these two systems [8, 10].
$$\begin{aligned} \text {simply typed } \lambda _\rightarrow : {{{{{\textsf {iPL}}}}}} \; \Leftrightarrow \; \text {randomized } \lambda \text {-calculi} : \; ? \end{aligned}$$
2.3 Probabilistic (Bounded) Arithmetic
2.3.1 Arithmetic and Computation Theory
The theory of (deterministic) computation and arithmetic are linked by deep results coming from logic and recursion theory, such as Gödel’s arithmetization [23], or realizability [30], or the Dialectica interpretation [24]. Many interesting properties of algorithms can be expressed in the arithmetical language, and, due to the relation between totality (of functions) and termination (of algorithms), several issues in computation theory can be analyzed in the framework of arithmetic. Also in this context, when considering the probabilistic realm, there is no theory relating to randomized computation as \(\textsf{\textbf{PA}}\) does to deterministic one:In the third part of the dissertation, we present a quantitative extension of the language of arithmetic, called \({{{{\textsf {MQPA}}}}}\), which allows us to formalize basic results from probability theory that are not expressible in \(\textsf{\textbf{PA}}\), for example the so-called infinite monkey theorem. This language is also proved to be actually connected to randomized computation as we establish the probabilistic version of Gödel’s arithmetization [17], namely it is shown that any random function can be expressed by a formula of \({{{{\textsf {MQPA}}}}}\).
$$\begin{aligned} \text {det. comput.} : {{{{{\textsf {P}}}}}{} {\textbf {A}}}\; \Leftrightarrow \; \text {prob. comput.} : \; ? \end{aligned}$$
2.3.2 Bounded Arithmetic and Probabilistic Complexity
In addition, the language of \({{{{\textsf {MQPA}}}}}\) is at the basis of our study of randomized bounded arithmetic theories. Historically, one of the main motivations for the development of bounded arithmetics (i.e. subsystems of \(\textsf{\textbf{PA}}\) whose language includes symbols for functions with specific growth rate together with bounded quantifiers, and in which induction is variously limited) was their connection with computational complexity [12]. As it is clear that not all computable functions are feasibly computable, bounded theories have become essential to characterize interesting (feasible) complexity classes in terms of families of arithmetic formulas. Specifically, in 1986, Buss proved that the class of poly-time computable functions precisely corresponds to that of functions which are \(\Sigma ^b_1\)-definable in a given bounded theory, \({{{{{\textsf {S}}}}}}^1_2\). Although this fact is very insightful, no similar result was established in the probabilistic framework:Inspired by \({{{{\textsf {MQPA}}}}}\), in the third part of the thesis we introduce a randomized bounded theory, called \({{{{{\textsf {RS}}}}}}^1_2\), enabling us to logically capture relevant probabilistic classes, as \(\textbf{BPP}\)2 [3‐5].
$$\begin{aligned} \text {deterministic classes } : \text {BA} \; \Leftrightarrow \; \text {probabilistic classes} : \; ? \end{aligned}$$
3 From Evaluating to Measuring
Counting quantifiers are quantifiers of the form \(\textbf{C}^q\) or \(\textbf{D}^q\) (for \(q\in {\mathbb {Q}}\cap [0,1]\)) and capable of expressing probabilities within a logical language. Intuitively, a counting quantified formula \(\textbf{C}^q F\) expresses that F is true with probability greater than or equal to q, while \(\textbf{D}^qF\) expresses that F has probability strictly smaller than q of being true. Thus, these quantifiers not only determine the existence of a satisfying assignment, but also count how many those assignments are. In a sense, they are quantitative generalizations of standard propositional ones. Accordingly, we move from a standard language made of formulas of the form \((\forall X)F,(\exists X)F\) to that of counting quantified ones, \(\textbf{C}^q F,\textbf{D}^q F\).
Such a generalization is possible only when contextually switching from a truth-functional (i.e. \(\llbracket F\rrbracket _{{{{{{\textsf {QPL}}}}}}} \in \{0,1\}\)) to a quantitative semantics, in which formulas are no more interpreted as single truth-values but as measurable sets of models (i.e. \(\llbracket F\rrbracket _{{{{{{\textsf {CPL}}}}}}_0} \subseteq 2^{\mathbb {N}}\)). So, while (the truth of) an existentially quantified formula of \({{{{{\textsf {QPL}}}}}}\), for instance, \((\exists X)(\exists Y)(X\wedge Y)\), gives us information about the existence of a model for \(X\wedge Y\), counting quantified formulas tell us something about the number of these satisfying valuations.
Example 1
The (pseudo-)counting formula \(\textbf{C}^{1/4}(X\wedge Y)\) says not only that there is a model for \(X\wedge Y\), but also that at least one out of four possible interpretations of the argument formula is a satisfying one.
In this way, such logic allows 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 [1], but, as predictable, their expressive power is quite limited. So, as anticipated, we have generalized the notion of counting quantifier to define the extended language \({{{{\textsf {MQPA}}}}}\), which is nothing but the language of first-order arithmetic endowed with second-order measure quantifiers and associated with a Borel semantics.
3.1 On Counting Propositional Logic
In order to make these intuitive notions clearer we briefly introduce the univariate fragment \({{{{{\textsf {CPL}}}}}}_0\). Although the expressive power of this logic is limited, its semantics has a very natural interpretation and can be extended to full \({{{{{\textsf {CPL}}}}}}\) in a straightforward way.
When dealing with \({{{{{\textsf {CPL}}}}}}_0\), any formula, say F, is interpreted as the set \(\llbracket F\rrbracket \subseteq 2^{\mathbb {N}}\) made of all maps \(f\in 2^{\mathbb {N}}\) “making F true” (and belonging to the standard Borel algebra over 2\(^{\mathbb {N}}\), \({\mathscr {B}}(2^{\mathbb {N}})\)). In particular, atomic propositions are interpreted as special cylinder sets [11] of the form \(Cyl(i)=\{f\in 2^{\mathbb {N}}\; | \; f(i)=1\}\) (for \(i\in {\mathbb {N}}\)), while non-atomic expressions are interpreted as standard operations of complementation, finite intersection and union. Since these sets are all measurable, and \({\mathscr {B}}(2^{\mathbb {N}})\) is endowed with a canonical probability measure, it makes sense to ask whether “F is true with probability at least q” or “F is true with probability strictly smaller than q”. This is formalized by the notion of counting quantifier, i.e. by \(\textbf{C}^q\) and \(\textbf{D}^q\) for \(q\in {\mathbb {Q}} \cap [0,1]\).3 As seen, the formula \(\textbf{C}^qF\) (resp., \(\textbf{D}^qF\)) intuitively expresses that F is satisfied by a portion of assignments greater (resp., strictly smaller) than q. For example, \(\textbf{C}^{1/2}F\) expresses that F is satisfied by at least half of its valuations.
A bit more formally,
Definition 1
(Formulas of \({{{{{\textsf {CPL}}}}}}_0\)) Formulas of \({{{{{\textsf {CPL}}}}}}_0\) are defined by the grammar below,where \(i\in {\mathbb {N}}\) and \(q\in {\mathbb {Q}}\cap [0,1]\).
$$\begin{aligned} F \; {:}{:}{=} \; \textbf{i} \; | \lnot F \; | \; F \wedge F \; | \; F \vee F \; | \; \textbf{C}^q F \; | \; \textbf{D}^q F, \end{aligned}$$
The definition of the semantics for \({{{{{\textsf {CPL}}}}}}_0\) relies on the standard cylinder space \(\big (2^{\mathbb {N}}, \sigma ({\mathscr {C}}), \mu _{{\mathscr {C}}}\big )\).4 x
Definition 2
(Semantics of \({{{{{\textsf {CPL}}}}}}_0\)) For each formula F of \({{{{{\textsf {CPL}}}}}}_0\) its interpretation, \(\llbracket F\rrbracket \in {\mathscr {B}}(2^{\mathbb {N}})\), is the measurable set:
$$\begin{aligned} \llbracket \textbf{i} \rrbracket&:= Cyl(i) \\ \llbracket \lnot G\rrbracket&:= 2^{\mathbb {N}}- \llbracket G\rrbracket \\ \llbracket G \wedge H\rrbracket&:= \llbracket G\rrbracket \cap \llbracket H\rrbracket \\ \llbracket G \vee H\rrbracket&:= \llbracket G \rrbracket \cup \llbracket H\rrbracket \\ \llbracket \textbf{C}^qG\rrbracket&:= {\left\{ \begin{array}{ll} 2^{\mathbb {N}}&{}\text {if } \mu _{{\mathscr {C}}}(\llbracket G\rrbracket ) \ge q \\ \emptyset &{}\text {otherwise} \end{array}\right. } \\ \llbracket \textbf{D}^q G\rrbracket&:= {\left\{ \begin{array}{ll} 2^{\mathbb {N}}&{}\text {if } \mu _{{\mathscr {C}}}(\llbracket G\rrbracket ) < q \\ \emptyset &{}\text {otherwise.} \end{array}\right. } \end{aligned}$$
Example 2
Let \(\textbf{C}^{1/2}(F\vee G)\), where \(F=\textbf{0} \wedge \lnot \textbf{1}\) and \(G=\lnot \textbf{0} \wedge \textbf{1}\). The measurable sets \(\llbracket F\rrbracket\) and \(\llbracket G\rrbracket\) have both measure \(\frac{1}{4}\) and are disjoint. Hence, \(\mu _{{\mathscr {C}}}(\llbracket F\vee G\rrbracket )\) = \(\mu _{{\mathscr {C}}}(\llbracket F\rrbracket ) + \mu _{{\mathscr {C}}}(\llbracket G\rrbracket )\) = \(\frac{1}{2}\) and \(\llbracket \textbf{C}^{1/2}(F\vee G)\rrbracket = 2^{\mathbb {N}}\).
Observe that counting quantifiers are inter-definable (as \(\textbf{C}^q F \equiv \lnot \textbf{D}^qF\)) but not dual in the sense of standard modal operators: \(\textbf{C}^q F\) is not equivalent to \(\lnot \textbf{D}^q\lnot F\).
In more expressive \({{{{{\textsf {CPL}}}}}}\), relations between valuations of different groups of variables can be taken into account. Contextually, the corresponding quantitative semantics is subtler than that of \({{{{{\textsf {CPL}}}}}}_0\), and to define the interpretation for counting quantified formulas we rely on a few technical notions.5 Remarkably, there is a strong connection between (closed) formulas of \({{{{{\textsf {CPL}}}}}}_0\) and (closed) formulas of \({{{{{\textsf {CPL}}}}}}\) in which only one name occurs.6 Moreover, in [6, 9, 10], sound and complete proof system(s) for \({{{{{\textsf {CPL}}}}}}_0\) and \({{{{{\textsf {CPL}}}}}}\) have also been introduced.
3.2 On Measure-Quantified Peano Arithmetic
The standard model \({\mathscr {N}}=({\mathbb {N}}, +, \times )\) has nothing probabilistic in itself. So, to define a model for \({{{{\textsf {MQPA}}}}}\) we extend it to a probability space, obtaining \({\mathscr {P}} = ({\mathbb {N}}, +, \times , \sigma ({\mathscr {C}}), \mu _{{\mathscr {C}}})\). The grammar for terms of \({{{{\textsf {MQPA}}}}}\) is standard, while that for formulas is obtained by endowing the language of \(\textsf{\textbf{PA}}\) with special flipcoin formulas of the form \(\textsc {Flip}(t)\) and measure-quantified formulas, namely, \(\textbf{C}^{t/s}F\) and \(\textbf{D}^{t/s}F\) (where, now, t and s are terms, possibly including variables). Specifically, \(\textsc {Flip}(\cdot )\) is a special unary predicate with an intuitive computational meaning: it provides an infinite sequence of independently and identically distributed bits. Given a closed term t, \(\textsc {Flip}(t)\) holds when the n-th tossing returns 1, and n is \(t+1\).
Definition 3
(Terms and Formulas of \({{{{\textsf {MQPA}}}}}\)) Let \({\mathcal {G}}\) be a denumerable set of ground variables, whose elements are indicated by metavariables \(x,y,\dots\). The terms of \({{{{\textsf {MQPA}}}}}\), denoted by \(t,s,\dots\), are defined by the grammar below:The syntax for formulas of \({{{{\textsf {MQPA}}}}}\) is as follows:for \(*\in \{\vee ,\wedge \}\) and \(\blacksquare \in \{\textbf{C}^{t/s}, \textbf{D}^{t/s}\}\).
$$\begin{aligned} t {:}{:}{=} x \; | \; \texttt{0} \; | \; \texttt{S}(t) \; | \; t+s \; | \; t\times s. \end{aligned}$$
$$\begin{aligned} F {:}{:}{=}&\; \textsc {Flip}(t) \; | \; t=s \; | \; \lnot F \; | \; F * G \; | \; \exists x .F \; | \; \forall x.F \; | \; \blacksquare F, \end{aligned}$$
Given an environment \(\xi : {\mathcal {G}} \rightarrow {\mathbb {N}}\), the interpretation for a term t, \(\llbracket t\rrbracket _\xi\), is defined as usual. Instead, that of formulas is not, being it inherently quantitative.
Definition 4
(Semantics for Formulas of \({{{{\textsf {MQPA}}}}}\)) Given a formula F and an environment \(\xi\), the interpretation of F in \(\xi\), \(\llbracket F\rrbracket _\xi \in \sigma ({\mathscr {C}})\), is the measurable set of sequences inductively defined as follows:
$$\begin{aligned} \llbracket \textsc {Flip}(t) \rrbracket _{\xi }&:= \{\omega \; | \; \omega (\llbracket t\rrbracket _\xi ) = 1\} \\ \llbracket t=s\rrbracket _\xi&:= {\left\{ \begin{array}{ll} 2^{\mathbb {N}}&{}\text {if } \llbracket t\rrbracket _\xi = \llbracket s\rrbracket _\xi \\ \emptyset &{}\text {otherwise} \end{array}\right. } \\ \llbracket \lnot G\rrbracket _\xi&:= 2^{\mathbb {N}}- \llbracket G\rrbracket _\xi \\ \llbracket G\vee H\rrbracket _\xi&:= \llbracket G\rrbracket _\xi \cup \llbracket H\rrbracket _\xi \\ \llbracket G \wedge H\rrbracket _\xi&:= \llbracket G\rrbracket _\xi \cap \llbracket H\rrbracket _\xi \\ \llbracket \exists x.G\rrbracket _\xi&:= \bigcup _{i\in {\mathbb {N}}} \llbracket G\rrbracket _{\xi \{x\leftarrow i\}} \\ \llbracket \forall x.G\rrbracket _\xi&:= \bigcap _{i\in {\mathbb {N}}} \llbracket G\rrbracket _{\xi \{x\leftarrow i\}} \\\quad \llbracket \textbf{C}^{t/s}G\rrbracket _\xi&:= {\left\{ \begin{array}{ll} 2^{\mathbb {N}}&{}\text {if } \llbracket s\rrbracket _\xi >0 \text { and } \mu _{{\mathscr {C}}}(\llbracket G\rrbracket ) \ge \llbracket t\rrbracket _\xi / \llbracket s\rrbracket _\xi \\ \emptyset &{}\text {otherwise} \end{array}\right. } \\ \quad \quad \llbracket \textbf{D}^{t/s} G\rrbracket _\xi&:= {\left\{ \begin{array}{ll} 2^{\mathbb {N}}&{}\text {if } \llbracket s \rrbracket _\xi = 0 \text { or } \mu _{{\mathscr {C}}}(\llbracket G\rrbracket _\xi ) < \llbracket t\rrbracket _\xi / \llbracket s\rrbracket _\xi \\ \emptyset &{}\text {otherwise.} \end{array}\right. } \end{aligned}$$
The semantics is well-defined as the sets \(\llbracket \textsc {Flip}(t)\rrbracket _\xi\) and \(\llbracket t=s\rrbracket _\xi\) are measurable, and measurability is preserved by all logical and counting operators. A formula of \({{{{\textsf {MQPA}}}}}\), say F, is said to be valid when, for every \(\xi\), \(\llbracket F\rrbracket _\xi = 2^{\mathbb {N}}\).
Example 3
The formula \(F=\textbf{C}^{1/1} \exists x.\textsc {Flip}(x)\) states that a true random bit will almost surely be met. The formula is valid as the set of constantly 0 sequences forms a singleton of measure 0.
4 Conclusion and Future Work
My Ph.D. thesis aims at being a first step to bridge logic and probabilistic computation. In it quantitative logical systems are developed to uniformly generalize standard achievements in TCS to the probabilistic setting. First, classical \({{{{{\textsf {CPL}}}}}}_0\) and \({{{{{\textsf {CPL}}}}}}\) are introduced and proved to be strongly connected to counting classes, as formulas of \({{{{{\textsf {CPL}}}}}}\) in a special prenex normal form provide complete problems for each level of Wagner’s hierarchy [6, Cor. 1].7 Then, the computational fragment of its intuitionistic version, \({{{{{\textsf {iCPL}}}}}}_0\), and the probabilistic CHC are defined: proofs in \({{{{{\textsf {iCPL}}}}}}_0\) correspond, in the sense of Curry and Howard, to typing derivations for the randomized \(\lambda\)-calculus \(\Lambda _{PE}\), so that counting quantifiers “reveal” the probability of termination of the underlying probabilistic program [8, Sec. 5].8 In addition, a quantitative extension of the language of \(\textsf{\textbf{PA}}\), able to formalize basic results from probability theory, which are not expressible in standard arithmetic, is presented together with the first randomized version of Gödel’s arithmetization [7, Th. 3].9 Finally, a randomized bounded theory á la Buss is defined such that bounded formulas provably total in it precisely capture poly-time random functions. Due to \(\textsf{\textbf{RS}}^1_2\), a new, syntactical characterization of \(\textbf{BPP}\) is obtained by internalizing the error-bound check within the logical system [5, Th. 15, 18].
To the best of my knowledge, the project and approach developed in the dissertation is quite new. Accordingly, several problems and challenges are still open. In general, the investigation of the expressive power of our logics (initiated in [1, Sect. 3]) and of their relation with probability and modal systems deserves further attention. About the proof theory of \({{{{{\textsf {CPL}}}}}}_0\) and \({{{{{\textsf {CPL}}}}}}\), the study of their dynamic (namely, the underlying cut-elimination procedure) and the introduction of a purely syntactical calculus have only been initiated.10 Also the introduction of intuitionistic logics and probabilistic CHC opens up several new avenues of research: from the extension of CHC to polymorphic types or to control operator to the study of intersection types to support program synthesis.
Concerning measure-quantified languages of arithmetic, one of the most compelling problems is the definition of a corresponding sound and sufficiently expressive proof system. Furthermore, as the language of \({{{{\textsf {MQPA}}}}}\) is somehow minimal “by design”, it would be natural to generalize its study to more expressive (named) fragments, following the path delineated by multivariate \({{{{{\textsf {CPL}}}}}}\). At the same time, the introduction of randomized bounded arithmetic could be the starting point for a long-term study on the logical nature of semantic classes and on its link with proof complexity, think for example of natural extensions of our approach to the characterization of other randomized classes, such as \(\textbf{ZPP}, {\textbf{R}}{\textbf{P}}\) and \(\textbf{coRP}\), or to its applications to the study of random resolution refutations.
Acknowledgements
I thank my Ph.D. thesis supervisor U. Dal Lago and co-supervisor P. Pistone for their constant guidance and crucial help: all the results presented in my dissertation are part of a joint work with them. I am grateful to the anonymous reviewers for their helpful comments.
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.