Showing 1–26 of 26 results for author: Powell, T

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.

Comments: 42 pages

GPT-4 Technical Report

Authors: OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, Irwan Bello, Jake Berdine, Gabriel Bernadett-Shapiro, Christopher Berner, Lenny Bogdonoff, Oleg Boiko , et al. (256 additional authors not shown)

Abstract: We report the development of GPT-4, a large-scale, multimodal model which can accept image and text inputs and produce text outputs. While less capable than humans in many real-world scenarios, GPT-4 exhibits human-level performance on various professional and academic benchmarks, including passing a simulated bar exam with a score around the top 10% of test takers. GPT-4 is a Transformer-based mo… ▽ More We report the development of GPT-4, a large-scale, multimodal model which can accept image and text inputs and produce text outputs. While less capable than humans in many real-world scenarios, GPT-4 exhibits human-level performance on various professional and academic benchmarks, including passing a simulated bar exam with a score around the top 10% of test takers. GPT-4 is a Transformer-based model pre-trained to predict the next token in a document. The post-training alignment process results in improved performance on measures of factuality and adherence to desired behavior. A core component of this project was develo** infrastructure and optimization methods that behave predictably across a wide range of scales. This allowed us to accurately predict some aspects of GPT-4's performance based on models trained with no more than 1/1,000th the compute of GPT-4. △ Less

Submitted 4 March, 2024; v1 submitted 15 March, 2023; originally announced March 2023.

Comments: 100 pages; updated authors list; fixed author names and added citation

Light Curves and Colors of the Ejecta from Dimorphos after the DART Impact

Authors: Ariel Graykowski, Ryan A. Lambert, Franck Marchis, Dorian Cazeneuve, Paul A. Dalba, Thomas M. Esposito, Daniel O'Conner Peluso, Lauren A. Sgro, Guillaume Blaclard, Antonin Borot, Arnaud Malvache, Laurent Marfisi, Tyler M. Powell, Patrice Huet, Matthieu Limagne, Bruno Payet, Colin Clarke, Susan Murabana, Daniel Chu Owen, Ronald Wasilwa, Keiichi Fukui, Tateki Goto, Bruno Guillet, Patrick Huth, Satoshi Ishiyama , et al. (19 additional authors not shown)

Abstract: On 26 September 2022 the Double Asteroid Redirection Test (DART) spacecraft impacted Dimorphos, a satellite of the asteroid 65803 Didymos. Because it is a binary system, it is possible to determine how much the orbit of the satellite changed, as part of a test of what is necessary to deflect an asteroid that might threaten Earth with an impact. In nominal cases, pre-impact predictions of the orbit… ▽ More On 26 September 2022 the Double Asteroid Redirection Test (DART) spacecraft impacted Dimorphos, a satellite of the asteroid 65803 Didymos. Because it is a binary system, it is possible to determine how much the orbit of the satellite changed, as part of a test of what is necessary to deflect an asteroid that might threaten Earth with an impact. In nominal cases, pre-impact predictions of the orbital period reduction ranged from ~8.8 - 17.2 minutes. Here we report optical observations of Dimorphos before, during and after the impact, from a network of citizen science telescopes across the world. We find a maximum brightening of 2.29 $\pm$ 0.14 mag upon impact. Didymos fades back to its pre-impact brightness over the course of 23.7 $\pm$ 0.7 days. We estimate lower limits on the mass contained in the ejecta, which was 0.3 - 0.5% Dimorphos' mass depending on the dust size. We also observe a reddening of the ejecta upon impact. △ Less

Submitted 9 March, 2023; originally announced March 2023.

Comments: Accepted by Nature

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.

Journal ref: Logical Methods in Computer Science (January 26, 2024) lmcs:10776

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.

Comments: 44 pages

COMAP Early Science: II. Pathfinder Instrument

Authors: James W. Lamb, Kieran A. Cleary, David P. Woody, Morgan Catha, Dongwoo T. Chung, Joshua Ott Gundersen, Stuart E. Harper, Andrew I. Harris, Richard Hobbs, Håvard T. Ihle, Jonathon Kocz, Timothy J. Pearson, Liju Philip, Travis W. Powell, Lilian Basoalto, J. Richard Bond, Jowita Borowska, Patrick C. Breysse, Sarah E. Church, Clive Dickinson, Delaney A. Dunne, Hans Kristian Eriksen, Marie Kristine Foss, Todd Gaier, Junhan Kim , et al. (10 additional authors not shown)

