具有无界循环的混合量子程序的有效量子霍尔逻辑

尽管量子硬件仍然有限，但具有复杂控制结构（包括无界循环）的混合量子-经典算法正在涌现，这给量子程序分析带来了新的挑战，包括对给定程序资源消耗的准确估计。同时，诸如符号执行等精确分析技术在很大程度上忽略了混合化和无界递归。另一方面，当前普遍支持它们的量子霍尔逻辑在表达能力上有所欠缺，并且错失了可以在半自动工具中实现的高效计算等式推理。这留下了一个有待填补的空白。在这项工作中，我们通过首个结合有效功能验证和资源（终止或成本）估计的半自动静态分析解决方案来应对这一挑战，该方案适用于具有无界循环的混合量子程序。为此，我们引入了整数混合路径和（IHPS），将路径和扩展以处理无界while循环，作为程序可能执行的表示。还提出并说明了通过循环不变量确定终止和预期资源消耗的通用策略，并通过几个示例进行了说明。最后，该解决方案被实现为一个半自动的Haskell程序。这项工作是朝着为混合量子程序设计完整的静态资源分析工具迈出的第一步，这对于现实世界量子计算的发展至关重要。