立方类型论中边界填充的自动化

在使用证明助手时，自动化是解决常规证明目标（如代数表达式之间的方程）的关键。同伦类型论允许用户利用高阶归纳类型 (HITs) 和单值性原理对高阶结构（如拓扑空间）进行推理。立方类型论为 HITs 和单值性原理提供了计算支持。在立方类型论中工作的一个难点是处理高阶结构的复杂组合学，这是等式推理的无限维推广。求解这些高维方程在于构造具有指定边界的立方体。我们开发了一种简化的立方语言，在其中隔离并研究了两个自动化问题：形变求解，即尝试“扭曲”立方体以适应给定边界；以及更一般的 Kan 求解，即寻找涉及粘贴多个立方体的解。这两个问题在一般情况下都很困难——Kan 求解甚至是不可判定的——因此我们专注于在实际示例中表现良好的启发式方法。我们的语言涵盖了立方类型论的不同变体，它们在“形变理论”（即支持的形变类）上有所不同。通过将形变重新表述为偏序集映射，我们为当前研究中最复杂的形变理论（Dedekind 和 De Morgan 形变）提供了形变问题求解器。我们使用约束满足编程解决 Kan 问题，该方法独立于底层的形变理论适用。我们将算法实现为一个实验性的 Haskell 求解器，可用于自动解决立方类型论用户可能面临的许多目标。我们通过使用我们的求解器建立 Eckmann-Hilton 定理的案例研究以及各种基准测试来说明这一点。