Escalares y sumas, al arXiv // Scalars and sums, to arXiv

(English version below)
Ya está disponible el paper que escribimos con Barbara Petit sobre el análisis de las sumas en los cálculos algebraicos que presentamos en Types 2010. La semana pasada lo subimos al arXiv: http://arxiv.org/abs/1011.3542.

También la semana pasada con Pablo Arrighi actualizamos en el arXiv el paper sobre los escalares en los cálculos algebraicos. En este caso es un sistema de tipos que nos permite llevar de cierta manera una cuenta de 'la cantidad de un tipo' que participa en cada término. Acá dejo el link: http://arxiv.org/abs/0903.3741v4.

Ambos casos son análisis del lambda cálculo algebraico-lineal de Pablo Arrighi y Gilles Dowek, el cual fue pensado originalmente como un lambda cálculo cuántico, en el sentido de que permite encodear algoritmos cuánticos y está diseñado de tal manera de no permitir cloneo.

---

It is now available the paper we wrote with Barbara Petit about the analysis of sums in algebraic calculi, presented in Types 2010. Last week we uploaded it to arXiv: http://arxiv.org/abs/1011.3542.

Also last week with Pablo Arrighi we updated in the arXiv our paper about scalars in algebraic calculi. In this case it is a type system which allows us to take care of the 'amount of a type' that participates in each term. Here it is the link: http://arxiv.org/abs/0903.3741v4.

Both papers are analyses of the linear-algebraic lambda-calculus developed by Pablo Arrighi and Gilles Dowek, which was originally thought as a quantum lambda calculus, in the sense that it allows to encode quantum algorithms and it is designed to not allow clonning.

Slides Types 2010

Como ya había adelantado, la semana pasada estuve en Varsovia participando del workshop Types 2010. Los slides de mis presentaciones están disponibles a través de mi página web: Sums in algebraic lambda-calculi y A vectorial type system (work-in-progress).

Hubo en general muy buenas charlas. En particular, les recomiendo ver los slides de la excelente charla de Henk Barendregt: Lambda calculus with types.

Equivalencia de λ-cálculos algebraicos

Como ya adelanté anteriormente, con Simon Perdrix, Christine Tasson y Benoît Valiron tenemos un paper aceptado en el workshop Higer-Order Rewriting que se llevará a cabo en Edimburgo el 14 de Julio.

Ayer enviamos la versión final (extended abstract de 5 páginas + referencias) y subimos la versión completa (con todas las pruebas, 19 páginas) al arXiv.

En este paper lo que hacemos es probar que el Algebraic λ-Calculus de Lionel Vaux (λalg), el cual es un fragmento del differential λ-Calculus, puede simular el Linear-Algebraic λ-Calculus de Pablo Arrighi y Gilles Dowek (λlin), el cual es un candidato a λ-Calculus para computación cuántica, y también probamos la simulación inversa. Ambos cálculos permiten la combinación lineal de términos, sin embargo presentan diferencias a la hora de realizar las reducciones. Por ejemplo en λalg el término


reduce a


en cambio en λlin, ese mismo término reduce a


Las pruebas de simulación se basan en la observación de que esencialmente λlin es call-by-value mientras que λalg es call-by-name. La simulación en un sentido usa la idea de "thunks" y en el otro es una extensión del continuation passing style.

Este paper es un paso hacia probar la dualidad entre ambos cálculos.

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.

A System F accounting for scalars

Hoy hemos enviado la versión extendida del paper del Scalar Type System a un journal internacional. El preprint se puede descargar del arXiv (arXiv:0903.3741).
Esta versión incluye:

• La prueba completa de subject reduction
• La prueba completa de strong normalisation
• La definición formal y prueba del probabilistic type system
• La prueba completa del teorema de no-cloning
  

Vectorial, Lógica Lineal y Ortogonalidad

El miércoles y jueves pasados estuve en Lyon, invitado por Barbara Petit del grupo PLUME de la École Normale Supérieure de Lyon. Allí di un seminario sobre los sistemas de tipos que he desarrollado: Scalar, Additive y Vectorial, y algunos de los problemas sobre cómo chequear ortogonalidad entre términos y algunas pistas para resolverlo.

