MARRYing the analyses of feasible algorithms and problems (MARRY)
Royal Society International Exchanges Grant, IES\R3\223051
Wider Research Context. Pure foundational research provides seeds for successful applications. A notable example in the context of our proposal is a tool, RaML: While based on implicit characterisations of feasible computation by Martin Hofmann to provide elegant descriptions, RaML is nowadays the most advanced tool to estimate resource consumptions of OCaml programs. Also the direction from applications to theory is significant. Deeply rooted in practical questions, Ashish Tiwari defined a restrictive class of linear loop programs and initiated an ongoing study into their termination. It emerged that this links intimately to Skolem's problem, a deep problem in number theory that attracted comments from Terence Tao.
Objectives. Inspired by these examples, we aim to study results between application-oriented areas in program analysis and foundational aspects in proof theory. More precisely, the analysis of feasible algorithms is concerned with the development of (often) automated methods to infer the runtime costs of programs. On the other hand, complexity theory, the study of the inherent complexity of given computational problems, is naturally couched in theories of Bounded Arithmetic (BA). Thus, questions of feasibility of algorithms and problems become questions of provability in BA.
Methods. In an initial phase of the project, we aim to validate our approach by investigating the transfer of methods in the study of rewriting systems and the analysis of proofs in BA. A second phase will explore methods used in the study of BA and program analysis with the aim to develop a long-term programme that can be sustained by follow-up funding.
Duration: 2 Years
The project started on January 1, 2023.Meetings
- July 7--21, 2023, Swansea University, UK
Members
The project is coordinated by- Arnold Beckmann ()
- Georg Moser (Theoretical Computer Science; University of Innsbruck)