类型论中扩展的内部化

许多证明助理允许使用增加其表达力的功能和公理。然而，这些扩展必须谨慎使用，因为某些组合已知会导致逻辑不一致。因此，证明助理包括跟踪机制，以确保在证明开发或模块中使用了哪些扩展，从而防止同时使用不兼容的扩展。不幸的是，现有的扩展跟踪机制是外部于类型系统的。这意味着我们无法精确指定某个定义所依赖的扩展。具有更精确规格的能力意味着我们不会选择所需扩展的过度近似值，这防止了在存在不兼容扩展的情况下重用定义。此外，我们无法即使它们在不一致的方式下从未被使用的定义进行引用。一个扩展的推理原则因此无法用作对不兼容扩展属性的 metatheory。本报告中，我探索了由 Liu 等人提出的不可区分依赖类型系统 (DCOI) 用于扩展跟踪。DCOI 是一种具有依赖跟踪的依赖类型系统，其中分配给项和变量的依赖水平与其类型一起。这些依赖水平形成一个 lattice，用于描述哪些水平允许访问什么。要跟踪扩展，每个扩展集合将对应一个依赖水平，lattice 将描述扩展如何被允许相互作用。