Olivier Laurent se dio cuenta de simplemente ver la presentación, la conexión entre Additive y Intuitionistic Multiplicative Exponential Linear Logic.

Pronto estaré publicando un nuevo paper sobre Additive (con esa conexión a la lógica lineal) y Vectorial. Además, hemos empezado a trabajar juntos con Barbara en el problema de la ortogonalidad, usando subtyping.

Próximos viajes:
Los días 4 y 5 de Mayo voy a París a visitar a Benoît Valiron y Gilles Dowek del proyecto TypiCal, en la École Polytechnique de París, donde daré otro seminario. Luego, el 18 de Mayo estaré en Chambery, donde iremos con mi director, Pablo Arrighi, a participar de una serie de seminarios organizados por Lionel Vaux del grupo LAMA.

System F escalar: los slides

Subí a mi home page los slides que usé para la presentación del System F escalar. Aquí pueden bajar la versión para ver en pantalla (qpl09-talk.pdf) y aquí una versión print friendly (qpl09-talk-to-print.pdf).

La presentación era de 15 minutos, así que los slides están muy resumidos, lo que puede ser útil para un primer pantallazo sobre de qué se trata. Si les interesa, el paper completo está aquí: arXiv:0903.3741v1.

El workshop en general estuvo muy bueno. Filmaron todas las presentaciones, así que supongo que pronto estarán online (avisaré cuando estén y dónde).

System F escalar: hacia una lógica cuántica.

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)

Y acá dejo el abstract en español:

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).

Update 11/04/09: Slides disponibles
Update 31/07/09: Versión extendida disponible

System F à la Curry y Grupo de trabajo

Buenas!

Les cuento que ya estoy instaladísimo en Grenoble. Lo que he hecho en estos días es adaptar un sistema de tipos polomórficos (System F à la Curry, ver [1], [3] o [4] para más detalles) al Linear-Algebraic Lambda-Calculus de Arrighi y Dowek [2], además hice una prueba de strong normalization (ver [1] o [3]) para este «Linear-Algebraic System F» y algunos comentarios respecto a que este sistema se corresponde de acuerdo al Isomorfismo de Curry-Howard (ver [4]) con la misma lógica (Lógica Proposicional de Segundo Orden) que el System F original. La idea ahora es empezar a jugar con reglas de tipos más complejas, hacer alguna clase de álgebra de tipos, para obtener alguna lógica un poco más loca. Ya les comentaré cuando tenga algo más armado :)

Este próximo jueves nos juntamos con el grupo de trabajo que estamos más o menos en los mismos temas, en lo que le hemos dado a llamar WHOCAS: «(informal) Workshop on Higer-Order Calculi and Algebraic Structures», seremos sólo 5 personas, ya que es un grupo de trabajo más que un workshop: Lionel Vaux, Benoît Valiron, Gilles Dowek, Pablo Arrighi y yo. La idea es que cada uno dará una pequeña charla de 40 minutos contando en qué está trabajando, así vemos qué colaboraciones pueden salir de allí. Luego del WHOCAS publicaré aquí las transparencias que use.

Referencias
[1] Jean-Yves Girard, Yves Lafont, Paul Taylor. Proofs and types. Cambridge University Press, 1989.
[2] Pablo Arrighi, Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. Lecture Notes in Computer Science: (RTA'08), 5117:17-31, 2008. (preprint en arXiv:quant-ph/0612199)
[3] Henk Barendregt. Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science. Clarendon Press, Oxford, 1992.
[4] Morten Sørensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. (disponible para bajar en CiteSeer)

Preparando las valijas

Los últimos posts de este blog han sido demasiado personales para mi gusto (comentando en qué ando). Pero bueno, lo voy a cambiar dentro de poco cuando empieze el doctorado.

Por ahora les comento, el Jueves 9 de Octubre llego a Grenoble, al grupo Quantum Computation in Grenoble, donde iniciaré mi doctorado bajo la dirección de Pablo Arrighi. La idea es que el doctorado dure tres años, espero terminarlo a tiempo :)

El trabajo será en lógica cuántica y teoría de tipos para la computación cuántica, e iré contando detalles a medida que vayamos obteniendo resultados. Mi idea es continuar este blog como un "diario de doctorado", donde iré contando los avances que vayamos teniendo.

