21 de julio de 2011

LSFA (y QuAND!)

Con Pablo Buiras, a quien estoy dirigiendo en su tesis de licenciatura (el equivalente a la tesis de master en el sistema de la Unión Europea) y Mauro Jaskelioff, su codirector, hemos escrito un paper basado en la tesis de Pablo, que fue aceptado en LSFA 2011. Será Pablo quien lo presente allí.

El paper aborda el problema de la confluencia del lambda cálculo algebraico lineal por medio de un sistema de tipos (el cual permite sólo términos fuertemente normalizables, lo que en conjunto con la confluencia local, nos da la confluencia del lenguaje). Este sistema de tipos puede verse como una extensión de Additive al cálculo completo o como una simplificación de Vectorial. Tiene la ventaja de que, al igual que Additive, sólo introduce sumas en los tipos, y no escalares como lo hace Vectorial, lo cual lo haría mucho más complejo y difícil de interpretar en otros sistemas conocidos. Además, da información aproximada de qué es lo que está pasando en el término: por ejemplo, si tenemos un término 2.1 M + 1.5 N donde M tiene tipo T y N tipo R, el tipo de esta combinación lineal de términos será T+T+R, dicho de otro modo, el tipo "aproxima las cantidades" de términos de cada tipo que están presentes en la combinación, tomando su parte entera.

El paper completo (el borrador, claro, aún tenemos tiempo para enviar la versión definitiva) lo pueden bajar de acá. Y el lunes pasado presenté el trabajo (con un cambio, ya que en mi presentación la normalización fuerte la derivo a partir de la normalización fuerte de Vectorial) en el encuentro del proyecto QuAND. Los slides de esa presentación están acá.

La versión definitiva del paper será publicada en el Electronic Proceedings in Theoretical Computer Science, una revista científica electrónica que suele publicar los anales de workshops y conferencias, y que tiene la particularidad de ser abierta: cualquiera puede descargarse sus artículos, no hace falta pagar por ello.

Update 25/03/12: Los proceedings del workshop han aparecido. Pueden bajar la versión publicada del paper desde aquí.