Quantum computing (QC) represents the future of computing systems, but the tools for reasoning about the quantum model of computation, in which the laws obeyed are those on the quantum mechanical scale, are still a mix of linear algebra and Dirac notation; two subjects more suitable for physicists, rather than computer scientists and software engineers. On this ground, we believe it is possible to provide a more intuitive approach to thinking and writing about quantum computing systems, in order to simplify the design of quantum algorithms and the development of quantum software. In this paper, we move the first step in such direction, introducing a specification language as the tool to represent the operations of a quantum computer via axiomatic definitions, by adopting the same symbolisms and reasoning principles used by formal methods in software engineering. We name this approach formal quantum software engineering (F-QSE). This work assumes familiarity with the basic principles of quantum mechanics (QM), with the use of Zed (Z) which is a formal language of software engineering (SE), and with the notation and techniques of first-order logic (FOL) and functional programming (FP).
1 The probability for an observable to collapse into any of its states is the squared modulus of the states’ corresponding probability amplitudes, which are complex numbers that weight each eigenvector and such that it is |c0|2 + ... + |cn|2 = 1.
By the third postulate of QM, an observable that has a finite number of quantum states can be
represented via a Hermitian matrix 2 . As such, the three requirements that it must have can be
described, with a sound formalism, by adopting strongly typed data and first-order logic [
3. for every eigenvector (or, column) of the matrix the eigenvalue must be a real number; and such that it is the element on the main diagonal of the matrix:
In Z, all three requirements can be summarized with the following axiomatic definition satisfying
the principle of soundness promoted by FM [
After having introduced the new type , it is now possible to define the observable operators. They are elementary quantum gates that perform unitary transformations Uf (i.e., reversible computations) and that, applied to an observable, make it possible to write quantum programs.
In the following paragraphs, we introduce the axiomatic definition of the most common quantum gates, establishing the basic tools to design quantum programs in Z.
Identity gate.
It is the simplest, single qubit, quantum operator, that maps the input to the output unchanged. It is required by any operation where the same qubits that are passed as arguments must be returned:
It is the quantum equivalent of the classical NOT gate: 2 But if the Hilbert space ℋ is infinite-dimensional, the observable is described by a symmetric operator, which is represented as a map between two domains of basis’ states and ∗ dense in ℋ, such that ∀x: D, y: D∗∃ : ↦ ∗ • ⟨ (x), y ⟩ = ⟨ x, (y) ⟩. This is a bijective function (injective-surjective), in the sense that it cannot map two distinct states of the domain onto the same state of the co-domain ∗, thus preserving its unitary quality. However, because an infinite-dimensional space is unbounded also the operator is unbounded; therefore, it does not have a largest eigenvalue, leaving us with the conclusion that it might not be defined everywhere and, as such, classifying it as a partial bijective function, which implies graph inclusion: ≤ ∗. Phase Shift gate.
It represents a family of gates, that rotate the basis state |1⟩ of any arbitrary angle :
It is a special case of the Phase Shift gate, that rotates the basis state |1⟩ a angle:
It is perhaps the most useful quantum operator because it maps any basis state to one qubit with balanced superposition, and vice-versa:
The Controlled Not gate is the most popular 2-qubits operator, because it puts two qubits in a separable state, with a tensor product pairing the first qubit with the result of an addition modulo-2 between both. As such, it is used to entangle two qubits or disentangle the EPR pair:
Similarly to what happens in any conventional computation, a quantum computation is just a sequence of gates applied in a particular order: each gate takes an input and, after having performed its operation on that input, returns an output. However, in QC, the single use of an operator simultaneously applies to all basis states [9].
The Deutsch algorithm, foundation model of QC [7, 8], proves if a quantum oracle function, i.e. a
black-box that performs a unitary transformation Uf on a qubit, is constant (always maximizing the
same state) or balanced (returning each state half of the time). It exploits the quantum entanglement
principle [
In Dirac notation, it is represented as a ket taking a pair of qubits, prepared from two different basis states ( and ), and mapping them to an entangled pair where the second qubit performs as the register storing the state (solution) that will be set on the first qubit by the quantum oracle. The measurement of the first qubit shall, therefore, make it collapse into the state that is held by the second qubit, to which it is entangled:
With the Z notation, the algorithm can be described through axiomatic definitions; either by writing the constraining predicate from the conventional Dirac representation (which is sound but doesn’t add much in a SE perspective):
or from the quantum circuit by taking advantage of the axiomatic definitions of the observable operators, such as: rather then:
Indeed, with the last two definitions, by describing the algorithm through a sequence of formal operators we offer a guidance for coding it, by directly following the stepwise logic represented.
Of course, the coding part can be done in any quantum programming language. For our case, in
order to match the formal definitions introduced, we worked out an instruction set in Haskell that
leans on Green’s QIO library [
The Deutsch algorithm can be now, effortlessly, translated into the following QC program: for which, the required operators are implemented as follows: ---- return a qubit in a given state qb :: [Char] -> QIO ( Qbit ) qb qstate | qstate = = "|0>" = mkQ( False ) | qstate = = "|1>" = mkQ( True ) | qstate = = "|+>" || qstate = = "H|0>" = do qBit <- qb( "|0>" ) applyU( uhad( qBit ) ) return( qBit ) | qstate = = "|->" || qstate = = "H|1>" = do qBit <- qb( "|1>" ) applyU( uhad( qBit ) ) return( qBit ) | otherwise = error "qb: wrong argument" ---- apply the Hadamard gate to a qubit qH :: Qbit -> QIO () qH qbit = applyU( uhad( qbit ) ) ---- measure a qubit mq :: Qbit -> QIO ( Bool ) mq qbit = measQ( qbit ) ---- apply the C-Not gate to a qubit qN :: (Bool -> Bool) -> Qbit -> Qbit -> QIO () qN f qx qy = applyU( cond (qx) (\ a → if f(a) then unot(qy) else mempty )) 3
The diffusion of QC cannot be forever relegated within a narrow circle of experts, but many
computer scientists and software engineers entering the field of QC are quickly put off by the existing
conceptual and notational barriers [
One of the possible ways to overcome this stasis is to introduce a vocabulary inspired by the
formal tools of SE. In this paper, the main notions of QC take the form of axiomatic definitions in the
Z notation so that they can be used throughout specifications [
Hopefully, it can open the doors of QC to a wider audience of players, helping them to beautifully understand, describe, and finally convert the structure of quantum algorithms into fully working code.
The author would like to thank you professor emeritus Prof. Giuseppe Moesch, Prof. Ralf Hinze, and Dr. Wojciech Roga, for the lasting guidance offered during the most intense moments of his life. [7] D. Deutsch “Quantum Theory, the Church-Turing Principle and the Universal Quantum
Computer”, Proc. Royal Soc. of London, A400:97-117, 1985 [8] D. Deutsch, R. Jozsa “Rapid Solutions of Problems by Quantum Computation”, Proc. Royal Soc.
of London, A439:553, 1992 [9] A. Barenco “Quantum Computation: an Introduction”. in “Introduction to Quantum Computation and Information”, H. Lo, S. Popescu and T. Spiller (Eds.), World Scientific, 1998 [10] A. M. Gross, J. Stallard “Implementing Grover’s Algorithm Using Linear Transformations in Haskell”, Proceedings of the Eight Symposium on Trends in Functional Programming, 8:XXV, 2007 [11] Mateus P., Sernadas A. (2004) Reasoning About Quantum Systems. In: Alferes J.J., Leite J. (eds) Logics in Artificial Intelligence. JELIA 2004. Lecture Notes in Computer Science, vol 3229.
Springer, Berlin, Heidelberg [12] Simon D. R. “On the Power of Quantum Computation” SIAM J. Comput., 26(5), 1474-1483 (1997) [13] P. Kaye, R. Laflamme, M. Mosca “An Introduction to Quantum Computing” Oxford University Press, 2007