非良基简约证明与非均匀复杂性
Non-wellfounded parsimonious proofs and non-uniform complexity
AI总结:
本文提出捕获FP和FP/poly的非良基简约证明系统,通过多项式模连续性证明可靠性,并利用带建议的图灵机编码证明完备性,同时得到多种有限证明系统的特征化结果。
摘要:
本文研究了在简约逻辑(线性逻辑的一种变体,其中指数模态!被解释为有限数据上的流构造子)背景下循环和非良基证明的复杂性理论方面。我们提出了捕获类$\mathbf{FP}$和$\mathbf{FP}/\mathsf{poly}$的非良基简约证明系统。可靠性通过连续消割的多项式模连续性建立。完备性依赖于在基于简约逻辑的类型赋值系统内对带建议的多项式图灵机的编码。作为我们证明方法的副产品,我们为各种有限证明系统建立了一系列特征化结果。
英文摘要:
In this paper we investigate the complexity-theoretical aspects of cyclic and non-wellfounded proofs in the context of parsimonious logic, a variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. We present non-wellfounded parsimonious proof systems capturing the classes $\mathbf{FP}$ and $\mathbf{FP}/\mathsf{poly}$. Soundness is established via a polynomial modulus of continuity for continuous cut-elimination. Completeness relies on an encoding of polynomial Turing machines with advice within a type assignment system based on parsimonious logic. As a byproduct of our proof methods, we establish a series of characterisation results for various finitary proof systems.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。