El título de este post es el título de un paper (bueno, su traducción) que acabamos de terminar de escribir y enviar a una conferencia con Pablo E. Martínez López (o Fidel, como lo conoce todo el mundo).
En este paper proponemos una implementación de λ⁺ (un cálculo del que ya he hablado varias veces en este blog, que desarrollamos con Gilles Dowek). λ⁺ tiene la característica de que toma los isomorfismos de tipos y los considera igualdades. Por ejemplo, una función que toma dos argumentos es igual a una función que toma un par, y una función que retorna dos argumentos es igual a dos funciones, porque A⇒B⇒C es isomorfo a (A∧B)⇒C y A⇒(B∧C) es isomorfo a (A⇒B)∧(A⇒C).
El sistema de reescritura de λ⁺ utiliza reescritura modulo una relación de equivalencia, lo cual hace que implementar un lenguaje con esas características no sea trivial. Y eso es exactamente lo que proponemos en este nuevo paper. Además, extendemos λ⁺ con números naturales y recursión general, y, usando un resultado clásico para dividir recursiones mutuas (teorema de Bekić), junto a las características de λ⁺, logramos una forma interesante de transformación de programas: podemos, por ejemplo, definir una función recursiva que calcula dos valores y luego proyectar el valor que nos interesa... sólo que el programa va a hacer la proyección antes de recibir sus argumentos, proyectando la función y transformándola en una función que sólo calcula el valor que nos interesa.
Otra propiedad interesante es que la curryficación, llevada al extremo, junto a la asociatividad y conmutatividad, hacen que tengamos una forma de aplicación parcial muy potente: una función que recibe más de un argumento, puede recibir cualquiera de ellos en cualquier orden.
Bueno, les dejo el paper tal como lo acabamos de enviar (aún debe ser revisado por los reviewers):
0 comments:
Publicar un comentario