多形依赖类型理论中的不可导结果
Non-Derivability Results in Polymorphic Dependent Type Theory
AI总结：
本文研究了多形依赖类型理论中归纳原理和共归纳原理的可导性问题，发现参数quotient类型无法在λP2中定义，而流类型不具有共归纳原理，函数扩展性对归纳原理的可证明性至关重要。
摘要：
在纯构造算术（CC）中，可以定义数据类型和这些类型上的函数，并且有一个强大的高阶逻辑来推理这些函数和数据类型。这是由于impredicativity和依赖类型的结合，而大多数这些特性已经在多形（第二阶）依赖类型理论λP2中可以观察到。impredicative编码数据类型（在λP2或CC中）是强大的，但并不完全令人满意：例如，归纳原理无法被证明。事实上，可以证明，对于任何可能的数据类型表示，归纳原理都无法被证明。在最近的一篇论文中，Awodey、Frey和Speight展示了在扩展的λP2中加入Sigma类型、身份类型和唯一身份证明后，可以定义数据类型，其归纳原理可以被证明。更近期的研究表明，在这种扩展的λP2中，也可以用quotient类型定义具有适当归纳原理的类型，并且使用quotient类型可以定义具有适当共归纳原理的共归纳类型。这留下了一些开放的问题：quotient类型是否无法在原始λP2中定义？而共归纳类型是否无法在λP2中获得强共归纳原理？从另一角度考虑：用于使归纳和共归纳工作所需的扩展是否真的必要？在本文中，我们对这些问题给出了部分答案：参数quotient类型无法在λP2中定义，而众所周知的可定义流类型不具有共归纳原理。对于后者问题，我们证明，如果仅将λP2扩展为Sigma类型和带有唯一身份证明的身份类型，仍然无法为自然数证明归纳原理。因此，函数扩展性在使归纳原理可证明方面至关重要。我们通过研究λP2的模型来证明这些结果，其中代表这些原理的类型为空，因此这些模型作为原理可导性的反例。
英文摘要：
In the pure Calculus of Constructions (CC) one can define data types and function over these, and there is a powerful higher order logic to reason over these functions and data types. This is due to the combination of impredicativity and dependent types, and most of these features can already be observed in polymorphic (second order) dependent type theory $λ$P2. The impredicative encoding of data types (in $λ$P2 or CC) is powerful but not fully satisfactory: for example, the induction principle is not provable. As a matter of fact, it can be shown that induction is not provable for whatever possible representation of data types. In a recent paper, Awodey, Frey and Speight show that in an extension of $λ$P2 with Sigma-types, identity types with uniqueness of identity proofs and function extensionality, it is possible to define data types for which the induction principle is provable. More recently it has been shown that in this extension of $λ$P2, also quotient types can be defined with the proper induction principle, and, using quotient types, coinductive types can be defined with the proper coinduction principle. This leaves various questions open: Are quotient types with induction principle not definable in the original $λ$P2? And how about coinductive types, is it impossible to get a strong coinduction principle in $λ$P2? Looking at it from the other side: which of the extensions used are really needed to make induction and coinduction work? In this paper, we contribute partial answers to these questions: parametric quotient types are not definable in $λ$P2 and the well-known definable stream type does not have a coinduction principle. For the latter question we show that, if we just extend $λ$P2 with Sigma-types and identity types with uniqueness of identity proofs, we still cannot prove an induction principle for the natural numbers. So function extensionality is crucial in making induction provable. We show these results by studying models of $λ$P2 where the types representing these principles are empty, so these models act as counter models to the derivability of the principles.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