Abstract: Line intensity map** (LIM) is a new technique for tracing the global properties of galaxies over cosmic time. Detection of the very faint signals from redshifted carbon monoxide (CO), a tracer of star formation, pushes the limits of what is feasible with a total-power instrument. The CO Map** Project (COMAP) Pathfinder is a first-generation instrument aiming to prove the concept and develop th… ▽ More Line intensity map** (LIM) is a new technique for tracing the global properties of galaxies over cosmic time. Detection of the very faint signals from redshifted carbon monoxide (CO), a tracer of star formation, pushes the limits of what is feasible with a total-power instrument. The CO Map** Project (COMAP) Pathfinder is a first-generation instrument aiming to prove the concept and develop the technology for future experiments, as well as delivering early science products. With 19 receiver channels in a hexagonal focal plane arrangement on a 10.4 m antenna, and an instantaneous 26-34 GHz frequency range with 2 MHz resolution, it is ideally suited to measuring CO($J$=1-0) from $z\sim3$. In this paper we discuss strategies for designing and building the Pathfinder and the challenges that were encountered. The design of the instrument prioritized LIM requirements over those of ancillary science. After a couple of years of operation, the instrument is well understood, and the first year of data is already yielding useful science results. Experience with this Pathfinder will drive the design of the next generations of experiments. △ Less

Submitted 29 November, 2021; v1 submitted 10 November, 2021; originally announced November 2021.

Comments: Paper 2 of 7 in series. 27 pages, 28 figures, submitted to ApJ

COMAP Early Science: I. Overview

Authors: Kieran A. Cleary, Jowita Borowska, Patrick C. Breysse, Morgan Catha, Dongwoo T. Chung, Sarah E. Church, Clive Dickinson, Hans Kristian Eriksen, Marie Kristine Foss, Joshua Ott Gundersen, Stuart E. Harper, Andrew I. Harris, Richard Hobbs, Håvard, T. Ihle, Junhan Kim, Jonathon Kocz, James W. Lamb, Jonas G. S. Lunde, Hamsa Padmanabhan, Timothy J. Pearson, Liju Philip, Travis W. Powell, Maren Rasmussen, Anthony C. S. Readhead , et al. (18 additional authors not shown)

Abstract: The CO Map** Array Project (COMAP) aims to use line intensity map** of carbon monoxide (CO) to trace the distribution and global properties of galaxies over cosmic time, back to the Epoch of Reionization (EoR). To validate the technologies and techniques needed for this goal, a Pathfinder instrument has been constructed and fielded. Sensitive to CO(1-0) emission from $z=2.4$-$3.4$ and a fainte… ▽ More The CO Map** Array Project (COMAP) aims to use line intensity map** of carbon monoxide (CO) to trace the distribution and global properties of galaxies over cosmic time, back to the Epoch of Reionization (EoR). To validate the technologies and techniques needed for this goal, a Pathfinder instrument has been constructed and fielded. Sensitive to CO(1-0) emission from $z=2.4$-$3.4$ and a fainter contribution from CO(2-1) at $z=6$-8, the Pathfinder is surveying $12$ deg$^2$ in a 5-year observing campaign to detect the CO signal from $z\sim3$. Using data from the first 13 months of observing, we estimate $P_\mathrm{CO}(k) = -2.7 \pm 1.7 \times 10^4μ\mathrm{K}^2 \mathrm{Mpc}^3$ on scales $k=0.051-0.62 \mathrm{Mpc}^{-1}$ - the first direct 3D constraint on the clustering component of the CO(1-0) power spectrum. Based on these observations alone, we obtain a constraint on the amplitude of the clustering component (the squared mean CO line temperature-bias product) of $\langle Tb\rangle^2<49$ $μ$K$^2$ - nearly an order-of-magnitude improvement on the previous best measurement. These constraints allow us to rule out two models from the literature. We forecast a detection of the power spectrum after 5 years with signal-to-noise ratio (S/N) 9-17. Cross-correlation with an overlap** galaxy survey will yield a detection of the CO-galaxy power spectrum with S/N of 19. We are also conducting a 30 GHz survey of the Galactic plane and present a preliminary map. Looking to the future of COMAP, we examine the prospects for future phases of the experiment to detect and characterize the CO signal from the EoR. △ Less

Submitted 29 November, 2021; v1 submitted 10 November, 2021; originally announced November 2021.

Comments: Paper 1 of 7 in series. 18 pages, 16 figures, submitted to ApJ

Rates of convergence for asymptotically weakly contractive map**s in normed spaces

Authors: Thomas Powell, Franziskus Wiesnet

Abstract: We study Krasnoselskii-Mann style iterative algorithms for approximating fixpoints of asymptotically weakly contractive map**s, 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 map**s, 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.

