VyZX：一种图形化量子语言的形式化验证

图形语言是表示计算的便捷简写，其重写规则将一个图与另一个图相关联。相比之下，证明助手严重依赖归纳数据类型，尤其在为嵌入语言赋予语义时。这给对图形语言进行形式化推理造成了障碍，因为强加归纳结构会模糊图形语言及其相应等式理论的图示本质。为弥补这一差距，我们提出 VyZX，一个用于推理归纳定义图形语言的已验证库。这些归纳构造自然源于范畴论定义。我们开发 VyZX 以验证 ZX-演算，一种用于推理量子计算的图形语言。ZX-演算带有一组保持图语义解释的图示重写规则。我们展示 VyZX 中的归纳图如何用于证明 ZX-演算重写规则的可靠性，并使用标准证明助手技术在实践中应用它们。我们还提供了一个 IDE 集成的可视化工具，供证明工程师直接以图形形式推理图示。