by Luis S. Barbosa, Alexandre Madeira (QuantaLab, and HASLab INESC TEC, Universidade do Minho)
Quantum algorithmics is emerging as a hot area of research, with the potential to have groundbreaking impacts on many different fields. The benefits come at a high price, however: quantum programming is hard and finding new quantum algorithms is far from straightforward. This area of research may greatly benefit from mathematical foundations and calculi, capable of supporting algorithm development and analysis. The Quantum Algorithmics Agenda at QuantaLab is contributing by seeking a suitable semantics-calculus-logic trilogy for quantum computation.
Software is a critical factor in the reliability of computer systems. While the development of hardware is assisted by mature science and engineering disciplines, software science is still in its infancy. This situation is likely to worsen in the future with quantum computer systems, as these will be more difficult to program and test. Moreover, quantum resources are critical. Thus, the need for correct-by-construction formal techniques [1] in quantum software development is even bigger than in classical computation. A lack of reliable approaches to quantum computer programming will put at risk the expected quantum supremacy of the new hardware.
Interest in quantum algorithmics has recently been boosted, with the identification of quantum technologies and computation as a strategic R&D domain for the EU. Over the last decade, the number of algorithmic techniques has grown significantly, exploring quantum effects, namely entanglement, in a number of ways. However, finding new and effective quantum algorithms has proved a challenging task. This entails the need for more mature mathematical techniques to provide rigorous semantics, effective program development calculi and suitable logics for specification and verification.
The class of quantum algorithms that encompasses classical control (deterministic, non-deterministic and probabilistic control structures) offers a wide scope of applications. This includes most common algorithms, as well as new applications to machine learning, computer graphics and quantum simulation.
The Quantum Algorithmics Agenda is a recently launched initiative at QuantaLab—the new collaborative research centre established by the International Iberian Nanotechnology Laboratory and the Universidade do Minho, located in Braga, Portugal. It brings together researchers in the broad areas of Quantum Materials and Technologies, covering experimental, theoretical, and computational research.
Our starting point is that, just like classical computation, quantum algorithmics will greatly benefit from a mathematically based approach, able to conceptualise, and predict behaviour, and to provide a rich, formal framework for specifying, developing and verifying quantum algorithms. Such foundations are produced in the confluence of several mathematical disciplines [2]: category theory (categorical logic, categorical semantics), logic (dynamic logic, lambda-calculus, linear logic, proof theory, type theory), theory of computation (complexity theory, information theory).
The goal of our research agenda is to develop such a framework and the corresponding mathematical techniques. We intend to fill a gap that we have identified in the literature at the following interrelated levels:
- Appropriate semantic structures, able to comply with the different types of classical control structures and quantum data, as well as to capture the notion of (quantum) program approximation;
- An algorithmic calculus consistent with the semantics above for the systematic derivation of quantum programs in a compositional way;
- A new family of dynamic logics, obtained in a parametric way [3] to support the formulation of contracts for quantum algorithms and their compositional verification;
- Proof systems for quantum logics, emphasising their role as type systems to ensure intentional properties of quantum algorithms, such as complexity and termination.
We are fully aware that such a broad goal cannot be achieved unless a particularly challenging application domain is selected as a testbed for theoretical results. Therefore, the construction of quantum convolutional codes was chosen as a case-study, not only because of its intrinsic difficulty, but also for its societal relevance. Modern societies depend heavily on the security level with which data is exchanged among complex, heterogeneous systems.
Quantum communication channels open the door for new, fast and secure communication schemes. For instance, in cryptography, the quantum key distribution protocol, that produces and distributes keys with an absolute guarantee of secrecy (relying on entanglement of quantum states) is already used and commercialised. Quantum error correction codes constitute simultaneously a rich source of semantic challenges and a vital tool in quantum technology, with a wide potential range of applications, from the protection of quantum information in noisy quantum channels, to the avoidance of decoherence in quantum computers.
References:
[1] R. Bird, O. de Moor: “Algebra of Programming. Series in Computer Science”,.Prentice-Hall, 1997.
[2] B. Coecke (Ed.): “New Structures for Physics”, Springer (Lecture Notes in Physics), 2011.
[3] A. Madeira, R. Neves, M.A. Martins: “An exercise on the generation of many-valued dynamic logics”, Jour. Logical and Algebraic Methods in Programming 85(5), 2016.
Please contact:
Luis Soares Barbosa, QuantaLab, and HASLab INESC TEC, Universidade do Minho, Portugal
+351 253604463,