Beca francesa

Bonjour!
Les comento que en Setiembre, si todo sale bien, iniciaré mis estudios de doctorado en el Laboratoire d'Informatiqué de Grenoble, Francia, más precisamente en el QCG bajo de dirección de Pablo Arrighi.
La semana pasada me llegó el mail donde me confirman que me han dado la beca! (ahora estoy esperando que me den todos los detalles de cómo tramitar la visa, todo el papelerío necesario, los detalles del monto de la beca, posible alojamiento, etc).
El tema de mi tesis de doctorado es "Models of quantum computation" y aquí pueden ver una descripción del proyecto (en Inglés).
Cómo decirlo.... ESTOY EUFORICO!!!! :)
Au revoir!

Paper sobre medición y confluencia enviado al QPL/DCM y subido al arXiv

El domingo pasado mandamos la versión extendida del paper que se presentará en el próximo QPL/DCM 2008 que se llevará a cabo en Reykjavik, Islandia los próximos 12 y 13 de Julio. Además, subimos esta versión preliminar al arXiv y hoy apareció como arXiv:0806.2447v1 (se puede acceder y descargar gratuitamente desde allí).

Trataré de hacer un muy breve resumen sobre el paper, dejando links a Wikipedia donde sea conveniente (claro que si les interesa enserio, nada mejor que uno o dos buenos libros (mis recomendaciones: "Quantum Computation and Quantum Information" de Michael Nielsen e Isaac Chuang y algún libro de Semántica y sistemas de Reescritura).

Primero, el título: "Measurements and confluence in quantum lambda calculi with explicit qubits", en castellano sería algo así como "Medición y confluencia en Lambda Calculos Cuánticos con qubits explícitos". Trataré de hacer una breve reseña de cada uno de los conceptos que figuran en éste título:

Medición: En Computación Cuántica, la medición es un proceso intrínsecamente probabilístico. O sea, cuando uno mide en qué estado está el sistema, cambia el estado, pero a qué cambia no se sabe con anterioridad, sólo las probabilidades de que cambie a uno u otro estado. Enlace a la Wikipedia (en Inglés).

Confluencia: Es una propiedad deseable de los sistemas de reescritura. La idea básica es: si puedo reescribir un término de mi lenguaje de dos maneras posibles, es necesario que exista otro término al cual ambos puedan "confluir". Enlace a la Wikipedia (en Inglés).

Lambda Cálculo: Es un sistema formal que abstrae el concepto de función. Es la base de los lenguajes de programación funcionales. Enlace a la Wikipedia (en Español).

Lambda Cálculos Cuánticos: Se han realizado muchas extensiones al Lambda Cálculo. Entre ellas, podemos encontrar las extensiones que se hicieron para representar las propiedades cuánticas (como paralelismo, enredo, etc). En el paper pueden encontrar muchas citas sobre estos desarrollos. También pueden ver los excelentes surveys ([1][2]) que han hecho Simon Gay y Peter Selinger.

Con qubits explícitos: Hay algunas extensiones cuánticas al lambda cálculo que manipulan qubits de manera explícita (los símbolos que representan qubits, realmente representan qubits) y hay otros que los manipulan a través de una especie de "punteros", o "memoria" (los símbolos que representan qubits, en realidad son punteros a los mismos).

Ahora sí, habiendo dejando los conceptos en claro: nuestro trabajo presenta un método de cómo agregar medición a aquellas extensiones cuánticas del lambda cálculo que manejan qubits de manera explícita. Y presenta una prueba de confluencia, la cual está hecha de una manera lo suficientemente general como para permitir utilizar el método para sistemas de reescritura probabilísticos en general. En lo particular, el paper está escrito siguiendo las extensiones cuánticas introducidas por André van Tonder, por ser uno de los mas simples.

Hemos trabajado en esto con Pablo Arrighi, Manuel Gadella y Jonathan Grattage, de quienes he aprendido muchísimo.

Categories, Logic and Foundations of Physics: Los videos

Copio (y traduzco) un post de Bob Coecke en el blog The n-Category Café:

Los videos del 2do workshop Categories, Logic and the Foundations of Physics que se realizó en Londres están disponibles aquí. También hay allí algunas charlas del workshop Logic, Physics and Quantum Information Theory organizado por Prakash Panagaden en Barbados. Desafortunadamente algunas de las charlas no salieron muy bien, por ejemplo la de Peter Selinger "completeness result for dagger compact categories". Esperamos poder compensar esto en el workshop Quantum Physics and Logic que se hará en julio en Islandia. Todos los créditos para Ben Jackson y Jamie Vicary por realizar esta filmación y ponerla online.

La fecha para el próximo workshop "Categories, Logic and the Foundations of Physics", el cual será en Oxford, es el 23 y 24 de agosto - dos días esta vez.

Ese congreso en Islandia es donde presentamos y nos fue aceptado el paper sobre medición y confluencia en lambdas cálculos cuánticos. Lamentablemente por razones económicas no podré ir, así que al menos espero poder ver los videos.

Publicada la lista de papers aceptados para el QPL

El paper que enviamos al QPL fue aceptado para una exposición completa de 30 minutos (en contraposición con una exposición corta de 15 minutos). La lista completa de los papers aceptados está publicada en la página del evento.

Medición y confluencia en lambda cálculos cuánticos con qubits explícitos

Ayer llegué de Francia. Estuve 2 semanas en Grenoble y 2 semanas en Orsay.

En Grenoble estuvimos trabajando con Pablo Arrighi y Jonathan Grattage en extender mi tesis de grado de agregado de medición al Lambda Cálculo cuántico de van Tonder[1]. La idea fue extenderlo para probar confluencia y dejar el método lo suficientemente general para que pueda ser fácilmente usado para extender otros lambda cálculos (en particular, ahora estamos trabajando en extender el lambda cálculo de Pablo[3,4], que es quien me invitó a Grenoble, y el QML de Jon[5,6], también investigador en Grenoble).

Hoy enviamos el extended abstract al QPL08 que se realizará en Reykjavík, Islandia los próximos 12 y 13 de Julio. Update: (16/6/08) En un post reciente pueden encontrar la versión extendida, la cual tiene varios cambios sustanciales

El 21 de Abril nos avisarán si el paper ha sido aceptado.

Esas dos semanas y el tiempo que le siguió, he aprendido muchísimo! Ahora Pablo está tramitando una beca para ver si puedo empezar mi doctorado allí en Setiembre.

En Orsay también fueron muy amables, y también aprendí mucho. Ellos están trabajando en algoritmos y complejidad (cuánticos), un tema que no conocía en profundidad.

Tanto en Grenoble como en Orsay, dí una charla sobre mi tesis de grado, los slides los pueden obtener de aquí. (Igualmente si les interesa el tema, les recomiendo leer el extended abstract, ya que tiene algunos cambios bastante importantes).

Referencias.

[1] A. van Tonder. A lambda calculus for quantum computation. SIAM Journal on Computing, 33(5):1109-1135, 2004. (también en arXiv:quant-ph/0307150).

[2] P. Arrighi y G. Dowek. A computational definition of the notion of vectorial space. Electronic Notes in Theoretical Computer Science, 117:249-261, 2005. (también disponible en la página de Gilles Dowek).

[3] P. Arrighi y G. Dowek. Linear-algebraic lambda-calculus: higher-order, encodings and confluence. Enviado a RTA'08 (también en arXiv:quant-ph/0612199).

[4] T. Altenkirch y J. J. Grattage. A functional quantum programming language. En Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 2005. (también en arXiv:quant-ph/0409065).

[5] T. Altenkirch, J. J. Grattage, J. K. Vizzotto, y A. Sabry. An algebra of pure quantum programming. Electronic Notes in Theoretical Computer Science, 170:23-47, 2007. (también en arXiv:quant-ph/0506012).

Volviendo a Francia

La semana que viene, más precisamente el 2 de Marzo, me voy a pasar un mes a Francia, estaré del 3 al 15 con el grupo de Pablo Arrighi en Grenoble y del 16 al 29 con el grupo de Miklos Santha en Orsay, quienes me han invitado.

Ambos grupos trabajan con Funcional Cuántico (entre otras cosas), un tema que cada día me apasiona más (y que cada día me doy más cuenta de lo poco que sé). Espero aprender mucho de ellos!

Video de la presentación de Tesis

Lo prometido: el video de la presentación "Agregando Medición al Cálculo de van Tonder". Los créditos para mi hermana y mi novia por la excelente filmación :).

