arXiv subjects

Melissa Antonelli

Publications and source records attributed to Melissa Antonelli.

13 recordsLinked to original sources

arXiv2026

Towards a Characterization of Counting and Alternating Classes via Discrete Ordinary Differential Equations

This paper presents a high-level report on an ongoing project aiming to leverage implicit approaches based on discrete ordinary differential equations (ODEs) to study multiple complexity classes, even beyond small circuit and polynomial-time classes. Stimulated by recent ODE-based characterizations of polynomial-time functions (FP) and classes over the reals, the research project outlined here pushes this investigation further into counting and alternation. Specifically, we present a uniform framework, built upon a single base algebra and a unified family of schemas, where complexity levels, such as those of the polynomial and counting hierarchies, are captured simply by the nesting depth of ODE operators. Crucially, our approach starts from a base class much weaker than FP, thus strengthening existing recursion-theoretic treatments and establishing a natural connection to descriptive complexity. Moreover, by isolating three elementary schemas, our framework makes the computational content of linearity restrictions completely transparent while extending ODE-based implicit complexity to previously unaddressed counting classes, such as oplusP. More generally, this work establishes a clear bridge between differentiation and counting, offering a fresh perspective on the relationships between different complexity classes, which remains the object of ongoing and future research.

cs.CC↗

arXiv2026

A Linear Temporal Logic of Frequencies on Series of Events

This paper introduces LTLF, a temporal logic designed to express the frequency properties of event series in a natural but rigorous manner. By introducing novel, measure-sensitive operators, LTLF allows for the evaluation of frequencies and the prediction of future occurrences, thus providing a formal framework to monitor and control quantitative systems, such as machine learning classifiers. The core novelty lies in the introduction of original modal quantifiers associated with a standard Kripke-style semantics. These quantifiers enable the explicit formalization of event series properties and the investigation of the relationship between actual observed frequencies and ideal distributions within a single logical structure. This framework bridges the gap between formal logical reasoning and empirical observation.

cs.LO↗

arXiv2026

Recursion and proof theoretical characterizations of small circuit classes with modulo counting via discrete differential equations (long version)

The paper proposes an implicit (i.e., machine-independent) complexity approach to studying computation by polynomial-size, constant-depth circuits with gates counting modulo a constant through the lens of discrete ordinary differential equations (ODEs). So far, recursion-theoretic characterizations have been provided for functions computed by circuits of constant depth, including gates counting modulo 2 and 6 only (i.e., for the classes FAC0[2] and FAC0[6], resp.). In this paper, it is shown that considering ODE schemas, rather than bounded recursion, allows for a more fine-grained analysis, leading to (uniform) characterizations for all classes FAC0[n] (n \in N), i.e. functions computed by circuits including counting modulo n gates. Inspired by the syntactic form of the ODE schemas, we go further in this direction and present first-order bounded theories for capturing provably total functions in each of these classes.

cs.CC↗

arXiv2026

Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI

Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. In this paper we introduce CTLF, a branching-time logic designed to reason about bias in series of generative AI outputs. CTLF adopts a counting worlds semantics where each world represents a possible output at a given step in the generation process and introduces modal operators that allow us to verify whether the current output series respects an intended probability distribution over a protected attribute, to predict the likelihood of remaining within acceptable bounds as new outputs are generated, and to determine how many outputs are needed to remove in order to restore fairness. We illustrate the framework on a toy example of biased image generation, showing how CTLF formulas can express concrete fairness properties at different points in the output series.

cs.LO↗

arXiv2025

Towards New Characterizations of Small Circuit Classes via Discrete Ordinary Differential Equations

Implicit computational complexity is a lively area of theoretical computer science, which aims to provide machine-independent characterizations of relevant complexity classes. % for uniformity with subsequent uses >> 1960s (but feel free to modify it) % One of the seminal works in this field appeared in the 1960s, when Cobham introduced a function algebra closed under bounded recursion on notation to capture polynomial time computable functions ($FP$). Later on, several complexity classes have been characterized using \emph{limited} recursion schemas. In this context, an original approach has been recently introduced, showing that ordinary differential equations (ODEs) offer a natural tool for algorithmic design and providing a characterization of $FP$ by a new ODE-schema. In the present paper we generalize this approach by presenting original ODE-characterizations for the small circuit classes $AC^0$ and $FTC^0$.

