Por Melissa Antonelli (University of Bologna).
Interactions between logics and theoretical computer science are numerous and deep. As it is well-known, the development of deterministic computational models has considerably benefitted from these mutual interchanges. There is, however, one aspect of the theory of computation which has only marginally been touched by such a back and forth interaction, namely randomized computation. This is becoming more and more evident, due to the increasing pervasiveness of probabilistic models in several areas of computer science. The aim of our study is to start bridging this gap by introducing a logical counterpart to certain aspects of randomized computation, therefore generalizing standard achievements to the probabilistic setting. All the results I am going to present are part of a joint work with Ugo Dal Lago and Paolo Pistone.
We will start by exploring counting propositional logic, which extends standard PL by means of counting quantifiers. We will first describe the simplistic fragment, CPL0, in which counting quantification is nameless, then move to its multivariate (actually non-conservative) generalization, CPL. Some interactions between these logics and theoretical computer science will be sketched. For example, thanks to CPL, we are able to give a logical characterization of the Counting Hierarchy (in the spirit of Meyer and Stockmeyer's work on QPL and PH), and to establish a correspondence with probabilistic lambda-calculi in the style of the Curry-Howard one.
We will conclude the presentation by briefly describing the more powerful MQPA, a generalization of CPL obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This logic is capable of expressing arithmetical formulas, dealing with probabilistic choices, and of formalizing basic results from probability theory. In our opinion, this system may constitute a logical counterpart to randomized computation, in the same way as Peano Arithmetic corresponds to deterministic computation.
This is a joint session with SAL (CMA/FCT-UNL).
Zoom | ID da reunião: 890 8479 3299 - senha de acesso: 409604
