基于分阶段取决器张量形状的编译时张量形状检查

在编写涉及矩阵或张量的程序时，理想情况下希望在实际计算之前消除张量形状不一致（即矩阵大小的泛化）的问题。为了此目的，一些语言提供依赖类型如Mat m n，另一些则提供细化类型来跟踪形状的谓词。尽管这些方法在理论上已经成熟，但由于需要为判断类型相等或子类型提供证明，这些方法往往不够便捷用于持续的软件开发；即使是自动证明，也常常不适合由于其不可预见的时间消耗。在此基础上，我们提供一种替代形式化方法，利用分阶段技术。在我们观察到许多典型情况下，形状一致性的条件可以在实际张量计算运行前提取出来的基础上，我们通过在编译时计算中求值的断言来确保此类一致性，而非通过证明。在这种形式化下，我们可以在几乎静态的意义上验证一致性，以致于关于张量形状的不一致将在编译时计算中作为断言失败立即被检测到。我们的工作实现了数学保证，成功生成的代码始终符合张量形状一致性。此外，为了大大减少添加形状或阶段相关描述的负担，我们（1）允许形状相关参数是隐式的，并以最佳努力方式推断它们，（2）提供一种非分阶段的表面语言，似乎类似于普通依赖类型语言，并将其程序翻译成分阶段核心语言。通过原型实现，我们确认该语言足够表达，可以验证包括多个ocaml-torch示例在内的多个程序。