Un lenguaje de programación para la computación cuántica

Investigadores del ICC proponen un lenguaje de programación completo donde todas las operaciones que se escriben son exclusivas de la computación cuántica, es decir, pueden compilarse en una computadora cuántica. El trabajo ya fue aceptado en el Simposio LICS (Logic in Computer Science) de ACM/IEEE, cuya edición 2019 se realizará en Vancouver, Canadá.

El Instituto de Ciencias de la Computación (ICC) continúa produciendo aportes en fundamentos teóricos de la computación, impulsados por un grupo de investigadores que se dedica a estudiar lenguajes de programación y lógicas formales asociadas a estos lenguajes. Una de las aplicaciones actuales a este tema es ni más ni menos que la computación cuántica (ver nota anterior del ICC).

Dicho de otro modo, se utilizan paradigmas de lenguajes de programación y el lambda cálculo -sistema formal diseñado por el reconocido matemático Alonzo Church que resulta la base de la programación funcional-  con el fin de comprender exhaustivamente la lógica detrás del nuevo paradigma de la computación cuántica.

¿Qué nuevos desafíos plantea la computación cuántica como modelo matemático y cuál es la lógica detrás que permitiría expresar sus propiedades naturalmente? Algunos de estos interrogantes son los que se formula diariamente Alejandro Díaz-Caro, investigador del ICC, quien trabaja en el grupo de Lógica y Reescritura para Lenguajes de Programación (LoReL).

El investigador comenta que si bien la mecánica cuántica, como rama de la física, ha avanzado durante el siglo XX con sus desarrollos matemáticos y corroboraciones experimentales, existen múltiples problemas lógicos que se intentan responder matemáticamente para representar el funcionamiento de los programas de computación. Uno de estos problemas es el de la Superposición. Para entenderlo conviene pensar cómo funciona una computadora clásica (máquina de Turing): la unidad básica de información es el bit, que puede tener dos estados posibles (0 ó 1) y con los que podemos realizar diversas operaciones lógicas. Reuniendo n bits podemos representar números y operar sobre esos números, pero con limitaciones: sólo podemos representar hasta 2^n estados distintos, y si queremos cambiar x bits tenemos que realizar al menos x operaciones sobre ellos. Eso significa que no hay forma de cambiarlos mágicamente sin tocarlos.

No obstante, la superposición nos permite reducir esas limitaciones: podemos almacenar muchos más que sólo 2^n estados con n bits cuánticos (Qubits), que pueden estar en cualquier combinación de 0 y 1 al mismo tiempo. Superposición es otra manera de llamar a una “combinación lineal”, es decir, la superposición de estados cuánticos consiste en la suma de todos los estados, multiplicados por algún número lo que nos da como resultado un nuevo estado, un vector.

“A diferencia de construir un programa clásico que le dé órdenes a una computadora cuántica, donde no haya superposiciones posibles en esa estructura de control, estamos investigando cuáles son las operaciones lógicas que existen dentro de la computación cuántica e incluso qué operaciones se pueden superponer en los programas, en esa estructura de control”, enfatiza el doctor Díaz-Caro. Para ello explica que el trabajo no consiste tanto en diseñar el lenguaje para programar los algoritmos para la computadora cuántica sino en entender la lógica que es propia y exclusiva de este modelo matemático.

Con este propósito los investigadores no sólo recurren a los aportes del lambda cálculo -que es el lenguaje de programación más simple y universal que existe- sino también específicamente al Isomorfismo de Curry-Howard, el cual relaciona los sistemas de tipos con la lógica proposicional. En este sentido, los tipos son teoremas y las instancias de un tipo son demostraciones del teorema que representa. “Entender la lógica detrás de un programa cuántico implica determinar cuáles serían los tipos que hay en este programa y si los tipos también tienen que estar en superposición. Dado que los Qubits son vectores, nuestra idea es pensar a los tipos dentro de este espacio vectorial y a los programas cuánticos como matrices que se multiplican respecto a  un vector”, sostiene el investigador. Y a su vez problematiza: “el tema es que no cualquier superposición de programas es un programa así como tampoco no cualquier superposición de Qubits es un nuevo Qubit. La superposición de programas debe poseer algunas propiedades específicas para que sea cuántica”.

En busca de un lenguaje completo para cuántica

Como parte de sus múltiples objetivos de investigación, el Dr. Alejandro Díaz-Caro dirige un proyecto ECOS-Sud en conjunto con el Dr. Gilles Dowek (investigador del INRIA y profesor del ENS París-Saclay), quien es uno de los precursores en el paradigma de superposición de lenguajes de programación (paradigma de “control cuántico”).

Al mismo tiempo, desarrolla colaboraciones conjuntas con 4 universidades de Francia (ENS París-Saclay, CentraleSupélec, Aix Marseille Université y LORIA) en el marco del Laboratorio Internacional Asociado entre Francia y Argentina “SINFIN”, 1 universidad de Brasil (Universidade Federal de Santa Maria), 1 universidad de Uruguay (Universidad de la República), 1 de Chile (Universidad de Chile) y 1 de Paraguay (Universidad Nacional de Asunción). El artículo aceptado en el el simposio LICS enviado recientemente trata sobre el primer lenguaje de programación completo en el paradigma de control cuántico, es decir, donde todo lo que se escribe en el programa es netamente de cuántica (“Realizability in the Unitary Sphere”, autores: Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel y Benoît Valiron). “Por ahora funciona para un sólo Qubit pero la idea de este lenguaje coherente es que no se pueden realizar operaciones matemáticas que no sean de la computación cuántica”. El investigador explica en detalle que este trabajo se centró en un método de diseño de lenguajes conocido como Realizabilidad. “En lugar de diseñar un lenguaje y ver si cumple las propiedades que necesitás, se hace al revés: las propiedades que se quieren cumplir son fijadas como axiomas y se arma el lenguaje como teoremas derivados de estos axiomas”.

El trabajo, que significa una contribución destacada a los fundamentos de computación cuántica, ya fue aceptado en el simposio de lógica y ciencias de la computación organizado por  ACM y la IEEE, cuya edición se realizará en junio de 2019 en Vancouver, Canadá.

Otro resultado subrayado en los proyectos de Díaz-Caro es haber generado una lógica dual a la lógica lineal para evitar el clonado de Qubits y determinar cuándo un programa está en superposición y cuándo no, respecto a una medición cuántica prefijada. Este aporte consistió en analizar un lenguaje de programación para cuántica desde un punto de vista categórico, demostrando que al considerar la medición cuántica en un lenguaje, no alcanza sólo con el álgebra lineal, ya que esta medición es por definición una operación no lineal. El investigador resalta que algunos de estos resultados significan un pequeño avance para entender, cada día, un poco más globalmente sobre la computación cuántica y, por ende, sobre la física cuántica, aunque efectivamente aún no se hayan desarrollado computadoras cuánticas reales.