Supervised machine learning techniques for data matching based on similarity metrics

Authors: Pim Verschuuren, Serena Palazzo, Tom Powell, Steve Sutton, Alfred Pilgrim, Michele Faucci Giannelli

Abstract: Businesses, governmental bodies and NGO's have an ever-increasing amount of data at their disposal from which they try to extract valuable information. Often, this needs to be done not only accurately but also within a short time frame. Clean and consistent data is therefore crucial. Data matching is the field that tries to identify instances in data that refer to the same real-world entity. In th… ▽ More Businesses, governmental bodies and NGO's have an ever-increasing amount of data at their disposal from which they try to extract valuable information. Often, this needs to be done not only accurately but also within a short time frame. Clean and consistent data is therefore crucial. Data matching is the field that tries to identify instances in data that refer to the same real-world entity. In this study, machine learning techniques are combined with string similarity functions to the field of data matching. A dataset of invoices from a variety of businesses and organizations was preprocessed with a grou** scheme to reduce pair dimensionality and a set of similarity functions was used to quantify similarity between invoice pairs. The resulting invoice pair dataset was then used to train and validate a neural network and a boosted decision tree. The performance was compared with a solution from FISCAL Technologies as a benchmark against currently available deduplication solutions. Both the neural network and boosted decision tree showed equal to better performance. △ Less

Submitted 15 September, 2021; v1 submitted 8 July, 2020; originally announced July 2020.

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.

MSC Class: 47H05; 47J25; 03F10

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.

Journal ref: Logical Methods in Computer Science, Volume 16, Issue 3 (September 9, 2020) lmcs:5746

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 map**s 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.

Sequential algorithms and the computational content of classical proofs

Authors: Thomas Powell

Abstract: We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes which interact with an oracle, and allows these processes to be modelled at any given level of abstraction. We discuss general constructions on algorithms which rep… ▽ More We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes which interact with an oracle, and allows these processes to be modelled at any given level of abstraction. We discuss general constructions on algorithms which represent specific patterns which often appear in classical reasoning, and in particular, we develop a computational interpretation of the rule of dependent choice which is phrased purely on the level of algorithms, giving us a clearer insight into the computational meaning of proofs in classical analysis. △ Less

Submitted 28 December, 2018; originally announced December 2018.

Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs

Authors: Thomas Powell

Abstract: The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem - the epsilon calculus, modified realizability and the dialectica interpretation - and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming. The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem - the epsilon calculus, modified realizability and the dialectica interpretation - and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming. △ Less

Submitted 14 December, 2018; originally announced December 2018.

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.

Comments: 25 pages

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.

Comments: 28 pages

MSC Class: 03D65; 03F03; 03F10; 03F25

Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma

Authors: Thomas Powell

Abstract: We use Gödel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which Nash-Williams' combinatorial idea is clearly present, along with an explicit program for finding an embedded pair in sequences of words. We use Gödel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which Nash-Williams' combinatorial idea is clearly present, along with an explicit program for finding an embedded pair in sequences of words. △ Less

Submitted 10 October, 2012; originally announced October 2012.

Comments: In Proceedings CL&C 2012, arXiv:1210.2890

Journal ref: EPTCS 97, 2012, pp. 49-62

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.

Quasiparticle Thermal Conductivities in a Type-II Superconductor at High Magnetic Field

Authors: S. Dukan, T. P. Powell, Z. Tesanovic

Abstract: We present a calculation of the quasiparticle contribution to the longitudinal thermal conductivities as well as transverse (Hall) thermal conductivity of an extreme type-II superconductor in a high magnetic field and at low temperatures. In the limit of frequency and temperature approaching zero, both longitudinal and transverse conductivities upon entering the superconducting state undergo a r… ▽ More We present a calculation of the quasiparticle contribution to the longitudinal thermal conductivities as well as transverse (Hall) thermal conductivity of an extreme type-II superconductor in a high magnetic field and at low temperatures. In the limit of frequency and temperature approaching zero, both longitudinal and transverse conductivities upon entering the superconducting state undergo a reduction from their respective normal state values by the factor $(Γ/Δ)^2$, which measures the size of the region at the Fermi surface containing gapless quasiparticle excitations. We use our theory to numerically compute the longitudinal transport coefficient in borocarbide and A-15 superconductors. The agreement with recent experimental data on LuNi_2B_2C is very good. △ Less

Submitted 18 April, 2002; originally announced April 2002.

Comments: 8 pages +1 ps figure included in text, to appear in Phys. Rev. B

Journal ref: Physical Review B 66, 014517 (2002)