Fundamentos de lenguajes de programación : sistemas de pruebas y computación cuántica

Fil: Díaz-Caro, Alejandro. Universidad Nacional de Quilmes; Argentina. Fil: Martínez López, Pablo E. Universidad Nacional de Quilmes; Argentina. La mecánica cuántica es el conjunto de construcciones matemáticas que dan predicciones sobre el comportamiento de las partículas. Desde sus inicios, hubo estudios matemáticos (y filosóficos) sobre qué sería una lógica cuántica, ya que no pareciera ir de la mano de la lógica clásica. En efecto, en lógica clásica, podemos considerar que una proposición es o bien verdadera, o bien falsa; sin embargo, debido a características intrínsecas de la mecánica cuántica, en una lógica cuántica deberíamos poder considerar proposiciones que son verdaderas y falsas a la vez. Esto llevó a Birkhoff y von Neumann a definir, en 1936, una "lógica cuántica" que pueda describir este tipo de "superposiciones". La computación cuántica aparece a principios de los 80s como una manera estructurada de pensar a la mecánica cuántica. Básicamente cualquier proceso cuántico tiene un estado inicial, un estado final, y una evolución entre uno y otro. Por lo tanto, esta evolución, puede ser considerada como un proceso de cómputo. El cálculo lambda es una manera de describir procesos de cómputo, y el cálculo lambda tipado es isomorfo a un sistema de pruebas lógico, donde los tipos son las proporciones, y los términos lambda, sus pruebas. Por lo tanto, desde hace más de una década, que se estudia la lógica cuántica (o "lógica cuántica computacional", para distinguirla de aquella de Birkhoff y von Neumann) desde un punto de vista formal utilizando técnicas de las ciencias de la computación. Así, de la mecánica cuántica pasamos a la computación cuántica como formalismo matemático, de allí al cálculo lambda tipado como método de formalizar los "programas" cuánticos, y finalmente a la lógica, utilizando el isomorfismo antes mencionado. Por ejemplo, estudiando la semántica categórica de ciertos cálculos cuánticos, se derivó una construcción dual de la lógica lineal, que puede describir la superposición cuántica, entre otras propiedades. En este proyecto proponemos por un lado, un desarrollo teórico, que consiste en explorar diversas líneas de extensiones al cálculo lambda para computación cuántica, y también de sistemas de pruebas novedosos, que puedan facilitar los modelos de lógica cuántica a los que se quiere arribar, y por otro lado, una parte más aplicada, de desarrollar prototipos de simuladores de computación cuántica, al implementar los lenguajes obtenidos a partir del cálculo lambda.