Non-uniform complexity via non-wellfounded proofs

TL;DR

This paper explores how non-wellfounded cyclic proofs can model non-uniform complexity classes like FP/poly, extending previous work on cyclic proofs and complexity characterization.

Contribution

It provides a novel proof-theoretic characterization of FP/poly using non-wellfounded cyclic proofs, linking proof irregularity to non-uniformity in complexity theory.

Findings

Characterizes FP/poly via non-wellfounded cyclic proofs.

Introduces proof-level conditions for non-uniformity.

Formalizes folklore techniques for non-uniform class characterization.

Abstract

Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)induction. Under the Curry-Howard correspondence, a cyclic proof can be seen as a typing derivation 'with loops', closer to low-level machine models, and so comprise a highly expressive computational model that nonetheless enjoys excellent metalogical properties. In recent work, we showed how the cyclic proof setting can be further employed to model computational complexity, yielding characterisations of the polynomial time and elementary computable functions. These characterisations are 'implicit', inspired by Bellantoni and Cook's famous algebra of safe recursion, but exhibit greater expressivity thanks to the looping capacity of cyclic proofs. In this work we investigate the capacity for non-wellfounded proofs, where finite presentability is relaxed, to model non-uniformity in complexity theory. In particular, we present a characterisation of the class $\mathsf{FP/poly}$ of functions computed by polynomial-size circuits. While relating non-wellfoundedness to non-uniformity is a natural idea, the precise amount of irregularity, informally speaking, required to capture $\mathsf{FP/poly}$ is given by proof-level conditions novel to cyclic proof theory. Along the way, we formalise some (presumably) folklore techniques for characterising non-uniform classes in relativised function algebras with appropriate oracles.