-
On quantitative convergence for stochastic processes: Crossings, fluctuations and martingales
Authors:
Morenikeji Neri,
Thomas Powell
Abstract:
We develop a general framework for extracting highly uniform bounds on local stability for stochastic processes in terms of information on fluctuations or crossings. This includes a large class of martingales: As a corollary of our main abstract result, we obtain a quantitative version of Doob's convergence theorem for $L_1$-sub- and supermartingales, but more importantly, demonstrate that our fra…
▽ More
We develop a general framework for extracting highly uniform bounds on local stability for stochastic processes in terms of information on fluctuations or crossings. This includes a large class of martingales: As a corollary of our main abstract result, we obtain a quantitative version of Doob's convergence theorem for $L_1$-sub- and supermartingales, but more importantly, demonstrate that our framework readily extends to more complex stochastic processes such as almost-supermartingales, thus paving the way for future applications in stochastic optimization. Fundamental to our approach is the use of ideas from logic, particularly a careful analysis of the quantifier structure of probabilistic statements and the introduction of a number of abstract notions that represent stochastic convergence in a quantitative manner. In this sense, our work falls under the 'proof mining' program, and indeed, our quantitative results provide new examples of the phenomenon, recently made precise by the first author and Pischke, that many proofs in probability theory are proof-theoretically tame, and amenable to the extraction of quantitative data that is both of low complexity and independent of the underlying probability space.
△ Less
Submitted 28 June, 2024;
originally announced June 2024.
-
Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
Authors:
Thomas Powell
Abstract:
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the assertions about the state compose in the correct way. The main result of the paper is a realizabili…
▽ More
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the assertions about the state compose in the correct way. The main result of the paper is a realizability interpretation of our logic that extracts programs into a mixed functional/imperative language. All programs expressible in this language act on the state in a sequential manner, and we make this intuition precise by interpreting them in a semantic metatheory using the state monad. Our basic framework is very general, and our intention is that it can be instantiated and extended in a variety of different ways. We outline in detail one such extension: A monadic version of Heyting arithmetic with a wellfounded while rule, and conclude by outlining several other directions for future work.
△ Less
Submitted 25 January, 2024; v1 submitted 4 January, 2023;
originally announced January 2023.
-
A computational study of a class of recursive inequalities
Authors:
Morenikeji Neri,
Thomas Powell
Abstract:
We examine the convergence properties of sequences of nonnegative real numbers that satisfy a particular class of recursive inequalities, from the perspective of proof theory and computability theory. We first establish a number of results concerning rates of convergence, setting out conditions under which computable rates are possible, and when not, providing corresponding rates of metastability.…
▽ More
We examine the convergence properties of sequences of nonnegative real numbers that satisfy a particular class of recursive inequalities, from the perspective of proof theory and computability theory. We first establish a number of results concerning rates of convergence, setting out conditions under which computable rates are possible, and when not, providing corresponding rates of metastability. We then demonstrate how the aforementioned quantitative results can be applied to extract computational information from a range of proofs in nonlinear analysis. Here we provide both a new case study on subgradient algorithms, and give overviews of a selection of recent results which each involve an instance of our main recursive inequality. This paper contains the definitions of all relevant concepts from both proof theory and mathematical analysis, and as such, we hope that it is accessible to a general audience.
△ Less
Submitted 1 May, 2023; v1 submitted 29 July, 2022;
originally announced July 2022.
-
Rates of convergence for asymptotically weakly contractive mappings in normed spaces
Authors:
Thomas Powell,
Franziskus Wiesnet
Abstract:
We study Krasnoselskii-Mann style iterative algorithms for approximating fixpoints of asymptotically weakly contractive mappings, with a focus on providing generalised convergence proofs along with explicit rates of convergence. More specifically, we define a new notion of being asymptotically $ψ$-weakly contractive with modulus, and present a series of abstract convergence theorems which both gen…
▽ More
We study Krasnoselskii-Mann style iterative algorithms for approximating fixpoints of asymptotically weakly contractive mappings, with a focus on providing generalised convergence proofs along with explicit rates of convergence. More specifically, we define a new notion of being asymptotically $ψ$-weakly contractive with modulus, and present a series of abstract convergence theorems which both generalise and unify known results from the literature. Rates of convergence are formulated in terms of our modulus of contractivity, in conjunction with other moduli and functions which form quantitative analogues of additional assumptions that are required in each case. Our approach makes use of ideas from proof theory, in particular our emphasis on abstraction and on formulating our main results in a quantitative manner. As such, the paper can be seen as a contribution to the proof mining program.
△ Less
Submitted 29 April, 2021;
originally announced April 2021.
-
On the computational content of Zorn's lemma
Authors:
Thomas Powell
Abstract:
We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is achieved through Gödel's functional interpretation, and requires the introduction of a novel form of recursion over non-wellfounded partial orders whose existence in the model of total continuous functionals is proven us…
▽ More
We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is achieved through Gödel's functional interpretation, and requires the introduction of a novel form of recursion over non-wellfounded partial orders whose existence in the model of total continuous functionals is proven using domain theoretic techniques. We show that a realizer for the functional interpretation of open induction over the lexicographic ordering on sequences follows as a simple application of our main results.
△ Less
Submitted 28 April, 2020; v1 submitted 10 January, 2020;
originally announced January 2020.
-
A note on the finitization of Abelian and Tauberian theorems
Authors:
Thomas Powell
Abstract:
We present finitary formulations of two well known results concerning infinite series, namely Abel's theorem, which establishes that if a series converges to some limit then its Abel sum converges to the same limit, and Tauber's theorem, which presents a simple condition under which the converse holds. Our approach is inspired by proof theory, and in particular Gödel's functional interpretation, w…
▽ More
We present finitary formulations of two well known results concerning infinite series, namely Abel's theorem, which establishes that if a series converges to some limit then its Abel sum converges to the same limit, and Tauber's theorem, which presents a simple condition under which the converse holds. Our approach is inspired by proof theory, and in particular Gödel's functional interpretation, which we use to establish quantitative version of both of these results.
△ Less
Submitted 17 October, 2019;
originally announced October 2019.
-
Rates of convergence for iterative solutions of equations involving set-valued accretive operators
Authors:
Ulrich Kohlenbach,
Thomas Powell
Abstract:
This paper studies proofs of strong convergence of various iterative algorithms for computing the unique zeros of set-valued accretive operators that also satisfy some weak form of uniform accretivity at zero. More precisely, we extract explicit rates of convergence from these proofs which depend on a modulus of uniform accretivity at zero, a concept first introduced by A. Koutsoukou-Argyraki and…
▽ More
This paper studies proofs of strong convergence of various iterative algorithms for computing the unique zeros of set-valued accretive operators that also satisfy some weak form of uniform accretivity at zero. More precisely, we extract explicit rates of convergence from these proofs which depend on a modulus of uniform accretivity at zero, a concept first introduced by A. Koutsoukou-Argyraki and the first author in 2015. Our highly modular approach, which is inspired by the logic-based proof mining paradigm, also establishes that a number of seemingly unrelated convergence proofs in the literature are actually instances of a common pattern.
△ Less
Submitted 24 April, 2020; v1 submitted 19 August, 2019;
originally announced August 2019.
-
A unifying framework for continuity and complexity in higher types
Authors:
Thomas Powell
Abstract:
We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main…
▽ More
We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main goal is to provide a unifying scheme which brings together several concepts which are often treated separately in the literature. However, as a by-product, we also obtain (i) a method for extracting moduli of continuity for closed functionals of type $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ definable in (extensions of) System T, and (ii) a characterisation of the time complexity of bar recursion.
△ Less
Submitted 8 September, 2020; v1 submitted 25 June, 2019;
originally announced June 2019.
-
An algorithmic approach to the existence of ideal objects in commutative algebra
Authors:
Thomas Powell,
Peter M Schuster,
Franziskus Wiesnet
Abstract:
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, wh…
▽ More
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, which focuses on the elimination of ideal objects via syntactic methods. In this paper, we take an alternative approach based on Kreisel's no counterexample interpretation and sequential algorithms. We first give a computational interpretation to an abstract maximality principle in the countable setting via an intuitive, state based algorithm. We then carry out a concrete case study, in which we give an algorithmic account of the result that in any commutative ring, the intersection of all prime ideals is contained in its nilradical.
△ Less
Submitted 7 March, 2019;
originally announced March 2019.
-
Dependent choice as a termination principle
Authors:
Thomas Powell
Abstract:
We introduce a new formulation of the axiom of dependent choice that can be viewed as an abstract termination principle, which generalises the recursive path orderings used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.
We introduce a new formulation of the axiom of dependent choice that can be viewed as an abstract termination principle, which generalises the recursive path orderings used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.
△ Less
Submitted 25 February, 2019;
originally announced February 2019.
-
A new metastable convergence criterion and an application in the theory of uniformly convex Banach spaces
Authors:
Thomas Powell
Abstract:
We study a convergence criterion which generalises the notion of being monotonically decreasing, and introduce a quantitative version of this criterion, a so called metastable rate of asymptotic decreasingness. We then present a concrete application in the fixed point theory of uniformly convex Banach spaces, in which we carry out a quantitative analysis of a convergence proof of Kirk and Sims. Mo…
▽ More
We study a convergence criterion which generalises the notion of being monotonically decreasing, and introduce a quantitative version of this criterion, a so called metastable rate of asymptotic decreasingness. We then present a concrete application in the fixed point theory of uniformly convex Banach spaces, in which we carry out a quantitative analysis of a convergence proof of Kirk and Sims. More precisely, we produce a rate of metastability (in the sense of Tao) for the Picard iterates of mappings T which satisfy a variant of the convergence criterion, and whose fixed point set has nonempty interior.
△ Less
Submitted 6 December, 2019; v1 submitted 25 February, 2019;
originally announced February 2019.
-
A proof theoretic study of abstract termination principles
Authors:
Thomas Powell
Abstract:
We carry out a proof theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a very general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees which can be defined in Gödel's system T plus bar recursion. We then carry out a complexity analysis of these terms, and demonstrate how this can…
▽ More
We carry out a proof theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a very general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees which can be defined in Gödel's system T plus bar recursion. We then carry out a complexity analysis of these terms, and demonstrate how this can be applied to bound the derivational complexity of term rewrite systems.
△ Less
Submitted 22 February, 2019; v1 submitted 12 June, 2017;
originally announced June 2017.
-
Well quasi-orders and the functional interpretation
Authors:
Thomas Powell
Abstract:
The purpose of this article is to study the role of Gödel's functional interpretation in the extraction of programs from proofs in well quasi-order theory. The main focus is on the interpretation of Nash-Williams' famous minimal bad sequence construction, and the exploration of a number of much broader problems which are related to this, particularly the question of the constructive meaning of Zor…
▽ More
The purpose of this article is to study the role of Gödel's functional interpretation in the extraction of programs from proofs in well quasi-order theory. The main focus is on the interpretation of Nash-Williams' famous minimal bad sequence construction, and the exploration of a number of much broader problems which are related to this, particularly the question of the constructive meaning of Zorn's lemma and the notion of recursion over the non-wellfounded lexicographic ordering on infinite sequences.
△ Less
Submitted 9 June, 2017;
originally announced June 2017.
-
Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice
Authors:
Thomas Powell
Abstract:
During the last twenty years or so a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work we present the many variants…
▽ More
During the last twenty years or so a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work we present the many variants of bar recursion used in this context as instantiations of a general, parametrised recursor, and give a uniform proof that under certain conditions this recursor realizes a corresponding family of parametrised dependent choice principles. From this proof, the soundness of most of the existing bar recursive realizability interpretations of choice, including those based on the Berardi-Bezem-Coquand functional, modified realizability and the more recent products of selection functions of Escardó and Oliva, follows as a simple corollary. We achieve not only a uniform framework in which familiar realizability interpretations of choice can be compared, but show that these represent just simple instances of a large family of potential interpretations of dependent choice principles.
△ Less
Submitted 12 March, 2015; v1 submitted 3 November, 2014;
originally announced November 2014.
-
Spector bar recursion over finite partial functions
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recu…
▽ More
We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recursive updates, terminating the computation whenever $\varphi(\hat{u})\in\mbox{dom}(u)$. We begin by exploring theoretical aspects of this new form of recursion, then in the main part of the paper we show that demand-driven bar recursion can be directly used to give an alternative functional interpretation of classical countable choice. We provide a short case study as an illustration, in which we extract a new bar recursive program from the proof that there is no injection from $\mathbb{N}\to\mathbb{N}$ to $\mathbb{N}$, and compare this to the program that would be obtained using Spector's original variant. We conclude by formally establishing that our new bar recursor is primitive recursively equivalent to the original Spector bar recursion, and thus defines the same class of functionals when added to Gödel's system $\sf T$.
△ Less
Submitted 17 August, 2015; v1 submitted 23 October, 2014;
originally announced October 2014.
-
A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.
We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.
△ Less
Submitted 1 June, 2012; v1 submitted 25 April, 2012;
originally announced April 2012.
-
A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the prod…
▽ More
It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the product gives these theorems a natural computational interpretation that can be clearly understood in game theoretic terms.
△ Less
Submitted 23 April, 2012;
originally announced April 2012.