线性依赖类型理论中的反证法
Impredicativity in Linear Dependent Type Theory
AI总结：
本文通过构建线性依赖类型理论的实现模型，引入了具有双重解码操作的宇宙，实现了线性归纳类型的编码，并展示了相关性原则。
摘要：
我们从线性组合子代数构建了线性依赖类型理论的实现模型。该模型促使类型理论中增加了一些补充内容。特别是，我们添加了一个具有两个解码操作的宇宙：一个将代码转换为笛卡尔类型，另一个将代码转换为线性类型。该宇宙在反证法意义上是封闭的，因为它在大型笛卡尔依赖积和大型线性依赖积下都封闭。我们还添加了一个规则，用于确保将线性术语转换为笛卡尔术语的注入性。在所有补充之后，我们能够编码（线性）归纳类型。作为案例研究，我们考虑了一个线性类型的列表类型，并展示我们的编码具有相关性原则。实现模型的构建在证明助手Rocq中完全形式化。
英文摘要：
We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