Los slides los pueden bajar de aquí (versión para imprimir), y en unos días subiré el informe de tesis completo (le estoy arreglando algunos detalles que no me gustaron). Dejo un draft.

Obteniendo mi título

Después de una larga ausencia por este blog, paso a contar la causa: Estuve estudiando a full para llegar a recibirme antes de terminar el año.

Y llegó el momento de presentar mi Tesis de Licenciatura en Ciencias de la Computación:

Día y Hora:

Viernes 21 de Diciembre de 2007, 10:45hs

Lugar:

Aula 23, Pellegrini 250, Rosario.
Facultad de Ciencias Exactas, Ingeniería y Agrimensura
Universidad Nacional de Rosario

Título de la tesis:

Agregando medición al Cálculo de van Tonder

Tesista:

Alejandro Díaz-Caro

Director:

Dr. Manuel Gadella

Co-Director:

Dr. Pablo Martínez López

Resumen:

El área de los lenguajes de programación cuánticos se está desarrollando a una gran velocidad. En particular, se han definido varias extensiones al Lambda Cálculo que proveen la sintaxis y semántica necesarias para modelar algoritmos cuánticos.
Uno de los trabajos más influyentes en este sentido es el \lambda_q de André van Tonder[1]. Este es un Lambda Cálculo, definido mediante su semántica operacional, para cómputos puramente cuánticos: la medición no es parte del cálculo.
La intención de este trabajo es agregar medición al \lambda_q, para lo cual nos valemos de algunas herramientas del Lambda Cálculo probabilístico definido por Di Pierro, Hanking y Wiklicky en [2]. Además, siguiendo la línea de trabajo de van Tonder, también hacemos uso de la la sintaxis para la lógica lineal de Philip Wadler[3].

