Types 2010

Ya está publicada la lista de charlas y cronograma de Types 2010. Yo presentaré dos charlas allí:

• Sumas en cálculos lambda algebraicos. Un trabajo conjunto con Barbara Petit. En este trabajo definimos el fragmento (confluente) "aditivo" del Linear-Algebraic Lambda-Calculus. Le definimos un sistema de tipos que incluye sumas de tipos como reflejo de las sumas en los términos. Luego de probar subject reduction y strong normalisation, estudiamos el rol de las sumas en el cálculo interpretando nuestro sistema en System F con pares. Mostramos que este cálculo se puede interpretar como System F con un constructor de pares asociativo y conmutativo, el cual es distributivo con respecto a la aplicación.
• Un sistema de tipos vectorial. Un trabajo en colaboración con Pablo Arrighi y Benoît Valiron. El objetivo de este trabajo es combinar Scalar con Additive (el de más arriba) para crear un sistema de tipos al estilo System F para el Linear-Algebraic Lambda-Calculus el cual nos de una teoría de tipos general y original donde los tipos, de la misma manera que los términos, tengan una estructura de espacio vectorial. Mencionamos las conexiones con computación cuántica.

Luego de las charlas subiré aquí los slides. Aquí están.

Más novedades: Caminatas Cuánticas

Reciéntemente (la semana pasada) he tomado y pasado con éxito lo que se conoce como exámen de cualificaciones (del inglés qualifying exam), aunque aquí en Japón lo llaman simplemente "exámen de ingreso al doctorado". Tuve que hacer una pequeña presentación de lo que hice hasta este momento y lo que planeo hacer en el futuro. Ya más adelante voy a comentar sobre lo que voy a hacer (de hecho ya lo comencé), pero ahora paso a transcribir un resumen que describe lo hecho hasta ahora.

Actualmente hay un gran interés en el diseño de algoritmos cuánticos utilizando el paradigma de las caminatas cuánticas. Generalmente, la construcción de algoritmos cuánticos resulta muy difícil, y la utlización de este paradigma resulta ser un enfoque muy prometedor. Las caminatas cuánticas fueron definidas en analogía a las caminatas aleatorias y las cadenas de Markov, y se espera que tengan el mismo éxito para el diseño y análisis de algoritmos cuánticos. Varios algoritmos utilizando caminatas cuánticas ya fueron descubiertos para verificación de multiplicación de matrices, búsqueda de triángulos en grafos, conmutatividad de grupos, por nombrar algunos. Clásicamente, la principal métrica de complejidad para algoritmos basados en cadenas de Markov es el hitting time. Es comúnmente definido como el número esperado de pasos para encontrar un conjunto de vértices marcados en un grafo, y está directamente relacionado con el tiempo de ejecución de los algoritmos aleatorios. De la misma forma, se puede definir una noción similar para caminatas cuánticas, pero esto resulta muy delicado. Si observamos la posición de la caminata sobre un grafo en cada paso, el sistema cuántico colapsa (de acuerdo a los postulados de la mecánica cuántica y el efecto Zenon cuántico), y no tiene ningún sentido tratar de explotar efectos mecánico-cuánticos para aceleración algorítmica. Por lo tanto, hay que tener mucho cuidado al definir una noción adecuada de hitting time. En este trabajo se estudia tal noción llamada One-Shot Hitting Time, y nos concentramos solamente en caminatas de tiempo discreto. Esta investigación está dividida en dos partes: i) líneas, y ii) grillas de 2 dimensiones. Para la primera parte, se propone una caminata que utiliza un operador con parámetros de fase a cargo de entonar la desviación estándar de la distribución de probabilidades inducida sobre la línea. Fórmulas para la evolución en el tiempo de la caminata fueron deducidas utilizando un método de punto silla para aproximación asintótica. Para este fin, como en trabajo anteriores, fue utilizado el análisis de Fourier para simplificar el estudio. También describimos la asintótica demostrando la convergencia débil de la caminata. Estos resultados dan una descripción precisa de los one-shot hitting times sobre la línea. Para la segunda parte, el análisis mencionado arriba no puede utilizarse debido a la complejidad de la fórmulas resultantes. Por lo tanto nos concentramos en acotar el hitting time y la probabilidad de encontrar un vértice arbitrario sobre la grilla. En una grilla de 2 dimensiones de tamaño n es demostrado, utilizando los modelos de caminatas cuánticas con monedas y basadas en cadenas de Markov, un hitting time de O(√n) con una probabilidad de éxito acotada para el primero, y no acotada para el segundo. Estos resultados pueden ser utlizados para aplicaciones algorítmicas en búsqueda espacial y ruteo de redes cuánticas.

La parte de aplicaciones aún la tengo que trabajar para tener todo bien cerrado. Estoy considerando utilizar para el caso de ruteo el modelo de cadenas de espines para transferencia de estados cuánticos. Esto me fue sugerido por Joe Fitzsimons aquí. Parece muy prometedor, pero aún debo de estudiarlo bien.

Algunas novedades

Estos 3 últimos meses fueron de los más atareados que he tenido, y aún no me desocupo y tengo varias cosas sobre que escribir. Mientras tanto algunas novedades:

1. Fui a AQIS'10 para presentar este trabajo. La conferencia estuvo simplemente excelente con muy buenas presentaciones dadas por reconocidos investigadores como Andrew Yao, Harry Buhrman, Richard Jozsa y otros. Conocí a otros investigadores y en especial a Luciano Aparicio de Argentina de la Universidad de Tokyo. El estudia con Rodney Van Meter en "multiplexación de información cuántica para ruteo en redes" quien resultó ser una persona muy agradable y aproveché para pedirle los slides de su presentación de video en youtube sobre el cual había escrito aquí. Al final puso un link en su página personal para acceder a los slides.
2. Ya está habilitado para su acceso al público en general el sitio web de preguntas y respuestas sobre computación teórica CSTheory. Se requiere que las preguntas y respuestas sean de nivel de investigación. Hay varias personas colaborando en esto de todas las áreas de las ciencias de la computación.
3. Ya está el CFP de STOC'11.
4. También la conferencia LAGOS'11 que se llevará a cabo en Bariloche. Esto es para los fanáticos de teoría de grafos.