Sequent Calculus Representations for Quantum Circuits

TL;DR

This paper proposes a sequent calculus framework based on quantum circuits to better represent quantum mechanics elements like phase, interference, and measurement, enhancing the logical understanding of quantum computation.

Contribution

It introduces a novel sequent calculus model rooted in quantum circuits that captures dynamic and conceptual aspects of quantum mechanics often missed by traditional logics.

Findings

The calculus incorporates phase and interference effects.

It offers a non-monotonic reasoning framework for quantum logic.

The approach aligns proof rules with quantum circuit dynamics.

Abstract

When considering a sequent-style proof system for quantum programs, there are certain elements of quantum mechanics that we may wish to capture, such as phase, dynamics of unitary transformations, and measurement probabilities. Traditional quantum logics which focus primarily on the abstract orthomodular lattice theory and structures of Hilbert spaces have not satisfactorily captured some of these elements. We can start from 'scratch' in an attempt to conceptually characterize the types of proof rules which should be in a system that represents elements necessary for quantum algorithms. This present work attempts to do this from the perspective of the quantum circuit model of quantum computation. A sequent calculus based on single quantum circuits is suggested, and its ability to incorporate important conceptual and dynamic aspects of quantum computing is discussed. In particular, preserving the representation of phase helps illustrate the role of interference as a resource in quantum computation. Interference also provides an intuitive basis for a non-monotonic calculus.