18 de mayo de 2010

Equivalencia de λ-cálculos algebraicos

Como ya adelanté anteriormente, con Simon Perdrix, Christine Tasson y Benoît Valiron tenemos un paper aceptado en el workshop Higer-Order Rewriting que se llevará a cabo en Edimburgo el 14 de Julio.

Ayer enviamos la versión final (extended abstract de 5 páginas + referencias) y subimos la versión completa (con todas las pruebas, 19 páginas) al arXiv.

En este paper lo que hacemos es probar que el Algebraic λ-Calculus de Lionel Vauxalg), el cual es un fragmento del differential λ-Calculus, puede simular el Linear-Algebraic λ-Calculus de Pablo Arrighi y Gilles Doweklin), el cual es un candidato a λ-Calculus para computación cuántica, y también probamos la simulación inversa. Ambos cálculos permiten la combinación lineal de términos, sin embargo presentan diferencias a la hora de realizar las reducciones. Por ejemplo en λalg el término

(\lambda x.x\ x)\ (\alpha.t+\beta.u)

reduce a

(\alpha.t+\beta.u)\ (\alpha.t+\beta.u)\ \to\ \alpha.((t)\ \ (\alpha.t+\beta.u))+\beta.((u)\ \ (\alpha.t+\beta.u))

en cambio en λlin, ese mismo término reduce a

\alpha.(\lambda x.x\ x)\ t+\beta.(\lambda x.x\ x)\ u\ \to\  \alpha.(t\ t)+\beta.(u\ u)

Las pruebas de simulación se basan en la observación de que esencialmente λlin es call-by-value mientras que λalg es call-by-name. La simulación en un sentido usa la idea de "thunks" y en el otro es una extensión del continuation passing style.

Este paper es un paso hacia probar la dualidad entre ambos cálculos.