Silq：具有安全反计算与直观语义的高级量子语言

论文信息（2020，PLDI）：Benjamin Bichsel、Maximilian Baader、Timon Gehr、Martin Vechev。DOI；作者页面

工作

Silq 针对高级量子语言中临时值必须显式反计算的问题，提供安全的自动反计算机制。它允许像经典程序一样隐式丢弃临时值，同时通过类型系统注解拒绝不符合物理语义的程序。论文报告 Silq 程序相较 Q# 与 Quipper 更短，并使用更少的量子原语。

主要贡献

• 提出支持安全自动反计算的高级量子语言。
• 用类型系统注解维护语义的物理可实现性。
• 让临时值的隐式丢弃拥有直观的程序语义。
• 通过实验比较程序长度和量子原语数量。

局限与适用范围

语言的安全规则依赖其类型系统、语义和编译器实现；代码更短不等于电路在所有后端都更快或更可靠。论文实验比较的是选定程序与语言，不能自动外推到所有算法、噪声模型、硬件门集或完整形式化证明。

与其他工作的关系

Silq 延续QPL与量子 Lambda 演算的类型化高级语言路线，并与Quipper形成语言工程对比。它的自动反计算问题也连接线性类型系统对量子资源使用的约束。

原论文

Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev, Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics, in PLDI 2020, DOI: 10.1145/3385412.3386007. 作者页面