Barbara Petit y yo hemos enviado un paper para revisión. En este trabajo, hacemos un análisis de la linealidad en el lambda cálculo algebraico lineal (Lineal), y la comparamos con la linealidad de lógica lineal.
En lógica lineal, una función es lineal, si utiliza una sola vez su argumento. Así, f(x)=x² no es lineal (ya que utiliza su argumento x dos veces), mientras f(x)=x+1 sí. En Lineal una función f(x+y) se toma como f(x)+f(y), imitando la definición de las funciones lineales en álgebra (o, tal es el objetivo, la multiplicación de matrices por vectores, como en computación cuántica).
En este nuevo paper definimos un sistema de tipos para Lineal (o para ser más precisos, para el fragmento de Lineal que sólo tiene sumas, ya que es la parte que nos interesa, y que además coincide con varios lenguajes no-deterministas). Este sistema de tipos caracteriza las superposiciones y la linealidad del lenguaje. Luego mostramos que este sistema se puede traducir en Sistema F con pares, el cual se corresponde con el fragmento no-lineal de IMELL (el fragmento intuisionista, multiplicativo, exponencial de la lógica lineal). Esto plantea la primera sorpresa: el cálculo Lineal se traduce en un fragmento no-lineal de la Lógica Lineal.
En realidad lo que sucede, es que Lineal se mantiene fiel a la computación cuántica, donde x+y representa una superposición de x e y, los cuales son atómicos, y una función que duplique su argumento, por ejemplo, es perfectamente válido, siempre y cuando sólo pueda duplicar elementos atómicos. Por tanto, f(x+y) se toma como f(x) + f(y) y no habrá problema en que f duplique su argumento. O sea, Lineal considera que todas sus funciones son lineales, no las fuerza a ser lineales, sólo las trata como tales, lo cual es necesario para evitar el clonado, operación prohibida en computación cuántica, y es suficiente ya que lo interesante en Lineal es que puede encodear operadores cuánticos, que son siempre lineales.
Update: el paper fue acceptado en WoLLIC 2012. Acá dejo un post sobre eso.
Pueden bajar el paper libremente desde arXiv o desde su sitio final de publicación (si tienen acceso) en Springer.
Update 2: slides de un seminario pre-conferencia.
En lógica lineal, una función es lineal, si utiliza una sola vez su argumento. Así, f(x)=x² no es lineal (ya que utiliza su argumento x dos veces), mientras f(x)=x+1 sí. En Lineal una función f(x+y) se toma como f(x)+f(y), imitando la definición de las funciones lineales en álgebra (o, tal es el objetivo, la multiplicación de matrices por vectores, como en computación cuántica).
En este nuevo paper definimos un sistema de tipos para Lineal (o para ser más precisos, para el fragmento de Lineal que sólo tiene sumas, ya que es la parte que nos interesa, y que además coincide con varios lenguajes no-deterministas). Este sistema de tipos caracteriza las superposiciones y la linealidad del lenguaje. Luego mostramos que este sistema se puede traducir en Sistema F con pares, el cual se corresponde con el fragmento no-lineal de IMELL (el fragmento intuisionista, multiplicativo, exponencial de la lógica lineal). Esto plantea la primera sorpresa: el cálculo Lineal se traduce en un fragmento no-lineal de la Lógica Lineal.
En realidad lo que sucede, es que Lineal se mantiene fiel a la computación cuántica, donde x+y representa una superposición de x e y, los cuales son atómicos, y una función que duplique su argumento, por ejemplo, es perfectamente válido, siempre y cuando sólo pueda duplicar elementos atómicos. Por tanto, f(x+y) se toma como f(x) + f(y) y no habrá problema en que f duplique su argumento. O sea, Lineal considera que todas sus funciones son lineales, no las fuerza a ser lineales, sólo las trata como tales, lo cual es necesario para evitar el clonado, operación prohibida en computación cuántica, y es suficiente ya que lo interesante en Lineal es que puede encodear operadores cuánticos, que son siempre lineales.
Update: el paper fue acceptado en WoLLIC 2012. Acá dejo un post sobre eso.
Pueden bajar el paper libremente desde arXiv o desde su sitio final de publicación (si tienen acceso) en Springer.
Update 2: slides de un seminario pre-conferencia.
0 comments:
Publicar un comentario