An interesting intervention of Scott Aaronson at the TEDx organized at Caltech
via La Consigna
Blog sobre computación cuántica y fundamentos de las ciencias de la computación. En general cubrimos los temas de investigación a los que nosotros nos dedicamos, los cuales comenzaron siendo computación cuántica, y con el tiempo van evolucionando, cambiando, agregando nuevas áreas, etc.
28 de febrero de 2011
27 de febrero de 2011
Cotas inferiores para funciones booleanas simétricas
Últimamente he estado estudiando una técnica para encontrar cotas inferiores para árboles de decisión basadas en polinomios. Básicamente, la función booleana se escribe como si fuera un polinomio, e.g. x1∧x2 se puede escribir como un polinomio en dos variables p(x1,x2)=x1⋅x2. Entonces el número de consultas al oráculo es exactamente el grado del polinomio. Para el ejemplo del and tenemos que este número es 2.
Bueno, hay un resultado en computación cuántica que dice que el número de consultas que hace un algoritmo a un oráculo cuántico está acotado por abajo por el grado de un polinomio de bajo grado que aproxima la función booleana. Este es el link al paper original que desarrolló la técnica.
Ahora consideremos la función threshold, donde Thrt(x)=1 si y solo si el número de 1s en x es mayor o igual a t, i.e. |x|≥t. La cota inferior reportada en muchos papers es de(n-t+1)} "\sqrt{(t+1)(n-t+1)}")
. Existe un teorema (Paturi 1992) basado en el método de los polinomios. Este teorema nos permite calcular la cota inferior para cualquier función booleana simétrica. Una función booleana f es simétrica, si dado cualquier entrada x, permutar el orden de los bits no cambia el valor de f(x). Claramente Thrt es simétrica.
Tengo una pregunta en Theoretical Computer Science Stack Exchange que está sin respuesta ya por unos días. Básicamente el problema es que la cota inferior para threshold indicada arriba no sigue en forma directa desde el teorema de Paturi.
Creo que voy a esperar unos días más, y si sigue sin respuesta voy a poner una recompensa. Pero si algún lector de este blog conoce la respuesta, le voy a estar muy agradecido :-)
Bueno, hay un resultado en computación cuántica que dice que el número de consultas que hace un algoritmo a un oráculo cuántico está acotado por abajo por el grado de un polinomio de bajo grado que aproxima la función booleana. Este es el link al paper original que desarrolló la técnica.
Ahora consideremos la función threshold, donde Thrt(x)=1 si y solo si el número de 1s en x es mayor o igual a t, i.e. |x|≥t. La cota inferior reportada en muchos papers es de
Tengo una pregunta en Theoretical Computer Science Stack Exchange que está sin respuesta ya por unos días. Básicamente el problema es que la cota inferior para threshold indicada arriba no sigue en forma directa desde el teorema de Paturi.
Creo que voy a esperar unos días más, y si sigue sin respuesta voy a poner una recompensa. Pero si algún lector de este blog conoce la respuesta, le voy a estar muy agradecido :-)
4 de febrero de 2011
QPL 08 y 09 en Electronic Notes in Theoretical Computer Science
El primer paper internacional que publiqué, en el QPL 2008, finalmente apareció en Electronic Notes in Theoretical Computer Science. Los editores se demoraron un poco (bastante), pero finalmente publicaron los proceedings de este workshop.
Y acá les dejo la cronología en el blog de este paper :)
- Acá está el post de cuando lo enviamos.
- Acá cuando nos avisaron que fue aceptado
- Acá cuando mandamos la versión final.
- Y finalmente, este post para la versión publicada :)
-
Y la cosa no queda allí, también los mismos editores enviaron los papers del QPL 2009! Allí encontrarán la primera versión de Scalar, en el siguiente número de ENTCS (esta es una versión de sólo 10 páginas, la versión de arXiv está mucho más completa). Este fue el primer paper durante mi doctorado, y como no podía ser de otra manera, la cronología también está reflejada en nuestro blog:
- Aquí cuando fue aceptado,
- y luego los slides de mi presentación y la versión arXiv.
3 de febrero de 2011
2 nuevos: λFA y λvec
El miércoles envié dos nuevos papers:
El primero está basado en la tesis de licenciatura, en progreso, de Pablo Buiras. El paper lo escribimos entre Pablo, Mauro Jaskelioff, y yo (sus directores). Pueden bajar el paper libremente del arXiv: arXiv:1102.0749.
El título del paper es
Acá copio el abstract y explico un poquito de qué se trata "en criollo".
En lugar de traducir el abstract, explico un poquito la idea: En [DCP10] Barbara Petit y yo creamos un sistema de tipos, λadd, para el fragmento aditivo del linear-algebraic lambda-calculus [AD08] (λlin para abreviar). Luego mostramos que ese cálculo podía traducirse a System F con pares.
En el nuevo trabajo, extendemos ese resultado para el cálculo λlin completo: Primero creamos un sistema de tipos muy similar a λadd, pero para todo el cálculo: o sea, no sólo para lambda términos que se pueden sumar, como t+r, con t y r lambda términos, sino que también se pueden escalar: α.t+β.r, con α, β reales positivos. El sistema se llama λFA (por Full-Additive). La sintaxis de los tipos sigue siendo la misma que la de λadd : básicamente es Sistem F donde además se pueden sumar tipos. Y los escalares? Bueno, lo que hacemos es aproximarlos tomando su parte entera: si un término t tiene tipo T, el término α.t:⌊α⌋.T (nótese que ⌊α⌋ es un número natural y por tanto ⌊α⌋.T no es más que T+T+····+T, ⌊α⌋-veces). Como alguno ya inferirá, mezclar escalares y sumas no es nada sencillo, por ejemplo: 1/2.t+1/2.t tendría tipo ⌊1/2⌋.T+⌊1/2⌋.T = 0.T+0.T = 0, sin embargo si tomamos números mayores (por ejemplo, multipliquemos todo por 100), pues la precisión será muy buena... bueno, depende de lo que queramos decir por "muy buena", pero si no nos parece buena, pues agregamos más 0s al 100 :)
Probamos una especie de subject reduction para este sistema: básicamente lo que dice que se pierde precisión en los escalares al reducir el término, pero no en los tipos. O sea, si un término tiene tipo T+R+S+S, pues sabemos que al reducirlo (al "ejecutar el programa"), obtendremos un término con al menos los tipos T, R y dos veces S.
Además hicimos una prueba de strong normalisation: algo no sencillo ya que la prueba de Scalar [ADC09] no nos sirve porque en Scalar sólo se puede tipar t+r si t y r tienen el mismo tipo (módulo un escalar), por lo tanto el conjunto de términos no es el mismo. Tampoco se puede re-usar la de λadd, porque allí los escalares en los términos no existen (por lo tanto también tenemos otro conjunto de términos), así que hubo que hacer una prueba desde cero.
Por último, mostramos que λadd se comporta como una interpretación abstracta de λFA, y luego conjeturamos (con muchas pistas de que la conjetura es cierta), que System F con pares por extensión también es una interpretación abstracta de λFA.
-
El segundo paper es un trabajo con Pablo Arrighi y Benoît Valiron y es una extensión (o digamos, la continuación) de este. El título es:
Abstract:
Básicamente los cambios con respecto al viejo son: volvimos a agregar una regla de reescritura que habíamos quitado previamente (usando un truco para que ahora sí funcione), haciendo que el sistema sirva para todo el cálculo λlin, y lo más importante: λlin originalmente (el cálculo no tipado) podía encodear programas cuánticos. Ninguno de los sistemas de tipos en los que trabajé hasta ahora podía hacerlo, Scalar puede tipar programas con distribuciones baricéntricas, λadd podría pensarse como no determinista y λFA podrían ser usado para tipar programas probabilísticos, pero este es el primero que permite tipar los programas cuánticos propuestos en el paper original.
El primero está basado en la tesis de licenciatura, en progreso, de Pablo Buiras. El paper lo escribimos entre Pablo, Mauro Jaskelioff, y yo (sus directores). Pueden bajar el paper libremente del arXiv: arXiv:1102.0749.
El título del paper es
Lower bounds for scalars in a typed algebraic λ-calculus
(Cotas inferiores para escalares en un λ-cálculo algebraico tipado)
The linear-algebraic λ-calculus is an untyped λ-calculus extended with arbitrary linear combinations of terms. As shown by previous works, building a type system on top of it is a delicate matter. A straightforward extension of a classic type system, like System F, would impose an undesirable restriction: it would only allow superpositions of terms of the same type. Adding sums of types lifts this restriction but raises the question of how to deal with the interaction between scalars and additions. We propose a type system with sums of types for the linear-algebraic λ-calculus which provides an answer to this question by allowing types to have some degree of imprecision. The proposed type system has a subject reduction property and is strongly normalising. Furthermore, we show that the additive fragment of the calculus can be seen as an abstract interpretation of the full calculus.
En lugar de traducir el abstract, explico un poquito la idea: En [DCP10] Barbara Petit y yo creamos un sistema de tipos, λadd, para el fragmento aditivo del linear-algebraic lambda-calculus [AD08] (λlin para abreviar). Luego mostramos que ese cálculo podía traducirse a System F con pares.
En el nuevo trabajo, extendemos ese resultado para el cálculo λlin completo: Primero creamos un sistema de tipos muy similar a λadd, pero para todo el cálculo: o sea, no sólo para lambda términos que se pueden sumar, como t+r, con t y r lambda términos, sino que también se pueden escalar: α.t+β.r, con α, β reales positivos. El sistema se llama λFA (por Full-Additive). La sintaxis de los tipos sigue siendo la misma que la de λadd : básicamente es Sistem F donde además se pueden sumar tipos. Y los escalares? Bueno, lo que hacemos es aproximarlos tomando su parte entera: si un término t tiene tipo T, el término α.t:⌊α⌋.T (nótese que ⌊α⌋ es un número natural y por tanto ⌊α⌋.T no es más que T+T+····+T, ⌊α⌋-veces). Como alguno ya inferirá, mezclar escalares y sumas no es nada sencillo, por ejemplo: 1/2.t+1/2.t tendría tipo ⌊1/2⌋.T+⌊1/2⌋.T = 0.T+0.T = 0, sin embargo si tomamos números mayores (por ejemplo, multipliquemos todo por 100), pues la precisión será muy buena... bueno, depende de lo que queramos decir por "muy buena", pero si no nos parece buena, pues agregamos más 0s al 100 :)
Probamos una especie de subject reduction para este sistema: básicamente lo que dice que se pierde precisión en los escalares al reducir el término, pero no en los tipos. O sea, si un término tiene tipo T+R+S+S, pues sabemos que al reducirlo (al "ejecutar el programa"), obtendremos un término con al menos los tipos T, R y dos veces S.
Además hicimos una prueba de strong normalisation: algo no sencillo ya que la prueba de Scalar [ADC09] no nos sirve porque en Scalar sólo se puede tipar t+r si t y r tienen el mismo tipo (módulo un escalar), por lo tanto el conjunto de términos no es el mismo. Tampoco se puede re-usar la de λadd, porque allí los escalares en los términos no existen (por lo tanto también tenemos otro conjunto de términos), así que hubo que hacer una prueba desde cero.
Por último, mostramos que λadd se comporta como una interpretación abstracta de λFA, y luego conjeturamos (con muchas pistas de que la conjetura es cierta), que System F con pares por extensión también es una interpretación abstracta de λFA.
-
El segundo paper es un trabajo con Pablo Arrighi y Benoît Valiron y es una extensión (o digamos, la continuación) de este. El título es:
A type system for the vectorial aspects of the linear-algebraic lambda-calculus
(Un sistema de tipos para los aspectos vectoriales del linear-algebraic lambda-calculus)
Abstract:
In this paper we describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors. The type system is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.
Básicamente los cambios con respecto al viejo son: volvimos a agregar una regla de reescritura que habíamos quitado previamente (usando un truco para que ahora sí funcione), haciendo que el sistema sirva para todo el cálculo λlin, y lo más importante: λlin originalmente (el cálculo no tipado) podía encodear programas cuánticos. Ninguno de los sistemas de tipos en los que trabajé hasta ahora podía hacerlo, Scalar puede tipar programas con distribuciones baricéntricas, λadd podría pensarse como no determinista y λFA podrían ser usado para tipar programas probabilísticos, pero este es el primero que permite tipar los programas cuánticos propuestos en el paper original.
El cálculo se llama λvec (bueno, el nombre correcto sería 
).
Aún no lo subimos al arXiv, pero lo que vamos a hacer es actualizar el anterior, ya que es su versión final (ah, por cierto, el anterior, que sería la versión "work-in-progress" de este, fue aceptado y lo vamos a presentar en QAPL 2011 (sólo como presentación, sin aparecer en los proceedings ya que es un work-in-progress)).Cuando aparezca la versión nueva en arXiv pondré el link aquí. Lo pueden bajar de aquí: arXiv:1012.4032.
Aún no lo subimos al arXiv, pero lo que vamos a hacer es actualizar el anterior, ya que es su versión final (ah, por cierto, el anterior, que sería la versión "work-in-progress" de este, fue aceptado y lo vamos a presentar en QAPL 2011 (sólo como presentación, sin aparecer en los proceedings ya que es un work-in-progress)).
Suscribirse a:
Entradas (Atom)