Ref:
[1] A. van Tonder, "A Lambda Calculus for Quantum Computation", SIAM J. Comput. 33(5), Society for Industrial and Applied Mathematics, 1109–1135, 2004
[2] A. Di Pierro, C. Hankin y H. Wiklicky, "Probabilistic Lambda-calculus and Quantitative Program Analysis", Journal of Logic and Computation 15(2), 159–179, 2005
[3] P. Wadler, "A Syntax for Linear Logic", Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, Springer-Verlag, 513–529, 1994


En algunos días subiré el PDF completo de la tesis y el PDF de la presentación (En otro post).

---

Update: Ya soy licenciado! Dejo algunas fotos (hay más en mi album picasa) y en unos días subiré el video de la presentación en otro post está el video de la presentación.

Antes de empezar, esperando a que llegue el director de escuela.

Abrazos y felicitaciones luego de la presentación.

Una vieja tradición argentina: Los compañeros y amigos ensucian a los egresados con huevos, harina, yerba mate, gaseosa y todo lo que se encuentre a la mano.

La foto de grupo, luego de los huevos. Por algún motivo nadie me quiso abrazar :P

Lenguajes de Programación Cuánticos

A todo aquel que le interesen los lenguajes de programación que se están desarrollando para la computación cuántica, les recomiendo el -bastante exhaustivo- review de Simon J. Gay: Quantum Programming Languages: Survey and Bibliography[1]
Además, en su página pueden encontrar un buscador de papers sobre el tema.

Ref:
[1] Mathematical Structures in Computer Science 16(4), 2006

Lambda Cálculo Cuántico

El viernes pasado dí una charla sobre el Lambda Cálculo Cuántico definido por André van Tonder[1] como parte de un ciclo de charlas sobre programación funcional organizadas por el Dr. Pablo E. Martínez López (a.k.a. Fidel).

Dejo las transparencias para quien quiera ver un poco de qué se trata (y también la versión para imprimir), aunque por supuesto, recomiendo recurrir a la fuente.

Ref.
[1] André van Tonder, "A Lambda Calculus for Quantum Computation". SIAM J. Comput. 33, 5 (May. 2004), 1109-1135. (preprint en arXiv)