技术摘要：Granthi：通过幺正布线实现的高阶量子编程

1. 问题陈述

现有的量子编程语言通常采用一种分裂式架构，其中高阶结构（函数、控制抽象、程序生成器）完全驻留在经典的宿主语言中，而量子层则被限制在对量子比特和寄存器的一阶操作上。这种设计限制了对量子程序本身的抽象；量子值无法作为参数传递、作为结果返回，也无法在更高阶的构造中进行组合。

此外，经典的抽象机制（模式匹配、分支分析、迭代）依赖于破坏性的检查与丢弃未使用的备选项，这会导致控制流坍缩。这些原则与纯幺正的量子设定是不兼容的，因为在量子设定中，数据不能被自由地检查、复制或丢弃，否则会不可逆地改变程序的行为。因此，目前缺乏一种能够支持真正的更高阶相干控制（如量子开关/quantum switch），同时又能保持纯幺正语义并编译为静态电路的编程语言。

2. 方法论

本文提出了 Granthi，一种纯幺正的高阶量子编程语言，其构建基于三个核心设计承诺：

1. 量子程序是一等公民： 量子程序是一等值，可以被传递、返回并进行相干组合。
2. 标签保持型路由（Tag-Preserving Routing）： 加性结构被定义为标签保持型路由，而非观测分支。这使得控制逻辑可以在叠加态中保持存在，而不发生坍缩。
3. 有限标签类型： 为程序员提供具有命名可逆操作的有限标签类型，这些类型会被细化为扁平的 $n$ 进制和（$n$-ary sums），而不使用递归类型或表示隐藏。

核心语言与语义

• 线性 $\lambda$-演算基础： 核心是一个包含张量积 ($\otimes$)、相干和 ($\oplus$) 以及线性函数空间 ($\multimap$) 的线性 $\lambda$-演算。基类型 $\mathbb{b}$ 是一个一维种子；有限维系统通过相干和构建（例如，$QBool := \mathbb{b} \oplus \mathbb{b}$）。
• 边界幺正性（Boundary Unitarity）： 核心语义创新在于“边界视图”。类型为 $A \multimap B$ 的项被视为一个具有结构化接口的开放电路片段。应用（Application）被解释为一种连通性结构（布线接口），而非消耗资源的归约步骤。每个类型良好的项都对应其边界接口上的一个幺正算子。
• 规范化与确定性： 该语言强制执行 $\beta/\eta$-稳定规范。系统证明了每个闭合且类型良好的项在定义相等意义下都有唯一的范式，从而确保源层面的重排（规范化）不会改变编译后的幺正电路。
• 量子扩展： 核心通过认证的对合算子（自逆算子）和 Exp 项构造器进行了增强，后者通过矩阵指数化 ($e^{i\theta J}$) 生成连续的幺正族。这允许在不引入测量或混合态的情况下实现相位移动和受控操作。

编译

Granthi 系统实现了一个端到端的编译器：

1. 细化（Elaboration）： 表面程序（使用 OCaml DSL 编写）被细化为无绑定器（binder-free）的核心中间表示（IR）。
2. 电路生成： 编译器通过 pytket 后端，将幺正边界的布线实现为物理量子比特布局上的静态量子电路。
3. 线缆布局（Wire Layouts）： 编译器针对涉及标签寄存器和共享负载包的求和类型，使用特定的线缆编码。结构同构（结合律、对称律、分配律）被编译为纯粹的线缆置换（zero gates），而相干控制构造（如 case）则编译为作用于标签寄存器的受控门。

3. 核心贡献

• 高阶幺正语义： Granthi 提供了第一个关于高阶结构内在属于量子层（而非局限于经典宿主）的编程语言解释。它证明了高阶可逆性是转移到了暴露的接口而非封闭的数据之上的普通幺正性。
• 对组合的相干控制： 该语言支持将**量子开关（Quantum Switch）**作为可定义的项。量子开关将两个操作的组合顺序置于叠加态中，它被编译为一个静态电路，证明了这类高阶效应是可编程的，并且在物理上是可实现的。
• 控制流上的干涉： 该语言支持对控制流历史的干涉（例如，带有相位标记的可逆短路合取），这是一种没有经典类比的现象，通过线程显式的见证线（witness wires）并在特定分支上施加相位来实现，而不进行观测。
• 有限控制数据类型： 系统引入了面向程序员的有限标签类型（例如循环群 $\mathbb{Z}_5$）及命名的可逆操作。这些类型被细化为核心的求和与布线机制，使得领域特定的控制空间（如群相干模式匹配）能够高效编译（例如，$n$ 进制分派的复杂度为 $O(\log n)$ 个门）。
• 形式化保证： 本文确立了规范化、确定性和边界幺正性定理。它证明了假设后端原语正确的前提下，编译后的电路等于通过布局同构传输的语义幺正算子。

4. 结果

作者将 Granthi 实现为以 OCaml DSL 为基础、以 Python 作为编译器目标（针对 pytket）的系统。原型在多个示例上得到了验证：

• 量子开关： 运行示例被编译为一个 8 量子比特的静态电路，实现了因果顺序的叠加。
• 受控操作： 实现了一致受控应用和 $n$ 进制受控分派（例如 SELECT 组合子），展示了高效的门计数（例如，$n$ 进制求和仅需 $O(\log n)$ 个标签翻转）。
• 标准算法： 系统成功编译并验证了包括 Deutsch–Jozsa、隐子群问题、Simon、Bell 态和 GHZ 态在内的标准算法。
• 门成本分析： 实现确认了乘法和结构化操作编译为零门（纯布线），而量子原语和相干控制构造则引入必要的门。例如，量子开关编译为 $2 + 2(|f| + |g|)$ 个门。

5. 意义与范围

本文将 Granthi 定位为一个受约束的幺正核心，用于研究量子编程中的高阶抽象，且独立于测量与经典反馈。

• 范围： 该语言有意排除了测量、混合态、经典反馈和递归类型。这些排除对于维持“每个类型良好的项都代表一个边界幺正算子并能编译为静态电路”这一不变性至关重要。
• 定位： Granthi 不同于现有的语言（如 Quipper 或 Q#），因为它将高阶结构置于对象语言而非宿主语言中。它也不同于 Qunity，因为它将正交性植入加性类型结构中，而非依赖于通用的正交判断。
• 未来方向： 作者承认，一个完整的量子编程系统需要将核心扩展到包含测量、混合态语义和更丰富的抽象数据。Granthi 被视为一个基础性的步骤，旨在理解在引入硬件约束和测量效应之前，量子程序应当如何构建。

总之，Granthi 证明了在纯幺正框架内，高阶量子控制在物理上是有意义的且是可编程的，它为控制流本身可以参与干涉的量子程序提供了一个形式化且可执行的基础。