23 de septiembre de 2009

Computación Cuántica, Teoría de Tipos y Lógicas Cuánticas

Más de uno me ha preguntado por el significado del subtítulo del blog: "Computación Cuántica, Teoría de Tipos y Lógicas Cuánticas", así que trataré de resumirlo aquí en un lenguaje lo más entendible posible (y cualquier cosa que no quede clara, pregunten en los comentarios (o corríjanme si encuentran algún error))

Este es mi tema de investigación del doctorado. Existen muchas lógicas matemáticas diferentes, como por ejemplo (y estas son sólo algunas): Lógica proposicional, Lógica de primer orden, Lógica de segundo_orden, Lógica difusa, Lógica relevante, Lógica no monotónica, Lógica intuicionista, Lógica modal, Lógica temporal y hasta incluso existe una llamada Lógica cuántica.

Por otro lado, existe una teoría llamada Teoría de Tipos, que, en su forma más básica, permite caracterizar un algoritmo sin necesidad de ejecutarlo. O sea, tenemos un algoritmo y podemos definir qué "tipo" tiene ese algoritmo, lo cual nos da alguna información relevante que queremos saber sobre el resultado al finalizar la ejecución de dicho algoritmo.

La idea es que uno tiene ciertas reglas que dicen cómo decidir si un algoritmo tiene cierto tipo. Veamos un ejemplo sencillo de regla: siempre que tengamos un algoritmo, vamos a llamarlo A1, de "tipo" booleano (cuando tiene tipo booleano lo que estamos diciendo es que su resultado puede ser uno de dos valores: "verdadero" o "falso" y no por ejemplo un número) y otro algoritmo, A2, también booleano, entonces el algoritmo "A1 and A2" tendrá también tipo booleano. Esto se escribe en símbolos así:
A1:Bool     A2:Bool
--------------------
A1 and A2: Bool

Vamos con un ejemplo un poco más complicado:
F: Bool => Numero   A: Bool
-------------------------------
F(A): Numero

Esto dice que si tengo una función que toma un booleano y devuelve un número, entonces la función aplicada a un booleano, será de tipo número.

Y qué tiene que ver esto con lógica?

Bien, la idea es que cada conjunto de reglas define una lógica. Esto fue descubierto por el matemático Haskell Curry y el lógico William Howard y se lo llama la correspondencia de Curry-Howard. Cómo funciona? Pongamos por ejemplo la segunda regla escrita arriba:
F: Bool => Numero   A: Bool
-------------------------------
F(A): Numero

 Si nos olvidamos de los "algoritmos" y nos quedamos sólo con los tipos, la regla quedaría así:
Bool => Numero   Bool
----------------------
Numero


La cual no es más que la regla lógica de implicación: Si Bool implica Número y tengo Bool, entonces tengo Número.

Diferentes reglas de tipado nos darán diferentes lógicas. La correspondencia nos asegura que por cada "fórmula bien formada" en nuestra lógica, tendremos un "algoritmo" capaz de producir una salida con ese tipo.

Y qué tiene que ver esto con computación cuántica?

Como mencioné antes, existe una lógica cuántica, pero esa lógica fue inventada mucho antes de la computación cuántica; fue desarrollada en base a la mecánica cuántica, de manera ad-hoc, tratando de capturar su comportamiento. Luego, con el advenimiento de la computación cuántica, se ha tratado intensamente de hacer una correspondencia entre los algoritmos cuánticos y la lógica cuántica, para lo cual se ha ido modificando la lógica a medida que avanzan las investigaciones de manera de adecuarla a los algoritmos.

Mi trabajo de investigación es empezar por el otro lado desde cero: ya hay lenguajes cuánticos definidos1, por lo tanto, si puedo definir un sistema de tipos para él, tendré una lógica cuántica definida directamente desde los lenguajes cuánticos (y con ello se podría analizar diferentes algoritmos a partir de su lógica).

Espero se haya entendido la explicación, y sino, sientanse libres de preguntar en los comentarios del blog.

