LNL-FPC：线性/非线性不动点演算
LNL-FPC: The Linear/Non-linear Fixpoint Calculus
AI总结：
本文提出LNL-FPC类型系统，混合线性和非线性递归类型，支持类型级递归，并给出基于前嵌入技术的笛卡尔范畴模型，证明其可靠且计算充分，适用于经典及量子编程等场景。
摘要：
我们描述了一个混合线性和非线性递归类型的类型系统，称为LNL-FPC（线性/非线性不动点演算）。该类型系统支持线性类型化，这增强了程序的安全属性，但也支持非线性类型化，这使得类型系统在编程中更加方便。正如在FPC中一样，我们证明LNL-FPC支持类型级递归，这反过来又引出了项级递归。我们还为LNL-FPC提供了可靠且计算上充分的范畴模型，这些模型描述了直觉线性逻辑的子结构操作在所有非线性类型（包括递归类型）上的范畴结构。为此，我们描述了一种新技术，用于在笛卡尔范畴中求解递归域方程，通过在前嵌入上构造解来实现。该类型系统还享有隐式的弱化规则和收缩规则，我们能够通过识别所有非线性类型的典范余幺半群结构来对这些规则进行建模。我们还通过构造一大类具体模型来证明我们抽象模型的要求是合理的，这些模型不仅在经典函数式编程中找到了应用，而且在融合了线性类型的新兴编程范式中也找到了应用，例如量子编程和电路描述编程语言。
英文摘要：
We describe a type system with mixed linear and non-linear recursive types called LNL-FPC (the linear/non-linear fixpoint calculus). The type system supports linear typing, which enhances the safety properties of programs, but also supports non-linear typing as well, which makes the type system more convenient for programming. Just as in FPC, we show that LNL-FPC supports type-level recursion, which in turn induces term-level recursion. We also provide sound and computationally adequate categorical models for LNL-FPC that describe the categorical structure of the substructural operations of Intuitionistic Linear Logic at all non-linear types, including the recursive ones. In order to do so, we describe a new technique for solving recursive domain equations within cartesian categories by constructing the solutions over pre-embeddings. The type system also enjoys implicit weakening and contraction rules that we are able to model by identifying the canonical comonoid structure of all non-linear types. We also show that the requirements of our abstract model are reasonable by constructing a large class of concrete models that have found applications not only in classical functional programming, but also in emerging programming paradigms that incorporate linear types, such as quantum programming and circuit description programming languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
