In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in polynomial time. These characterizations are also extensionally complete -- they capture all functions -- but are not intensionally complete as some polytime algorithms are rejected. This impact on expressive power is an unavoidable cost of achieving a tractable characterization. To overcome this issue, an avenue arising from security applications is to find a relaxation of noninterference based on a declassification mechanism that allows critical data to be released in a safe and controlled manner. Following this path, we present a new and intuitive declassification policy preserving FP-soundness and capturing strictly more programs than existing noninterference-based systems. We show the versatility of the approach: it also provides a new characterization of the class BFF of second-order polynomial time computable functions in a second-order imperative language, with first-order procedure calls. Type inference is tractable: it can be done in polynomial time.

翻译：在自动复杂度分析中，基于非干扰的类型系统通过可靠性静态保证良类型程序计算给定复杂度类别的函数，例如多项式时间可计算函数类FP。这些刻画在外延上是完备的——它们能捕获所有函数——但并非内涵完备，因为某些多项式时间算法会被拒绝。这种对表达能力的影响是实现易处理刻画的必然代价。为解决此问题，源自安全应用的一个途径是寻找基于去分类机制的非干扰松弛方法，该机制允许以安全可控的方式释放关键数据。遵循此路径，我们提出一种新颖直观的去分类策略，该策略保持FP可靠性并捕获比现有基于非干扰系统严格更多的程序。我们展示了该方法的普适性：它还在包含一阶过程调用的二阶命令式语言中，为二阶多项式时间可计算函数类BFF提供了新的刻画。类型推理是易处理的：可在多项式时间内完成。