Primer paper desde que empecé con este proyecto de doctorado. Fue aceptado en el VI Workshop Quantum Physics and Logic que se va a llevar a cabo en Oxford el 8 y 9 de Abril próximos. Está disponible para descargar libremente aquí: arXiv:0903.3741.
Título:
Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic
(System F escalar para el λ-Cálculo Algebraico Lineal: Hacia una Lógica Física Cuántica)
El λ-cálculo algebraico lineal [1] extiende el λ-cálculo con la posibilidad de crear combinaciones lineales arbitrarias de términos α.t+β.u. Dado que se pueden expresar operadores de punto fijo sobre sumas en este cálculo, surge la noción de infinito, y por lo tanto, la noción de formas indefinidas. Como consecuencia, a fin de garantizar confluencia, t-t no siempre reduce a 0, sólo si t es cerrado y en forma normal. En este paper proveemos un sistema de tipos estilo System F para el λ-cálculo algebraico lineal, el cual garantiza normalización y por lo tanto no hay necesidad de esas restricciones: t-t siempre reduce a 0. Además este sistema de tipos lleva la cuenta de "la cantidad de un tipo". Por lo tanto puede verse como un sistema de tipos probabilístico, garantizando que los términos definen funciones probabilísticas correctas. Por último, se puede ver este sistema de tipos como un paso en la búsqueda de una lógica física cuántica a través del isomorfismo de Curry-Howard [2].
Bueno, tal como se expresa en el abstract, lo que hicimos fue darle tipos al λ-cálculo algebraico lineal. Usamos System F, o sea un sistema de tipos polimórfico, expresado à la Curry. Los tres resultados que se podrían destacar son:
- Con System F tenemos strong normalization, o sea, todo término que tiene un tipo normaliza, siguiendo cualquier vía de reducción. Por lo tanto, no tenemos más el problema de los infinitos del λ-cálculo algebraico lineal.
- El sistema de tipos hace que cualquier función probabilística expresada en el lenguaje, esté bien definida, o sea, que, por ejemplo, en una función que devuelve una cosa u otra dependiendo de su argumento, ambos branches suman lo mismo.
- La idea de darle tipos a este cálculo, no es por el lenguaje en sí, sino para extraer una lógica utilizando el isomorfismo de Curry-Howard, lo cual, a diferencia de la lógica cuántica definida en 1936 por Barkhoff y von Neumann [3] (la cual no se sabe cómo relacionar con la computación cuántica), esta lógica no está definida ad hoc sino extraída de un sistema de tipos de un cálculo que permite expresar la computación cuántica. Por supuesto, este es el primer paso, aún falta trabajo por hacer hasta tener un sistema de tipos que sólo admita programas representables por la computadora cuántica (i.e. que sus términos estén normalizados y que sus compuertas sean unitarias), pero aquí, con este primer sistema de tipos, hacemos un intento de interpretación de la lógica: como ya dije, esta lógica no está inventada ad hoc, sino extraída automáticamente del sistema de tipos, entonces ¿qué significa esta lógica? ¿qué interpretación le podemos dar? A modo de discusión dejamos algunas ideas en la última sección del paper.
Referencias:
[1] Pablo Arrighi y Gilles Dowek. Linear-algebraic λ-calculus: higher-order, encodings and confluence. Lecture Notes in Computer Science (RTA'08), 5117:17-31, 2008. (arXiv:quant-ph/0612199).
[2] Morten H. Sørensen y Pawel Urzyczyn.Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., New York, NY, USA, 2006. (PDF).
[3] George D. Birkhoff y John von Neumann. The logic of quantum mechanics. Annals of Mathematics, 37:823-843, 1936. (JSTOR).