----------------------------------------------
1 En particular hay lo que se llama un lambda cálculo, que es una especie de lenguaje muy básico que permite expresar cualquier algoritmo. En realidad, hay varios, yo en particular uso el Linear-Algebraic Lambda-Calculus de Pablo Arrighi y Gilles Dowek.

7 comentarios:

  1. Daniel Montenegro23/9/09 09:57

    Buena info che! Suerte.

    ResponderEliminar
  2. No se cómo, creo que a través de Gmail, un día vi un link a tu blog, entré a leerlo, y me enganché más al ver que te habías relacionado con Fidel, que fue profesor mío en la UNLP. Desde ese momento leo todos tus post :D
    En una semana voy a comenzar a ver de cerca alguno de los temas con los que trabajás a diario, ya que arranco a hacer el trabajo final de la materia Programación Funcional (la cátedra donde hasta hace 2 años estaba Fidel, pero no se por qué ya no está). Es un proyecto sobre un Evaluador LIS. Por ahora no tengo mucha idea de qué se tratará, pero lo tengo que tener terminado para febrero del año que viene.

    Te dejo un saludo. Un placer verte progresar.
    Leonardo.

    ResponderEliminar
  3. Gracias por los comentarios!
    @Leonardo: Fidel está dirigiendo una carrera en la Universidad de Quilmes y creo que sigue con su cátedra en Rosario (hasta que me fui a Francia, seguía allí).
    Mucha suerte con el proyecto!

    Saludos.

    ResponderEliminar
  4. Hola Alejandro, acabo de descubrir este blog solo buscando "computacion cuantica" en espanhol en google. Excelente!!

    Mi area de investigacion no es teoria de tipos, sino quantum walks and quantum query complexity, pero te lanzo una pregunta que me quedo flotando gracias a la excelente introducion que hiciste de la teoria de tipos.

    Si aun no hay una logica que describa completa y correctamente los algoritmos cuanticos, eso significa que no hay metodos de verificacion para algoritmos cuanticos (conozco de metodos de verificacion para circuitos)? Con que lenguajes cuanticos trabajas (yo solo conozco el qcl de ibm) ? se podria utilizar la logica cuantica para describir y/o verificar modelos abstractos de computacion, e.g., quantum turing machines, cellular automata, etc?

    ResponderEliminar
  5. Hola Danny,

    «Mi area de investigacion no es teoria de tipos, sino quantum walks and quantum query complexity»
    Si te animás, te propongo que hagas una introducción a esos temas para publicar en el blog, te parece?

    «Si aun no hay una logica que describa completa y correctamente los algoritmos cuanticos, eso significa que no hay metodos de verificacion para algoritmos cuanticos (conozco de metodos de verificacion para circuitos)?»
    Correcto, al menos no métodos formales.

    «Con que lenguajes cuanticos trabajas (yo solo conozco el qcl de ibm) ?»
    Yo trabajo con lambda cálculo, en particular estoy trabajando con el "Linear-Algebraic Lambda-Calculus" de Arrighi y Dowek. Hay un review interesante sobre los lenguajes existentes, mantenido por Simon Gay.

    «se podria utilizar la logica cuantica para describir y/o verificar modelos abstractos de computacion, e.g., quantum turing machines, cellular automata, etc?»
    Si, se podría utilizar para ello y mucho más. Una vez definida la lógica se podría incluso utilizar asistentes de pruebas como COQ.

    Saludos!

    ResponderEliminar
  6. Gracias por la invitacion, me encantaria escribir una introduccion a esos temas. Podriamos comenzar con algo "light" asi como hiciste en tu introduccion a teoria de tipos y en otro momento pasar a la parte divertida.

    Siempre me gusto la logica, me parece un area fascinante, especialmente teoria recursiva, aunque es muy diferente a complexity theory.

    ResponderEliminar
  7. Genial. Te mandé un mail así seguimos charlando. Saludos.

    ResponderEliminar