有限二阶相干空间周围
Around finite second-order coherence spaces
摘要：
指称语义的许多应用，如高阶模型检验或规范化的复杂性，依赖于单态类型系统的有限语义。我们表现出这样一个有限的语义多态的纯线性语言：更确切地说，我们表明，在吉拉德的语义二阶线性逻辑使用连贯空间和正常函子，乘法加法公式的表示是有限的。这个模型也是有效的，在这个意义上，表示的公式和证明是可计算的，因为我们显示。我们还建立了类似的结果为二阶扩展的Ehrhard的hypercoherency;而有限性持有相同的原因，在相干空间，有效性提出了额外的困难。最后，我们讨论了应用我们的工作，在线性（或仿射）逻辑中的隐式计算复杂性。鉴于这些应用，我们研究基数和复杂性的界限，在我们的有限语义。
英文摘要：
Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We exhibit such a finite semantics for a polymorphic purely linear language: more precisely, we show that in Girard's semantics of second-order linear logic using coherence spaces and normal functors, the denotations of multiplicative-additive formulas are finite. This model is also effective, in the sense that the denotations of formulas and proofs are computable, as we show. We also establish analogous results for a second-order extension of Ehrhard's hypercoherences; while finiteness holds for the same reason as in coherence spaces, effectivity presents additional difficulties. Finally, we discuss the applications our our work to implicit computational complexity in linear (or affine) logic. In view of these applications, we study cardinality and complexity bounds in our finite semantics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
