Towards quantum program calculation

Abstract

Based on the similarity between the categorial derivation of classical programs from their specification and the category theory approach to quantum physics, this dissertation aims at extending the laws of classical program algebra to quantum programming. In this context, the principles of the algebra of classical programs are applied to quantum programming, in order to verify the feasibility of creating correct-by-construction quantum circuits that can run on quantum devices available in the IBM Q Experience. The reversibility restrictions of quantum circuits are ensured by minimal complements. Moreover, measurements are postponed to the end of recursive computations called “quantamorphisms” to avoid the collapse of quantum states. Quantamorphisms are classical catamorphisms extended to ensure quantum reversibility. The derived quantamorphisms implement quantum cycles (vulg. for-loops) and quantum folds on lists. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. The examples of the calculated quantum programs are simulated in Haskell, Quipper and QISKit and run on the quantum computers of the IBM Q Experience. The main conclusions of this work are that, while all the simulations produced correspond to the predicted results, running these programs on real quantum devices results in a significant amount of errors. As quantum devices are constantly evolving, it is likely that in the near future these devices will increase their reliability, allowing programs to run more accurately. The extension of the quantamorphism concept to more general input structures, such as finite trees, remains a challenge that is left for future work. Also relevant will be the study of conditional quantum control without measurements, which will extend the scope of quantamorphisms as quantum circuit specifications.

Tendo como base a similaridade entre a matemática categorial para derivar programas a partir da sua especificação e a teoria categorial usada na física quântica, esta dissertação pretende estender as leis da álgebra de programas clássicos à programação quântica. Nesse contexto, a dissertação trata de explorar o significado desses princípios e suas construções na programação quântica e verificar a viabilidade de as aplicar à criação de programas quânticos correctos que possam correr em dispositivos quânticos disponíveis no IBM Q Experience. As restrições de reversibilidades exigidas pela programação quântica são asseguradas por complemento mínimo, e para evitar o colapso dos estados quânticos a medição é adiada através de “quantamorfismos”, nome dado à extensão reversível do conceito clássico de catamorfismo. Os quantamorfismos que se implementaram permitem correr ciclos-for quânticos e folds quânticos sobre listas. Com base na correspondência de Kleisli é possível escrevê-los como programas funcionais monádicos com parâmetros quânticos. Para esse efeito recorre-se à linguagem de programação funcional Haskell como base para o trabalho experimental. Os exemplos dos programas quânticos calculados foram simulados em Haskell, Quipper e QISKit e correram nos computadores quânticos da IBM Q Experience. Constata-se que, enquanto todas as simulações produzidas correspondem ao previsto, correr estes programas em máquinas reais resulta numa quantidade significativa de erros. Como os dispositivos quânticos estão em constante evolução, é provável que num futuro próximo estes dispositivos aumentem a sua fiabilidade, permitindo que os programas corram de forma mais precisa. Entre as questões que esta tese levanta inclui-se a extensão dos seus resultados a estruturas de entrada mais gerais, como por exemplo árvores, e estruturas de controlo condicionais que não efectuem medidas e que assim possam estender o âmbito do quantamorfismo como veículo de especificação de circuitos quânticos.