基于二次量化Horn子句的形式验证
Formal Verification using Second-Quantized Horn Clauses
摘要：
在我们以前的工作[1]中，我们使用Horn子句描述了量子计算，并基于语义，称为纠缠语义作为指称和分布语义的推广，并通过利用经典随机变量具有量子分解的关键洞察力将其建立在量子概率上。为此，我们建立了H-解释的Hilbert空间和相应的有界线性算子的非交换von Neu- mann代数[2]。在这项工作中，我们扩展的形式主义使用二次量子化的霍恩条款，描述过程，如海森堡演化的光路，量子行走，和量子滤波器在一个正式的可验证的方式。我们将我们的系统基于测度论方法来处理无限维系统，并通过在这种语言中铸造用于描述互连量子系统（QNET）[5]的代数来展示形式主义的表达能力。由全称或存在量词限定的Horn子句的变量可以用于描述光学部件的参数，诸如分束器散射路径、谐振腔失谐、激光束的强度或这些部件的输入和输出端口。在这个非交换框架中的突出条款是Weyl谓词，即量子随机微积分、鞅和共轭布朗运动紧表示量子场波动统计的语言中玻色子-福克空间上的算子。我们制定的- orem证明作为一个量子随机过程，更确切地说是一个鞅，在海森堡图片的量子力学，一系列的目标被证明，在Herbrand基地。
英文摘要：
In our previous work [1] we described quantized computation using Horn clauses and based the semantics, dubbed as entanglement semantics as a generalization of denotational and distribution semantics, and founded it on quantum probability by exploiting the key insight classical random variables have quantum decompositions. Towards this end we built a Hilbert space of H-interpretations and a corresponding non commutative von Neu- mann algebra of bounded linear operators [2]. In this work we extend the formalism using second-quantized Horn clauses that describe processes such as Heisenberg evolutions in optical circuits, quantum walks, and quantum filters in a formally verifiable way. We base our system on a measure theoretic approach to handle infinite dimensional systems and demonstrate the expressive power of the formalism by casting an algebra used to describe interconnected quantum systems (QNET) [5] in this language. The variables of a Horn clause bounded by universal or existential quantifiers can be used to describe parameters of optical components such as beam splitter scattering paths, cavity detuning from resonance, strength of a laser beam, or input and output ports of these components. Prominent clauses in this non commutative framework are Weyl predicates, that are operators on a Boson Fock space in the language of quantum stochastic calculus, martingales and conjugate Brownian motions compactly representing statistics of quantum field fluctuations. We formulate the- orem proving as a quantum stochastic process, more precisely a martingale, in Heisenberg picture of quantum mechanics, a sequence of goals to be proved, on the Herbrand base.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
