Defensa Tesis Licenciatura Lucio Santi

El cálculo lambda permite representar cualquier estructura de datos así como cualquier función computable. No obstante esto, los lenguajes de programación y los asistentes de prueba modernos extienden el lenguaje básico con construcciones primitivas para representar estas estructuras con el fin de evitar la inadecuación de una codificación puramente funcional, en general de difícil utilización y eventualmente costosa en términos de recursos. Una de estas extensiones es el mecanismo de filtrado de valores (pattern matching, o coincidencia de patrones), problema al que se está dedicando mucha atención en la programación funcional u orientada a objetos. Es por eso que surgieron variantes del cálculo lambda que incorporan el manejo de patrones. Un patrón es esencialmente una especificación sintáctica de contextos en los cuales una función puede ser aplicable o una expresión puede ser evaluada. Esto facilita las definiciones por casos, hoy una práctica corriente en la programación declarativa.

Nuestro trabajo estudia relaciones entre distintos cálculos con patrones a través de la definición de traducciones entre ellos a nivel sintáctico. Presentamos la traducción de un gran fragmento del cálculo lambda con patrones múltiples (lambda-C) al cálculo lambda con constructores (lambda-Bc). Esto tiene como fin la posibilidad de compilación de un lenguaje de características y operaciones complejas que están "internalizadas", como el primero, en un lenguaje con un sistema de patrones minimales dados por el análisis por casos sobre constantes básicas, como el segundo, que incluye a cambio un conjunto de reglas de propagación de este constructor de análisis por casos.

Tenemos también interés en codificar con combinadores ciertos cálculos con patrones. Para esto, presentamos una formulación de un cálculo de combinadores para lambda-Bc. Si bien los combinadores S y K clásicos de la lógica combinatoria son funcionalmente completos (en el sentido de que permiten expresar todos los términos del cálculo lambda), proponemos una extensión de esta lógica a través de otros combinadores posibles para la propagación del constructor del análisis de casos, con el fin de obtener un sistema funcionalmente completo y minimal de combinadores para lambda-Bc. Así, se provee un mecanismo de implementación del pattern matching del mismo modo que la lógica combinatoria clásica provee una implementación del cálculo lambda. Para este nuevo sistema probamos su capacidad de abstracción y la confluencia (la cual garantiza la unicidad de formas normales).