Higher-order quantum logics

M. Dalla Chiara, Roberto Giuntini, Richard J. Greechie

Kenji Tokuo

Pablo J. Arrighi, Gilles Dowek B

We introduce a minimal language combining both higher-order computation and linear algebra. Roughly, this is nothing else than the Lambda-calculus together with the possibility to make linear combinations of terms a.t+b.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in field of quantum computation, which we show can be easily encoded in the calculus, as well as in other domains such as the interpretation of linear logic. Finally we prove the confluence of the calculus, this is our main result. Keywords: quantum programming language, quantum control, quantum logic, probabilistic and quantitative analysis, rewriting techniques.

Dov M. Gabbay, Kurt Engesser, Daniel J. Lehmann

Steven French, Décio Krause

Abstract Traditionally by ‘quantum logic’, one understands the study of the lattice of the subspace of Hilbert space. Here, ‘quantum logic’ is taken to be the underlying logic of quantum physics. Following Schrödinger’s idea that the standard concept of identity cannot be applied to quantum objects, a kind of ‘non-reflexive’ logic called Schrödinger logic is presented, in which the reflexive law of identity is taken not to apply. First order Schrödinger logics are presented, and extended to higher order logics and also to an intensional logic. Classical semantics is presented, and a weak completeness theorem is sketched. The last part of the chapter covers a logic of sortal predicates for which a quasi-set semantics is delineated. This completes the formal framework capable of accommodating quantum non-individuality and thus the initial understanding of Born, Heisenberg, and Schrödinger, as well as the second horn of the above metaphysical underdetermination, can be formally represented.

Julien Lamiroy, Benoît Valiron, Renaud Vilmart

Although the circuit model for quantum computation is well established, it is incapable of representing non-causal higher-order quantum processes such as the quantum switch. If several models of non-causal quantum computation have been considered in the literature, the approaches have so far only been focusing on the physicality of such processes, using matrices and other techniques from linear algebra. If these approaches are expressive, they however only provide a static and monolithic understanding of these processes. In this article, we propose a new formalism for non-causal, higher-order quantum processes. Based on a Curry-Howard interpetation, our proposal offers a computational interpretation that is both compositional and modular. In particular, we present Intuitionistic Unitary Linear Logic (IULL), a logic based on linear logic focusing on conservation of unitarity for higher order terms. We prove the coherence of IULLL, its completeness with regard to unitaries, and the admissibility of its cut rules. We finally discuss the validity of our approach by revisiting known non-causal quantum processes with IULL.