Non determinism through type isomorphism

(English below)

Con Gilles Dowek hemos enviado un nuevo artículo para revisión. Una versión muy preliminar de este artículo es lo que presentamos en la semana Enfoques Cuantitativos del LI2012.

Aquí dejo una traducción del título y resumen:

No determinismo por medio de isomorfismo de tipos 

Definimos una relación de equivalencia sobre proposiciones y un sistema de pruebas donde proposiciones equivalentes tienen la misma prueba. El sistema obtenido es similar a varios lambda-cálculo no determinísticos y algebraicos. Este sistema tiene preservación de tipos y normalización fuerte.

En las conclusiones del artículo se pueden ver varios problemas para trabajos futuros, y la posible conexión con los lenguajes cuánticos.

Actualización: El paper ha sido aceptado en LSFA 2012. La versión corregida se encuentra disponible en mi página web (próximamente en EPTCS) en EPTCS 113:137-144, 2013.

---

Gilles Dowek and I have just sent a paper for review. A very preliminary version of this paper is what we presented in the Quantitative Approaches week of LI2012.

Here is the abstract:

Non determinism through type isomorphism 

We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi. This system enjoys subject reduction and strong normalisation.

Update: The paper has been accepted in LSFA 2012. The corrected version is available for download from my web page. (soon at EPTCS) EPTCS 113:137-144, 2013.

WECIQ 2012

(English below)

Del 8 al 12 de Octubre, en la ciudad de Fortaleza, Brasil, se llevará a cabo el IV Workshop-Escuela en Computación e Información Cuántica - WECIQ 2012. Tuve la grata experiencia de asistir al primero de estos workshops, en 2006 (cuando aún era estudiante de la licenciatura), y hasta blogueé sobre ello!

La opinión que me generó por ese entonces, es la misma que tengo ahora: los brasileños son los punteros sudamericanos en computación cuántica, por lo cual un workshop nacional sobre estos temas, es sin lugar a dudas un buen lugar para asistir y conocer qué se está haciendo a nivel sudamericano en el área.

---

From 8 to 12 October, in Fortaleza, Brazil will be held the IV Worksop-School in Quantum Computation and Information - WECIQ 2012. I had the pleasure of attending the first of this series, in 2006 (while still an undergraduate), and I have even blogued about it!

My view at that time is the same that I have today: Brazil is the leading country in South America in quantum computation and information, so a Brazilian national workshop on these topics is, without doubt, a great place to go and see what  it is being done in South America in this field.

No-determinismo en llamada por valor, en una disciplina de tipos à la lógica lineal

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.