cs.CC↗

arXiv2025

Characterizing Small Circuit Classes from FAC^0 to FAC^1 via Discrete Ordinary Differential Equations

In this paper, we provide a uniform framework for investigating small circuit classes and bounds through the lens of ordinary differential equations (ODEs). Following an approach recently introduced to capture the class of polynomial-time computable functions via ODE-based recursion schemas and later applied to the context of functions computed by unbounded fan-in circuits of constant depth (FAC^0), we study multiple relevant small circuit classes. In particular, we show that natural restrictions on linearity and derivation along functions with specific growth rate correspond to kinds of functions that can be proved to be in various classes, ranging from FAC^0 to FAC^1. This reveals an intriguing link between constraints over linear-length ODEs and circuit computation, providing new tools to tackle the complex challenge of establishing bounds for classes in the circuit hierarchies and possibly enhancing our understanding of the role of counters in this setting. Additionally, we establish several completeness results, in particular obtaining the first ODE-based characterizations for the classes of functions computable in constant depth with unbounded fan-in and Mod 2 gates (FACC[2]) and in logarithmic depth with bounded fan-in Boolean gates (FNC1).

cs.CC↗

arXiv2024

On Randomized Computational Models and Complexity Classes: a Historical Overview

Since their appearance in the 1950s, computational models capable of performing probabilistic choices have received wide attention and are nowadays pervasive in almost every areas of computer science. Their development was also inextricably linked with inquiries about computation power and resource issues. Although most crucial notions in the field are well-known, the related terminology is sometimes imprecise or misleading. The present work aims to clarify the core features and main differences between machines and classes developed in relation to randomized computation. To do so, we compare the modern definitions with original ones, recalling the context in which they first appeared, and investigate the relations linking probabilistic and counting models.

cs.LO↗

arXiv2023

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories

We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in the theory T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T where T=$\mathrm{I}Δ_0+\mathrm{Exp}$ is a well-studied theory based on bounded induction.

cs.LO↗

arXiv2023

An Arithmetic Theory for the Poly-Time Random Functions

We introduce a new bounded theory RS^1_2 and show that the functions which are Sigma^b_1-representable in it are precisely random functions which can be computed in polynomial time. Concretely, we pass through a class of oracle functions over string, called POR, together with the theory of arithmetic RS^1_2. Then, we show that functions computed by poly-time PTMs are arithmetically characterized by a class of probabilistic bounded formulas.

cs.CC↗

arXiv2022

Some Remarks on Counting Propositional Logic

Counting propositional logic was recently introduced in relation to randomized computation and shown able to logically characterize the full counting hierarchy. In this paper we aim to clarify the intuitive meaning and expressive power of its univariate fragment. On the one hand, we provide an effective procedure to measure the probability of counting formulas. On the other, we make the connection between this logic and stochastic experiments explicit, proving that the counting language can simulate any (and only) event associated with dyadic distributions.

cs.LO↗

arXiv2022

Curry and Howard Meet Borel

We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambda-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. Remarkably, proofs (respectively, types) do not only guarantee that validity (respectively, termination) holds, but also reveal the underlying probability. We finally show that by endowing the type system with an intersection operator, one obtains a system precisely capturing the probabilistic behavior of lambda-terms.

cs.LO↗

arXiv2021

On Counting Propositional Logic

We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagner's counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.

cs.LO↗

arXiv2021

On Measure Quantifiers in First-Order Arithmetic (Long Version)

We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the argument formula is true in a certain portion of all possible interpretations of the quantified variable. We show that first-order arithmetic with measure quantifiers is capable of formalizing simple results from probability theory and, most importantly, of representing every recursive random function. Moreover, we introduce a realizability interpretation of this logic in which programs have access to an oracle from the Cantor space.

cs.LO↗