-
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
Authors:
Melissa Antonelli,
Ugo Dal Lago,
Davide Davoli,
Isabel Oitavem,
Paolo Pistone
Abstract:
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-sens…
▽ More
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.
△ Less
Submitted 25 November, 2023;
originally announced November 2023.
-
Curry and Howard Meet Borel
Authors:
Melissa Antonelli,
Ugo Dal Lago,
Paolo Pistone
Abstract:
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 vali…
▽ More
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.
△ Less
Submitted 21 March, 2022;
originally announced March 2022.
-
On Measure Quantifiers in First-Order Arithmetic (Long Version)
Authors:
Melissa Antonelli,
Ugo Dal Lago,
Paolo Pistone
Abstract:
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 probabi…
▽ More
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.
△ Less
Submitted 25 April, 2021;
originally announced April 2021.
-
High quality local interpolation by composite parametric surfaces
Authors:
Michele Antonelli,
Carolina Vittoria Beccari,
Giulio Casciola
Abstract:
In CAGD the design of a surface that interpolates an arbitrary quadrilateral mesh is definitely a challenging task. The basic requirement is to satisfy both criteria concerning the regularity of the surface and aesthetic concepts. With regard to the aesthetic quality, it is well known that interpolatory methods often produce shape artifacts when the data points are unevenly spaced. In the univaria…
▽ More
In CAGD the design of a surface that interpolates an arbitrary quadrilateral mesh is definitely a challenging task. The basic requirement is to satisfy both criteria concerning the regularity of the surface and aesthetic concepts. With regard to the aesthetic quality, it is well known that interpolatory methods often produce shape artifacts when the data points are unevenly spaced. In the univariate setting, this problem can be overcome, or at least mitigated, by exploiting a proper non-uniform parametrization, that accounts for the geometry of the data. Moreover, recently, the same principle has been generalized and proven to be effective in the context of bivariate interpolatory subdivision schemes. In this paper, we propose a construction for parametric surfaces of good aesthetic quality and high smoothness that interpolate quadrilateral meshes of arbitrary topology. In the classical tensor product setting the same parameter interval must be shared by an entire row or column of mesh edges. Conversely, in this paper, we assign a different parameter interval to each edge of the mesh. This particular structure, which we call an augmented parametrization, allows us to interpolate each section polyline of the mesh at parameters values that prevent wiggling of the resulting curve or other interpolation artifacts. This yields high quality interpolatory surfaces. The proposed surfaces are a generalization of the local univariate spline interpolants introduced in Beccari et al.(2013) and Antonelli et al.(2014), that can have arbitrary continuity and arbitrary order of polynomial reproduction. In particular, these surfaces retain the same smoothness of the underlying class of univariate splines in the regular regions of the mesh. Moreover, in mesh regions containing vertices of valence other than 4, we suitably define G1- or G2-continuous surface patches that join the neighboring regular ones.
△ Less
Submitted 7 January, 2016;
originally announced January 2016.
