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.
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.
In our previous work 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 Neumann algebra of bounded linear operators. 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. Our goal is to build a model of computation based on logic via Currry-Howard correspondence. Towards this end we can think of completely positive *-unital maps of Horn clauses as function types representing modus ponens (equation (19)). Recursions that result from inductive reasoning has a quantum analogue in terms of sequence of *-homomorphisms induced by completely positive *-unital maps (equation (18)). 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) 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 theorem proving as a quantum stochastic process in Heisenberg picture of quantum mechanics, a sequence of goals to be proved, using backward chaining.
The stochastic nature of quantum communication protocols naturally lends itself for expression via probabilistic logic languages. In this work we describe quantized computation using Horn clauses and base the semantics on quantum probability. Turing computable Horn clauses are very convenient to work with and the formalism can be extended to general form of first order languages. Towards this end we build a Hilbert space of H-interpretations and a corresponding non commutative von Neumann algebra of bounded linear operators. We demonstrate the expressive power of the language by casting quantum communication protocols as Horn clauses.
We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.
We describe a quantum mechanics based logic programming language that supports Horn clauses, random variables, and covariance matrices to express and solve problems in probabilistic logic. The Horn clauses of the language wrap random variables, including infinite valued, to express probability distributions and statistical correlations, a powerful feature to capture relationship between distributions that are not independent. The expressive power of the language is based on a mechanism to implement statistical ensembles and to solve the underlying SAT instances using quantum mechanical machinery. We exploit the fact that classical random variables have quantum decompositions to build the Horn clauses. We establish the semantics of the language in a rigorous fashion by considering an existing probabilistic logic language called PRISM with classical probability measures defined on the Herbrand base and extending it to the quantum context. In the classical case H-interpretations form the sample space and probability measures defined on them lead to consistent definition of probabilities for well formed formulae. In the quantum counterpart, we define probability amplitudes on Hinterpretations facilitating the model generations and verifications via quantum mechanical superpositions and entanglements. We cast the well formed formulae of the language as quantum mechanical observables thus providing an elegant interpretation for their probabilities. We discuss several examples to combine statistical ensembles and predicates of first order logic to reason with situations involving uncertainty.
The main contribution of the present paper is the introduction of a simple yet expressive hybrid-dynamic logic for describing quantum programs. This version of quantum logic can express quantum measurements and unitary evolutions of states in a natural way based on concepts advanced in (hybrid and dynamic) modal logics. We then study Horn clauses in the hybrid-dynamic quantum logic proposed, and develop a series of results that lead to an initial semantics theorem for sets of clauses that are satisfiable. This shows that a significant fragment of hybrid-dynamic quantum logic has good computational properties, and can serve as a basis for defining executable languages for specifying quantum programs. We set the foundations of logic programming in this fragment by proving a variant of Herbrand's theorem, which reduces the semantic entailment of a logic-programming query by a program to the search of a suitable substitution.
At the beginning of the last century, the theory of quantum optics arose and led to a revolution in physics, since it allowed the interpretation of many unknown phenomena and the development of numerous powerful, cutting edge engineering applications, \nsuch as high precision laser technology. The analysis and verification of such applications and systems, however, are very complicated. Moreover, traditional analysis tools, e.g., simulation, numerical methods, computer algebra systems, and paper-and-pencil approaches are not well suited for quantum systems. In the last decade, a new emerging verification technique, called formal methods, became common among engineering domains, and has proven to be effective as an analysis tool. Formal methods \nconsist in the development of mathematical models of the system subject for analysis, and deriving computer-aided mathematical proofs. In this thesis, we propose a framework for the analysis of quantum optics based on formal methods, in particular theorem proving. The framework aims at implementing necessary quantum mechanics and optics concepts and theorems that facilitate the modelling of quantum optical devices and circuits, and then reason about them formally. To this end, the framework \nconsists of three major libraries: 1) Mathematical foundations, which mainly contain the theory of complex-valued-function linear spaces, 2) Quantum mechanics, which develops the general rules of quantum physics, and 3) Quantum Optics, which \nspecializes these rules for light beams and implements all related concepts, e.g., light coherence which is typically emitted by laser sources. On top of these theoretical foundations, we build a library of formal models of a number of optical devices commonly \nused in quantum circuits, including, beam splitters, light displacers, and light phase shifters. Using the proposed framework, we have been able to formally verify common quantum optical computing circuits, namely the Flip gate, CNOT gate, and Mach-Zehnder interferometer.