AI 中文总结
研究连续变量量子计算（CVQC）语义基础未充分发展的问题，通过开发核心CV量子编程语言的形式语义及验证方法，选择封闭正二次形式作语义谓词，经案例研究验证，为CVQC提供了可靠语义基础。
AI 中文摘要
连续变量量子计算（CVQC）是一种测量产生连续域值的计算范式。它既是用于对物理量子系统建模的便捷计算框架，也是基于量子光学的硬件平台的良好抽象。然而，CVQC的语义基础仍未充分发展。为填补这一空白，我们为核心CV量子编程语言开发了形式语义以及程序正确性的可靠验证方法。这项工作的主要贡献是分离出一个行为良好的定量谓词域，该域具有足够的表现力来适应无限维连续设置中出现的无界值。具体而言，我们选择封闭正二次形式作为语义谓词，在一个有序对象中表示有限期望、有限域和无限惩罚。我们通过证明语义谓词满足包括最弱前置条件定义在内的理想封闭属性来验证我们的选择。我们用两个案例研究验证了我们的设计，包括一个基于著名的GKP纠错码的例子，为此我们建立了二阶矩界。
英文摘要
Continuous-variable quantum computing (CVQC) is a computing paradigm in which measurements yield values over a continuous domain. CVQC is both a convenient omputational framework for modeling physical quantum systems, and a good abstraction for hardware platforms based on quantum optics. Yet, the semantic foundations of CVQC remain underdeveloped. To address this gap, we develop a formal semantics for a core CV quantum programming language, and sound verification methods for program correctness. A main contribution of this work is to isolate a well-behaved quantitative predicate domain that achieves sufficient expressiveness to accommodate unbounded values as they arise in the infinite-dimensional, continuous setting. Specifically, we choose closed positive quadratic forms as semantic predicates, representing finite expectations, domains of finiteness, and infinite penalties in one ordered object. We validate our choice by establishing that our semantic predicates satisfy desirable closure properties including the definition of weakest preconditions. We validate our design with two case studies, including an example based on the celebrated GKP error-correcting code, for which we establish a second moment bound.
Comments119 pages,2 figures
