La semana pasada hemos enviado un nuevo paper para revisión con Giulio Manzonetto y Michele Pagani. El título en inglés "Call-by-value non-determinism in a linear logic type discipline" (perdón por mi mala traducción al español). En este paper presentamos un sistema de tipos intersección, basado en lógica lineal, para un cálculo no determinista, donde si M y N son términos del cálculo, la elección no determinista entre ellos se expresa como M+N o M||N, dependiendo el tipo de convergencia que queramos: cada vez que hay una elección no determinista M+N, el sistema puede elegir entre uno o el otro. Con que uno de ambos converja, diremos que el término es convergente. En cambio, una elección no determinista M||N demandará que ambos términos converjan, por lo cual se continuará el cálculo hasta el final con ambas opciones en paralelo. Esto hace que, por ejemplo, si M y N son máquinas que toman un argumento R, la máquina no determinista M||N aplicada al argumento R se expresará mediante la reducción (M||N)R → MR||NR. En cambio, (M+N)R→MR o NR, ya que no nos interesan ambas opciones.
En la literatura estas dos opciones se conocen como may-convergence (+) y must-convergence (||). En este trabajo presentamos un sistema de tipos tal un término es convergente si y sólo si es tipable. A modo de ejemplo, si M es convergente: M+Y, donde Y→Y (o sea, Y no es convergente), tiene tipo en nuestro sistema, ya que el término M+Y puede converger ("may converge").
Más aún, el sistema de tipos cuenta con una medida, la cual nos da una cota de la cantidad de pasos necesarios para la convergencia (la cual es exacta si ciertas condiciones de minimalidad en el tipado se cumplen).
Estos modelos no deterministas se pueden considerar como una versión simplificada de un modelo cuántico, donde sólo interesa estudiar la superposición, sin tener en cuenta las amplitudes.
El borrador del paper estará disponible en mi página (mientras siga siendo sólo un borrador): dmp12.pdf.
No hay comentarios:
Publicar un comentario