Cockett-Seely极化对策的复杂性
On the complexity of Cockett-Seely polarized games
摘要：
本文讨论了（初始）Cockett-Seely极化博弈逻辑中极化加、乘、指数公式可证性的复杂性。复杂性最终是基于在公式中找到策略的复杂性，对于极化加法公式，在最坏情况下，其大小是线性的。拥有相继式的证明相当于拥有内部宿主对象的策略。为了证明内孔对象的大小可以比原始公式的大小指数级地大，我们开发了用于计算乘法公式的大小的技术。可以利用内部hom对象的结构，并且使用动态规划技术，可以将在这样的公式中找到策略的成本降低到原始公式的大小的乘积的量级。动态技术的使用促使考虑游戏作为非循环图，我们展示了如何计算这些图形游戏的乘法和加法片段的大小，因此，使用这种动态规划方法确定其可证明性的成本。论文的最后一部分指出，尽管公式的表面复杂性，但对于具有所有连接词（加法、乘法和指数）的初始极化逻辑，有一种确定公式大小为\emph{linear}的可证明性的方法。
英文摘要：
In this paper the complexity of provability of polarized additive, multiplicative, and exponential formulas in the (initial) Cockett-Seely polarized game logic is discussed. The complexity is ultimately based on the complexity of finding a strategy in a formula which is, for polarized additive formulas, in the worst case linear in their size. Having a proof of a sequent is equivalent to having a strategy for the internal-hom object. In order to show that the internal-hom object can have size exponentially larger than the formulas of the original sequent we develop techniques for calculating the size of the multiplicative formulas. The structure of the internal hom object can be exploited and, using dynamic programming techniques, one can reduce the cost of finding a strategy in such a formula to the order of the product of the sizes of the original formulas. The use of dynamic techniques motivates the consideration of games as acyclic graphs and we show how to calculate the size of these graph games for the multiplicative and additive fragment and, thus, the cost of determining their provability using this dynamic programming approach. The final section of the paper points out that, despite the apparent complexity of the formulas, there is, for the initial polarized logic with all the connectives (additives, multiplicatives, and exponentials) a way of determining provability which is \emph{linear} in the size of the formulas.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
