The last 10 years has seen a surge of renewed interest in non-wellfounded proofs, from modal and predicate logics to more structural proof theoretic endeavours. A particularly fascinating direction, pioneered by the French school, is to construe circular proofs as a typing discipline for functional programs, à la Curry-Howard. Circular typing has a notable advantage against traditional (co)recursors: the operational semantics are more explicit, closer to low-level machine models with loops while nonetheless enjoying excellent metalogical properties. After foundational work of Santocanale, Baelde and Clairambault in the 2000s, the subject was considerably advanced in the 2010s by several researchers in the Paris circle.
A recurring question running through these works has been to gauge the precise computational strength of circular proofs. The obvious problem here is the non-constructive character of totality/soundness arguments for non-wellfounded proofs, a barrier to traditional approaches. In this talk I will survey a recent line of work building up a general methodology for answering such questions via a metamathematics. In particular, we manage to pin down the precise computational strengths of a circular version of system T and its extension by least and greatest fixed points.
This talk is partly based on joint work with Gianluca Curzi.
There is a large body of work on fixpoint theorems, guaranteeing the existence of fixpoints for certain functions and providing methods for computing them. This includes for instance Banachs’s fixpoint theorem, the well-known result by Knaster-Tarski that is frequently employed in computer science and Kleene iteration.
It is less clear how to compute fixpoints if the function whose (least) fixpoint we are interested in is not known exactly, but can only be obtained by a sequence of subsequently better approximations. This scenario occurs for instance in the context of reinforcement learning, where the probabilities of a Markov decision process (MDP) - for which one wants to learn a strategy - are unknown and can only be sampled. There are several solutions to this problem where the fixpoint computation (for determining the value vector and the optimal strategy) and the exploration of the model are interleaved. However, these methods work only well for discounted MDPs, that is in the contractive setting, but not for general MDPs, that is for non-expansive functions.
After describing and motivating the problem, we will in particular concentrate on the non-expansive case. There are many interesting systems who value vectors can be obtained by determining the fixpoints of non-expansive functions. Other than contractive functions, they do not guarantee uniqueness of the fixpoint, making it more difficult to approximate the least fixpoint by methods other than Kleene iteration. And also Kleene iteration fails if the function under consideration is only approximated.
We hence describe a dampened Mann iteration scheme for (higher-dimensional) functions on the reals that converges to the least fixpoint from everywhere. This scheme can also be adapted to functions that are approximated, under certain conditions.
We will in particular study the case of MDPs and consider a related problem that arises when performing model-checking for quantitative mu-calculi, which involves the computation of nested fixpoints.
This is joint work with Paolo Baldan, Sebastian Gurke, Tommaso Padoan and Florian Wittbold.