Fundamentos de lenguajes de programación para computación cuántica

ALEJANDRO DÍAZ CARO

Lima

Conferencia; X Congreso Internacional de Computación y Telecomunicaciones; 2018

La computación cuántica puede ser considerada de diversas maneras. Entre ellas, se puede considerar a la computación cuántica como un modelo de la mecánica cuántica. Como tal, estudiar este modelo tiene implicaciones en la manera de entender la física. También puede ser considerado un nuevo paradigma computacional, por lo tanto, con implicaciones en la manera de entender la computación, los algoritmos y la lógica. Finalmente, puede ser considerado como un dispositivo que existirá en un futuro, el cual necesitará ser programado, y por lo tanto, se deben estudiar los lenguajes de programación para el mismo.El estudio de los fundamentos de los lenguajes de programación cuánticos, la teoría de tipos y, a través de la correspondencia de Curry-Howard, la lógica, pueden arrojar luz en el entendimiento de la mecánica cuántica. Además, puede conducir a nuevas lógicas, o a comprender nuevas estructuras de la lógica clásica. Por último, la implementación de dichos lenguajes enriquecerá las maneras de programar los dispositivos cuánticos cuando éstos arriben.Actualmente, se destacan dos paradigmas contrapuestos en el diseño de lenguajes de programación cuánticos: el de control clásico y datos cuánticos, y el de control y datos cuánticos.El concepto de control clásico y datos cuánticos dice que las computadoras cuánticas correrán en dispositivos especializados anexos a una computadora clásica, y esta computadora clásica es quien instruirá a la computadora cuántica qué operaciones realizar sobre qué qubits. Luego, cuando se realice una medición, es la computadora clásica la que recuperará los bits clásicos para continuar el programa. Este paradigma es una consecuencia directa de la observación de que los circuitos cuánticos son clásicos (no se puede superponer circuitos o medirlos). En contraposición, el paradigma de control y datos cuánticos estudia los modelos lógicos provenientes de la computadora cuántica en sí, dando posibilidad de estudiar las consecuencias de las estructuras de control cuánticas, como por ejemplo, el llamado quantum-if, que permite una condición que sea una superposición de verdadero y falso, produciendo una superposición de las ramas del if.En esta conferencia haré un recorrido por ambos paradigmas, y mostraré algunos resultados recientes en cálculo lambda para computación cuántica, como modelo mínimo de lenguaje de programación, y como sistema formal de pruebas en lógica.