有限性结构的输运及其应用
Transport of finiteness structures and applications
摘要:
我们描述了有限性空间的一般构造,它包含了线性逻辑的所有正连接子的解释。然后,我们展示了如何应用这种构造来证明有限性空间范畴中特定函子的最小不动点的存在性:这些函子包括沿着系统T的一致性语义的懒惰递归代数数据集的关系解释中所涉及的函子。
英文摘要:
We describe a general construction of finiteness spaces which subsumes the interpretations of all positive connectors of linear logic. We then show how to apply this construction to prove the existence of least fixpoints for particular functors in the category of finiteness spaces: these include the functors involved in a relational interpretation of lazy recursive algebraic datatypes along the lines of the coherence semantics of system T.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。