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 definidos¹, 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.

Función de lista de secuentes en arboles de pruebas: ¿Alguien conoce algo así?

Buenas,

Este post es para preguntar si alguien conoce algo parecido a esto (dado que ya he buscado en varios lugares y preguntado y nadie me ha sabido responder que haya algo así... pero debería haberlo ¿no?)

La idea es, dado un sistema de tipos deterministico, i.e. si me das un secuente y una regla de tipado, te doy la conclusión determinísticamente (Para ponerlo más claro, piensen en un sistema de tipos de segundo orden, donde hay un y la regla me dice que lo puedo eliminar reemplazando la por algo, bueno, eso no sería determinístico ya que a la la puedo reemplazar por diferentes cosas, algo determinístico en cambio sería si la regla fuese una familia de reglas (una por cada posible)), bueno, entonces, dado un sistema de tipos determinístico, lo que quiero es algo parecido a una función que tome una lista de sequentes y devuelva un árbol de prueba completo. O sea, es como si la función tuviera un árbol de pruebas vacío, donde sólo están las reglas a aplicar y los sequentes que hay en los axiomas, y cuando toma la lista de secuentes, los acomoda en los espacios vacíos de las hojas del árbol (o sea, los toma como hipótesis).

¿Se entiende la idea? Definirlo formalmente no es muy difícil, de hecho ya lo tengo hecho, pero quería saber si alguien conocía que ya exista algo así (como para no redefinir lo que ya existe).

Ya he preguntado a varias personas y nadie me supo decir que haya algo así, pero bueno, si a alguien esta "función" le suena parecido a algo que conozcan, avisen.