论文标题
部分可观测时空混沌系统的无模型预测
Controlling unfolding in type theory
论文作者
论文摘要
我们提出了一种新的机制，用于控制依赖类型理论中定义的展开。传统上，证明助手允许用户指定每个定义在其余的开发中是否不能展开；为了推理这些定义，通常需要进行展开定义，但是过多的展开可能会导致证明脆弱的证明和很大的证明目标。在我们的系统中，默认情况下的定义不是不展开的，但是用户可以选择性地以当地方式展开它们。我们通过详细说明具有扩展类型的核心类型理论来证明我们的机制是合理的，这是在同型类型理论背景下首次引入的结缔组织。我们证明了核心演算的标准化定理，并已在Cooltt证明助手中实施了系统，为此提供了理论和实际证据。
We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it.
