=Paper=
{{Paper
|id=Vol-3615/paper5
|storemode=property
|title=Towards a Logical Foundation of Randomized Computation
|pdfUrl=https://ceur-ws.org/Vol-3615/paper5.pdf
|volume=Vol-3615
|authors=Melissa Antonelli
|dblpUrl=https://dblp.org/rec/conf/beware/Antonelli23
}}
==Towards a Logical Foundation of Randomized Computation==
https://ceur-ws.org/Vol-3615/paper5.pdf
Towards a Logical Foundation of Randomized
Computation (Thesis Abstract)β
Melissa Antonelli1
1
HIIT Helsinki Institute for Information Technology, Pietari Kalmi katu, 5, 00560, Helsinki, Finland.
Abstract
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 Curry-
Howard 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].
Keywords
Randomized Computation, Logical Foundations of Computer Science, Probability Logic, Reasoning about
Uncertainty
1. Introduction
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 deter-
mined. In the second half of the XX century, this assumption started to be relaxed in different
ways and randomized algorithms were introduced for the first time β where a randomized algo-
rithm 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. Such a
more flexible design makes this computational model a very efficient 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
BEWARE 2023: Joint Workshop, AIxIA 2023, November 6-9, 2023, Rome, Italy,
β
The author thanks her Ph.D. thesis supervisor U. Dal Lago and co-supervisor P. Pistone for their constant guidance
and crucial help: all the results presented here are part of the joint work with them. The author is grateful to
Helsinki Institute for Information Technology - HIIT for supporting her work since 2023. Finally, the author wish
to thank the anonymous reviewers for helpful comments.
$ melissa.antonelli@helsinki.fi (M. Antonelli)
Β© 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
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 non-
standard quantifiers βmeasuringβ the probability of their argument formula, and associated with
inherently quantitative semantics.
2. The Importance of Being Randomized
As said, randomized algorithms are powerful tools with numerous applications in different
fields 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 [4] or of computer vision modelling [5]. Notably, in some areas
probabilistic models have become even more than optional; for instance in cryptography, where
secure encryption schemas are probabilistic [6].
On Logical Foundations of Computer Science. The existence of several and deep inter-
actions 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 [2], verification [7] and database theory [8], computational and
descriptive complexity [9, 10], just to quote a few β has effectively benefitted from their mutual
dialogue. As Siekmann wrote, β[i]n many respects, logic provides computer science with both a
unifying foundational framework and a tool for modelingβ [11, p. 17]. Indeed, several aspects
of computer science are intrinsically related with logic, as shown by a variety of seminal results,
e.g. [12, 13, 14, 9]. The other side of the coin is the existence of numerous concrete exchanges
between these disciplines: while the growing importance of IT has guided and stimulated
many advances in logic, logical tools have extensive applications in CS and technology β from
software and hardware verification to the modelling of interactive or multi-agent systems, from
the study of relational databases to argumentation theory.
Probabilistic Computation. Probabilistic computational models have been widely investi-
gated 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:
JπK : N β N β Jπβ K : N β DN .
In this way, algorithms have enabled efficient solutions to numerous problems [15], becoming
essential in different areas. As a consequence, several probabilistic (formal) models were
introduced: from PTMs [16, 17] and stochastic automata [18, 19] to probabilsitic π-calculi [20].
At this point, randomized algorithms and programs are widespread, steering disciplines like
robotics, AI, verification and security coding, computer vision and NLP:
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 [21]. These
new, concrete demands also led to the first attempts to analyze probabilistic reasoning in a
formal way and to the introduction of a few logical systems, starting in 1986 with Nilssonβs
pioneering proposal:
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 [22], were presented and developed
in the context of modal logic [23, 24, 25]. Nowadays, different formal systems to deal with
probabilistic and uncertain reasoning have been defined, even basing on alternative (non-
modal) approaches, for example via non-monotonic and fuzzy logics or due to direct numerical
representations.2
1
Probabilistic models become fundamental in AI research from the 1970s-1980s on. For further details on the βmain
phasesβ in the history of this discipline, see e.g. [5].
2
A detailed overview of logics for probability can be found e.g. in [21] or in [26, pp. 91ff.].
3. Towards Logical Foundations of Randomized Computation
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.
3.1. Relating Logic and Randomized Computation
Concretely, we generalized a few standard results linking logic and computation to the proba-
bilistic 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 [9], while the language of classical tautologies is coNP-
complete. In the early 1970s, Meyer and Stockmeyer also showed that, when switching to
quantified propositional logic (QPL, for short), the full polynomial hierarchy (PH, for short)
can be captured by a single logical system and that each level in it is characterized by the
validity of QPL-formulas (in PNF), with the corresponding number of quantifier alternations.
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, as introduced by Valiant [27] and Wagner [1]:
polynomial hierarchy : QPL ββ counting hierarchy : ?
In the first part of the dissertation, a counting propositional system, called CPL, is introduced.
This logic is basically a generalization of PL capable of expressing that a formula is true with a
given probability [28, 29]. Then, CPL is shown to be strongly related to counting computation
and classes, being the probabilistic counterpart of QPL [30, 28, 31]. Indeed, its counting
quantifiers can be naturally seen as βquantitativeβ versions of standard propositional ones.
Our main result here is the purely logical characterization of Wagnerβs hierarchy via complete
problems defined in terms of CPL-formulas.
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. Mean-
while, randomized π-calculi [20] and associated type systems were introduced, sometimes also
guaranteeing desirable forms of termination [32]. Yet, they are not so-to-say βlogically orientedβ
and no (probabilistic) CHC [2] is known for them:
simply typed πβ : intuitionistic PL ββ randomized π-calculi : ?
In the second part of the thesis, two new ingredients are introduced to define the first probabilistic
version of the quoted correspondence. On the one hand, we consider the intuitionistic version
of univariate CPL, called iCPL0 , and show it able to capture quantitative behavioral properties.
On the other, we define a βcountingβ-typed randomized π-calculus. Its untyped part is strongly
inspired by the probabilistic event π-calculus introduced in [33], while its types are defined
mimicking counting quantifiers. Finally, we establish a (static and dynamic) correspondence in
the style of Curry and Howard between these two systems [34, 31].
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 [35] or realizability [36] or the Dialectica interpretation [37]. Indeed,
the language of arithmetic is able to express many interesting properties of algorithms 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 switching to the probabilistic realm, no theory can be found to relate to randomized
computation as Peano Arithmetic (PA, for short) does in the deterministic case:
deterministic computation : PA ββ 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 [33], namely it is shown
that any random function can be expressed by a formula of MQPA.
In addition, this language is at the basis of our study of randomized bounded theories [38].
One of the central motivations for the development of bounded arithmetics β i.e., subsystems of
PA the language of which includes functions with specific growth rate together with bounded
quantifiers, and in which induction is (variously) limited β was their connection with compu-
tational complexity. As it is clear that not all computable functions are feasibly computable,
bounded theories become essential to characterize interesting (feasible) complexity classes
in terms of families of arithmetic formulas. Specifically, in 1986 Buss proved that poly-time
computable functions precisely correspond to those functions which are Ξ£π1 -definable in a
given bounded theory, called S12 [3]. Although this fact is very insightful, no similar result was
established in the probabilistic framework:
deterministic classes : BA ββ 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 [39, 40].
3.2. From Evaluating to Measuring
Counting quantifiers are quantifiers of the form Cππ or Dππ and capable of expressing prob-
abilities 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.
1/2
On the other hand, the (pseudo-)counting formula Cπ πΉ expresses that πΉ has probability
greater than 12 of being true, i.e. that πΉ is true for at least one half of all possible interpretations
1/2
of π. Dually, Dπ πΉ 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-
1/4
)counting formula Cπ,π (π β§ π ) 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.
References
[1] K. Wagner, The Complexity of Combinatorial Problems with Succinct Input Representation, Acta Informatica
23 (1986) 325β356.
[2] M. Sorensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, volume 149, Elsevier, 2006.
[3] S. Buss, Bounded Arithmetic, Ph.D. thesis, Princeton University, 1986.
[4] S. Thrun, W. Burgard, D. Fox, Probabilistic Robotics, MIT Press, 2006.
3
For further details, see [29].
[5] D. Koller, N. Friedman, Probabilistic Graphical Models: Principles and Techniques, MIT Press, 2009.
[6] S. Goldwasser, S. Micali, Probabilistic Encryption, Journal of Computer and System Sciences 28 (1984) 279β299.
[7] M. Thornton, R. Drechsler, D. Miller, Logic Verification, Springer, 2001, pp. 201β230.
[8] E. Codd, Relational Completeness of Data Base Sublanguages, in: Proc. 6th Courant Computer Science
Symposium, 1972, pp. 65β98.
[9] S. Cook, The Complexity of Theorem-Proving Procedures, in: Proc. Symposium on Theory of Computing
(STOC), 1971, pp. 151β158.
[10] N. Immerman, Descriptive Complexity, Springer, 1999.
[11] J. Siekman, Computational Logic, in: J. Siekmann (Ed.), Handbook of the History of Logic: Computational
Logic, volume 9, Elsavier, 2014, pp. 15β30.
[12] A. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem, in: Proc. London
Mathematical Society, volume 42, 1936, pp. 230β265.
[13] A. Church, S. Kleene, Formal Definitions in the Theory of Ordinal Numbers, Fundamenta Mathematicae 28
(1936) 11β21.
[14] W. Howard, The Formulae-as-Types Notion of Construction, in: J. Seldin, J. Hindley (Eds.), To H.B. Curry:
Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 479β490.
[15] R. Motwani, P. Raghavan, Randomized Algorithms, Cambridge University Press, 1995.
[16] E. Santos, Probabilistic Turing Machines and Computability, Proc. American Mathematical Society 22 (1969)
704β710.
[17] J. Gill, Computational Complexity of Probabilistic Turing Machines, in: Proc. Symposium on Theory of
Computing (STOC), 1974, pp. 91β95.
[18] M. O. Rabin, Probabilistic Automata, Information and Computation 6 (1963) 230β245.
[19] R. Segala, A Compositional Trace-Based Semantics for Probabilistic Automata, in: Proc. International
Conference on Concurrency Theory (CONCUR), 1995, pp. 234β248.
[20] N. Saheb-Djaromi, Probabilistic LCF, in: A. Press (Ed.), Proc. International Symposium on Mathematical
Foundations of Computer Science, 1978, pp. 154β165.
[21] J. Pearl, Probabilistic Reasoning in Intelligent Systems. Networks of Plausible Inference, Elsavier, 1988.
[22] N. Nilsson, Probabilistic Logic, Artificial Intelligence 28 (1986) 71β87.
[23] F. Bacchus, Representing and Reasoning with Probabilistic Knowledge, MIT Press, 1990.
[24] R. Fagin, J. Halpern, N. Megiddo, A Logic for Reasoning about Probabilities, Information and Computation 87
(1990) 78β128.
[25] J. Halpern, Reasoning About Uncertainty, MIT Press, 2003.
[26] M. Antonelli, Towards a Logical Foundation of Randomized Computation, Ph.D. thesis, University of Bologna,
Department of Computer Science and Engineering, 2023.
[27] L. Valiant, The Complexity of Computing the Permanent, Theoretical Computer Science 8 (1979) 189β201.
[28] M. Antonelli, U. Dal Lago, P. Pistone, On Counting Propositional Logic and Wagnerβs Hierarchy, Theoretical
Computer Science (2023).
[29] M. Antonelli, Two Remarks on Counting Propositional Logic, in: Proc. Workshop on Bias, Risk, Explainability
and the role of Logic and Logic Programming (BEWARE), AIxIA Conference, 2022, pp. 20β32.
[30] M. Antonelli, U. Dal Lago, P. Pistone, On Counting Propositional Logic and Wagnerβs Hierarchy, in: Proc.
Italian Conference of Theoretical Computer Science (ICTCS), 2021, pp. 107β121.
[31] M. Antonelli, U. Dal Lago, P. Pistone, Towards Logical Foundations for Probabilistic Computation, Annals of
Pure and Applied Logic (2023).
[32] C. Faggian, S. Ronchi della Rocca, Lambda Calculus and Probabilistic Computation, in: Proc. Symposium on
Logic in Computer Science (LICS), 2019, pp. 1β13.
[33] U. Dal Lago, G. Guerrieri, W. Heijltjes, Decomposing Probabilistic Lambda-Calculi, in: Proc. Foundations of
Software Science and Computation Structures (FoSSaCS), 2020, pp. 136β156.
[34] M. Antonelli, U. Dal Lago, P. Pistone, Curry and Howard Meet Borel, Proc. Symposium on Logic in Computer
Science (LICS) (2022) 1β13.
[35] K. GΓΆdel, Γber Formal Unentscheidbare SΓ€tze der Principia Mathematica und Verwandter Systeme, Monatsch.
Math. Phys. 38 (1931) 173β178.
[36] G. Kreisel, Interpretation of Analysis by Means of Constructive Funcionals of Finite Types, in: A. Heyting
(Ed.), Constructivity in Mathematics, North-Holland, 1959, pp. 101β128.
[37] K. GΓΆdel, Γber eine Bisher noch nicht BenΓΌtzte Erweiterung des Finiten Standpunktes, Dialectica 12 (1958)
280β287.
[38] M. Antonelli, U. Dal Lago, D. Davoli, I. Oitavem, P. Pistone, Enumerating Erorr Bounded Polytime Algorithms
Through Arithmetical Theories, in: Proc. Computer Science Logic (CSL), 2024.
[39] M. Antonelli, U. Dal Lago, D. Davoli, I. Oitavem, P. Pistone, Towards a Randomized Bounded Arithmetic, in:
AILA - Book of Abstract, 2022.
[40] M. Antonelli, U. Dal Lago, D. Davoli, I. Oitavem, P. Pistone, Enumerating Erorr Bounded Polytime Algorithms
Through Arithmetical Theories, in: Logic Colloquium 2023 - Book of Abstract, 2023, pp. 45β46.
[41] M. Antonelli, U. Dal Lago, P. Pistone, On Measure Quantifiers in First-Order Arithmetic, in: L. De Mol, M. F.
Weiermann, A., D. FernΓ‘ndez-Duque (Eds.), Proc. Computability in Europe Conference (CiE), 2021, pp. 12β24.
[42] P. Billingsley, Probability and Measure, Wiley, 1995.
A. Outline of the Thesis
The Ph.D. dissertation Towards a Logical Foundation of Randomized Computation [26] was defended in July 2023 at
the University of Bologna, Department of Computer Science and Engineering (DISI). Its main contributions concern
three aspects of the interaction between quantitative logic and probabilistic computation. Accordingly, the thesis is
divided into three parts. Each one is intended to be as self-contained as possible and the opening chapter always
offers a birdβs-eye view of the topic captioned in the corresponding part. It includes a brief historical overview and
global motivations, together with an informal presentation of the results to be later considered.
β’ In the first part of the dissertation [26, Ch. 2-5], counting propositional logics are introduced and proved
able to define complete (logical) problems for each level of Wagnerβs hierarchy. Specifically, the languages of
univariate CPL0 and of multivariate CPL are presented in Chapters 3 and 4, respectively, together with the
associated, quantitative semantics. These systems provide a natural formalism to represent stochastic events
(see [26, Sec. 3.4]) and support a suitable proof-theoretical treatment (see [26, Sec. 3.3, Sec. 4.2]), in the form
of sound and complete sequent calculi. The main result of this part is the logical characterization of CH, as
presented in Chapter 5.
β’ The second part of the thesis [26, Ch. 6-10] is devoted to our proposal of a probabilistic CHC. In Chapter 7,
the intuitionistic version of counting propositional logic, called iCPL, is defined, while, in Chapter 8, the
computational part of the correspondence, namely a slightly modified version of the probabilistic event
π-calculus by Dal Lago, Guerrieri and Heijltjes [33], is considered. The principal contribution here is the
definition of a probabilistic CHC between a fragment of intuitionistic counting propositional logic and a
counting-typed system able to express the probability of termination. This is presented in Chapter 9. Then,
in Chapter 10, termination properties are further investigated by introducing a related intersection type
system.
β’ Finally, in the third part of the dissertation [26, Ch. 11-13], a more general language, called MQPA, is
introduced together with a quantitative semantics. This language extends that of PA via second-order
measure quantifiers, which are not far from counting ones. In Chapter 12, it is shown that the expressive
power of MQPA is effectively remarkable. Indeed, results from probability theory, which cannot be expressed
in PA, can instead be properly formalized in it. Furthermore, it is proved that any recursive random function
can be represented by a formula of MQPA. In Chapter 13, a new randomized bounded arithmetic theory is
defined and it is established that the class of formulas which are Ξ£π1 -representable in it is precisely that of
poly-time random functions. Due to this result, an arithmetical characterization of BPP is provided.
All the quoted contributions are part of the joint work with Ugo Dal Lago and Paolo Pistone. Our research about
randomized bounded theory, as presented in Section 14, was developed together with Davide Davoli and Isabel
Oitavem. Crucial results from [26, Part I] have been partially presented in [30, 29, 28, 31]. The main contributions
of [26, Part II] have been published in [34, 31]. The language MQPA and its connections with random functions, as
introduced in [26, Part III], have been presented in [41], while results concerning randomized bounded theories [26,
Ch. 13] have appeared (or will appear) in [39, 40, 38].
B. Counting and Measure-Quantified Logics in a Nutshell
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.
B.1. Basic Probability Theory
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 F of 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 affect 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 πΆπ¦π(π) = 12 .
)οΈ
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 , . . . , π’π ) β π».
B.2. On Counting Propositional Logic
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 intersec-
tion 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 β© [0, 1] β, inspired by
Wagnerβs counting operator [1]. Intuitively, the formula Cπ πΉ (resp., Dπ πΉ ) expresses that πΉ is satisfied by a portion
of assignments greater (resp., strictly smaller) than π. For example, C1/2 πΉ expresses the fact that πΉ is satisfied by at
least half of its valuations. In the more expressive counting propositional logic, CPL, relations between valuations
of different groups of variables can be taken into account. Contextually, the corresponding quantitative semantics is
subtler than that of CPL0 and the interpretation for counting-quantified formulas relies on some technical notions.
Remarkably, in [30, 28, 31], sound and complete proof system(s) for both CPL0 and CPL are introduced.
Remark 1. There is a strong connection between (closed) formulas of CPL0 and (closed) formulas of CPL in which
only one name occurs. Indeed, a translation which preserves validity can be easily defined to pass from ones to the
others [26, Sec. 4.1].
B.2.1. Syntax and Semantics of CPL0
Definition 3 (Formulas of CPL0 ). Formulas of CPL0 are defined by the grammar below:
πΉ ::= i | Β¬πΉ | πΉ β§ πΉ | πΉ β¨ πΉ | Cπ πΉ | Dπ πΉ,
where π β N and π β Q β© [0, 1].
(οΈ )οΈ
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:
{οΈ (οΈ
JiK := πΆπ¦π(π) 2N if π C JπΊK) β₯ π
JCπ πΊK :=
JΒ¬πΊK := 2N β JπΊK β
otherwise
{οΈ (οΈ
JπΊ β§ π»K := JπΊK β© Jπ»K 2N if π C JπΊK) < π
JDπ πΊK :=
JπΊ β¨ π»K := JπΊK βͺ Jπ»K β
otherwise.
Example 1. Let us consider C1/2 (πΉ β¨ πΊ), where(οΈ πΉ = 0 β§)οΈΒ¬1 and )οΈ Β¬0 β§(οΈ1. The
(οΈ πΊ = )οΈ measurable sets, JπΉ K and JπΊK,
have both measure 14 and are disjoint. Hence, π C JπΉ β¨ πΊK = π C JπΉ K + π C JπΊK = 12 , and JC1/2 (πΉ β¨ πΊ)K = 2N .
Observe that counting quantifiers are inter-definable but not dual, in the sense of standard modal operators:
Cπ πΉ is not equivalent to Β¬Dπ Β¬πΉ .
Definition 5. For any formula of CPL0 , call it πΉ , πΉ is said to be valid when JπΉ K = 2N and to be invalid when
JπΉ K = β
.
Remark 2. By combining counting quantifiers it is possible to easily express that a formula πΉ βis true with precisely
a given probabilityβ, see [29].
B.2.2. Syntax and Semantics of CPL
We now introduce the more expressive fragment CPL, in which relations between valuations of different 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 π, π... β A for (countable) sets of names.
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 β© [0, 1].
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 π.
The interpretation of a formula πΉ now depends on the )οΈ of a finite set of names π β FN(πΉ ) and is a
(οΈ choice
measurable set JπΉ Kπ belonging to the Borel algebra, B (2N )π . To define it formally we need to introduce the
technical notion of π -projection.
Definition 7 (π -projection). Let π, π be two disjoint, finite sets of names, and π β (2N )π . For all π³ β (2N )πβͺπ ,
the π -projection of π³ is the set:
Ξ π (π³ ) := π β (2N )π | π + π β π³ β (2N )π ,
{οΈ }οΈ
where {οΈ
π (πΌ) if πΌ β π
(π + π)(πΌ) :=
π(πΌ) if πΌ β π.
Definition 8 (Semantics of CPL). For each formula πΉ of CPL and finite set of names such that π β FN(πΉ ), the
interpretation JπΉ Kπ β (2N )π is defined as follows:
Jiπ Kπ := {π | π (π)(π) = 1} JΒ¬πΊKπ := (2N )π β JπΊKπ
JCππ πΊKπ := π | π C Ξ π (JπΉ Kπβͺ{π} ) β₯ π
{οΈ (οΈ )οΈ }οΈ
JπΊ β§ π»Kπ := JπΊKπ β© Jπ»Kπ
JDππ πΊKπ := π | π C JπΊKπβͺ{π} ) < π .
{οΈ (οΈ )οΈ }οΈ
JπΊ β¨ π»Kπ := JπΊKπ βͺ Jπ»Kπ
1/2 1/2
Example 2. Let us consider the formula Cπ Cπ πΉ , where
(οΈ )οΈ (οΈ )οΈ (οΈ )οΈ
πΉ = 2π β§ (Β¬2π β§ 3π ) β¨ Β¬2π β§ (2π β§ Β¬3π ) β¨ (Β¬2π β§ 3π ) β§ 3π .
1/2
The valuations π β (2N ){π} belonging to JCπ πΉ K{π} are those which can be extended to valuations of all Boolean
variables satisfying πΉ in at least half of the cases. Let us list all possible cases:
1. π (π)(2) = π (π)(3) = 1. Then, πΉ has 41 chances of being true, as both Β¬2π and 3π have to be true
2. π (π)(2) = 1, π (π)(3) = 0. Then, πΉ has 21 chances of being true, as Β¬2π has 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
to be true
4. π (π)(2) = π (π)(3) = 0. Then, πΉ has no chance of being true.
1/2 q 1/2 1/2 y
Clearly, JCπ πΉ K{π} only contains the valuations which agree with cases 2. and 3. Therefore, Cπ Cπ πΉ β
= 2N ,
1/2 1/2
i.e. Cπ Cπ πΉ is valid, since half of the valuations of π has at least 12 chances of being extended to a model of πΉ .
B.3. On Measure-Quantified Peano Arithmetic
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:
π‘ ::= π₯ | 0 | S(π‘) | π‘ + π | π‘ Γ π .
The syntax for formulas of MQPA is as follows:
πΉ ::= Flip(π‘) | (π‘ = π ) | Β¬πΉ | πΉ β¨ πΊ | πΉ β§ πΊ | βπ₯.πΉ | βπ₯.πΉ | Cπ‘/π πΉ | Dπ‘/π πΉ.
Given an environment π : π’ β N, the interpretation Jπ‘Kπ of a term π‘ is defined as usual. Instead, the interpretation
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π := π | π Jπ‘Kπ = 1 JπΊ β¨ π»Kπ := JπΊKπ βͺ Jπ»Kπ
JπΊ β§ π»Kπ := JπΊKπ β© Jπ»Kπ
{οΈ
2N if Jπ‘Kπ = Jπ Kπ
J(π‘ = π )Kπ := βοΈ
β
otherwise Jβπ₯.πΊKπ := JπΊKπ{π₯βπ}
πβN
JΒ¬πΊKπ := 2N β JπΊKπ βοΈ
Jβπ₯.πΊKπ := JπΊKπ{π₯βπ}
πβN
{οΈ
π‘/π 2N if Jπ Kπ > 0 and π C(JπΊKπ ) β₯ Jπ‘Kπ /Jπ Kπ
JC πΊKπ :=
β
otherwise
{οΈ
2N if Jπ Kπ = 0 or π C(JπΊKπ ) < Jπ‘Kπ /Jπ Kπ
JDπ‘/π πΊKπ :=
β
otherwise
The semantics is well-defined as the sets JFlip(π‘)Kπ and J(π‘ = π )Kπ are measurable, and measurability is preserved
by all logical and counting operators. A formula of MQPA, say πΉ , is said to be valid when, for every π, JπΉ Kπ = 2N .
Example 3. The formula πΉ = C1/1 βπ₯.Flip(π₯) states that a true random bit will almost surely be met. This formula
is valid, as the set of constantly 0 sequences forms a singleton of measure 0.