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.
翻译:现在,在各种环境,特别是具有(co)诱导形式(co)的类型系统中,正在越来越多地使用循环和非证据证据来建立元结果。在Curry-Howard通信中,周期性证据可以被视为“带环的”打字衍生,更接近于低级机器模型,因此包含一个高度直观的计算模型,尽管具有极好的元性。在最近的工作中,我们展示了如何进一步利用周期性证据设置来建立计算复杂性模型,从而产生多元时间和基本可调解函数的特性。这些特性是“不完全的 ”, 受Bellantoni 和Cook著名的安全循环的代数的启发, 但是由于周期性证据的循环能力而表现出更大的直观性。 在这项工作中,我们调查了非可靠证据的能力,在有限的现今性方面,在复杂理论中模拟不统一性。我们特别展示了等级 $\mathfsf{FP/poly 的直观性特征, 由Bellantonito colal calal orizal colal oral-deal ormal-de laphyal lade) 和非正解的正统性平流法化, 在非正统的顺序中, 和正统性平流法性平流法性是非正序的平流法化的平流法化的平流法化的平流法化的平流的平流法性, 。