有语境和无语境的有限类型理论
Finitary type theories with and without contexts
摘要：
我们给出了有限类型理论的定义，它包含了许多依赖类型理论的例子，如马丁-洛夫类型理论的变体，简单类型理论，一阶和高阶逻辑，同伦类型理论。我们证明了几个一般的元定理有限型理论：弱化，容许的替代和实例化的元变量，可导性的前提，唯一性的类型，反演原则。然后，我们给出了第二个制定有限型理论，其中没有明确的背景。相反，自由变元显式地使用它们的类型进行注释。我们提供有限类型理论之间的翻译，没有上下文，从而表明，他们有相同的表达能力。上下文无关类型理论在Andromeda 2证明助手的核心中实现。
英文摘要：
We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-Löf type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly annotated with their types. We provide translations between finitary type theories with and without contexts, thereby showing that they have the same expressive power. The context-free type theory is implemented in the nucleus of the Andromeda 2 proof assistant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
