Estruturando computaçõoes quânticas gerais e completas em Haskell : abordagem das setas

Computaçãao quântica pode ser entendida como transformação da informação codificada no estado de um sistema físico quântico. A idéia básica da computação quântica é codificar dados utilizando bits quânticos (qubits). Diferentemente do bit clássico, o qubit pode existir em uma superposição dos seus estados básicos permitindo o “paralelismo quântico”, o qual é uma característica importante da computação quântica visto que pode aumentar consideravelmente a velocidade de processamento dos algoritmos. Entretanto, tipos de dados quânticos são bastante poderosos não somente por causa da superposição de estados. Existem outras propriedades ímpares como medida e emaranhamento. Nesta tese, nós discutimos que um modelo realístico para computações quânticas deve ser geral com respeito a medidas, e completo com respeito a comunicação entre o mundo quântico e o mundo clássico. Nós, então, explicamos e estruturamos computações quânticas gerais e completas em Haskell utilizando construções conhecidas da área de semântica e linguagens de programação clássicas, como mônadas e setas. Em mais detalhes, esta tese se concentra nas seguintes contribuições. Mônadas e Setas. Paralelismo quântico, emaranhamento e medida quântica certamente vão além do escopo de linguagens funcionais “puras”. Nós mostramos que o paralelismo quântico pode ser modelado utilizando-se uma pequena generalização de mônadas, chamada mônadas indexadas ou estruturas Kleisli. Além disso, nós mostramos que a medida quântica pode ser explicada utilizando-se uma generalização mais radical de mônadas, as assim chamadas setas, mais especificamente, setas indexadas, as quais definimos nesta tese. Este resultado conecta características quânticas “genéricas” e “completas” `a construções semânticas de linguagens de programação bem fundamentadas. Entendendo as Interpretações da Mecânica Quântica como Efeitos Computacionais. Em um experimento hipotético, Einstein, Podolsky e Rosen demonstraram algumas consequências contra-intuitivas da mecânica quântica. A idéia básica é que duas partículas parecem sempre comunicar alguma informação mesmo estando separadas por uma distância arbitrariamente grande. Existe muito debate e muitos artigos sobre esse tópico, mas é interessante notar que, como proposto por Amr Sabry, essas características estranhas podem ser essencialmente modeladas por atribuições a variáveis globais. Baseados nesta idéia nós modelamos este comportamento estranho utilizando noções gerais de efeitos computacionais incorporados nas noções de mônadas e setas. Provando Propriedades de Programas Quânticos Utilizando Leis Algébricas. Nós desenvolvemos um trabalho preliminar para fazer provas equacionais sobre algoritmos quânticos escritos em uma sublinguagem pura de uma linguagem de programação funcional quântica, chamada QML.Quantum computation can be understood as transformation of information encoded in the state of a quantum physical system. The basic idea behind quantum computation is to encode data using quantum bits (qubits). Differently from the classical bit, the qubit can be in a superposition of basic states leading to “quantum parallelism”, which is an important characteristic of quantum computation since it can greatly increase the speed processing of algorithms. However, quantum data types are computationally very powerful not only due to superposition. There are other odd properties like measurement and entangled. In this thesis we argue that a realistic model for quantum computations should be general with respect to measurements, and complete with respect to the information flow between the quantum and classical worlds. We thus explain and structure general and complete quantum programming in Haskell using well known constructions from classical semantics and programming languages, like monads and arrows. In more detail, this thesis focuses on the following contributions. Monads and Arrows. Quantum parallelism, entanglement, and measurement certainly go beyond “pure” functional programming. We have shown that quantum parallelism can be modelled using a slightly generalisation of monads called indexed monads, or Kleisli structures. We have also build on this insight and showed that quantum measurement can be explained using a more radical generalisation of monads, the so-called arrows, more specifically, indexed arrows, which we define in this thesis. This result connects “generic” and “complete” quantum features to well-founded semantics constructions and programming languages. Understanding of Interpretations of QuantumMechanics as Computational Effects. In a thought experiment, Einsten, Podolsky, and Rosen demonstrate some counter-intuitive consequences of quantum mechanics. The basic idea is that two entangled particles appear to always communicate some information even when they are separated by arbitrarily large distances. There has been endless debate and papers on this topic, but it is interesting that, as proposed by Amr Sabry, this strangeness can be essentially modelled by assignments to global variables. We build on that, and model this strangeness using the general notions of computational effects embodied in monads and arrows. Reasoning about Quantum Programs Using Algebraic Laws. We have developed a preliminary work to do equational reasoning about quantum algorithms written in a pure sublanguage of a functional quantum programming language, called QML