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)
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í.
0 comments:
Publicar un comentario