Skip to content
Institute for Logic and Data Science
Menu
  • Home
  • Research
    • Research Projects
    • Scientific Seminars
  • Events
  • People
  • Partners
  • About
    • About Us
    • Support us
    • Executive Board
    • Contact
Menu

Proof Mining Seminar

The Proof Mining Seminar is a joint LOS/ILDS seminar, featuring talks on recent results in proof mining.

Proof mining is a paradigm of research, concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of highly infinitary principles. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of a quantitative nature, such as algorithms and effective bounds, as well as of a qualitative nature, such as uniformities in the bounds or weakenings of the premises.

All seminars, except where otherwise indicated, will be on Wednesdays between 16:00 and 18:00, Bucharest time. The seminars are held remotely.

To receive announcements about the seminar, please send an email to proof-mining-seminar@ilds.ro.

Organizers: Ulrich Kohlenbach, Laurențiu Leuștean, Andrei Sipoș

Past Talks in 2022-2023


Wednesday, July 26, 2023

Pedro Pinto (TU Darmstadt)

The strange case of Dykstra’s algorithm

Abstract:

In this talk we discuss the proof mining treatment of the strong convergence of Dykstra’s algorithm.

Halpern’s iterative method is probably the most common approach to strongly approximate fixed points of nonexpansive maps. The canonical proof (pliable to many other results) establishing strong convergence of the iteration relies on a crucial use of sequential weak compactness. It is well-understood how a proof-theoretical approach allows for the elimination of the compactness arguments via bounded collection principles, thus allowing for simple quantitative data in the analysis of such proofs.

Here, we focus on a different iterative method. Generalizing the alternating projection method, Dykstra’s algorithm strongly approximates the optimal solution of the convex feasibility problem. Similarly to Halpern, the strong convergence of Dykstra’s method makes crucial uses of compactness principles substantiated by arithmetical comprehension. Yet, as the iterative schema has no connection with Halpern’s definition and the proof follows a completely different structure, it was not known whether the removal of the compactness arguments would be possible and thus, a priori, we were only guaranteed to obtain quantitative data defined by bar-recursive functionals. Strikingly, still here, it was possible to bypass the use of arithmetical comprehension and bar-recursive functionals. We will discuss the recent quantitative analysis of Dykstra’s convergence proof and explain how it was possible to avoid the compactness principles crucial in the original proof.

References:
[1] P. Pinto, On the finitary content of Dykstra’s cyclic projections algorithm. arXiv:2306.09791 [math.OC], 2023.


Past Seminars

  • LOS/ILDS Proof Mining Seminar in 2021-2022

Follow us

Subscribe to our RSS feed.

Subscribe

Support us

Looking for ways to support our research? Check out all the different opportunities!

Contact us

Interested in logic and/or data science research? Send an email to contact@ilds.ro

Institute for Logic and Data Science
Str. Popa Tatu nr. 18
010805 Bucharest, Romania
contact@ilds.ro

© 2023 Institute for Logic and Data Science | Powered by Minimalist Blog WordPress Theme