Operational aspects of full reduction in lambda calculi

• Autores: Alvaro Garcia Perez
• Directores de la Tesis: Pablo Nogueira Iglesias (codir. tes.) , Juan José Moreno Navarro (codir. tes.)
• Lectura: En la Universidad Politécnica de Madrid ( España ) en 2014
• Idioma: español
• Tribunal Calificador de la Tesis: Santiago Escobar Román (presid.) , Julio Mariño Carballo (secret.) , Malgorzata Biernacka (voc.) , Pierre-Yves Strub (voc.) , Jan Midtgaard (voc.)
• Enlaces
  • Tesis en acceso abierto en: Archivo Digital UPM
• Resumen

  • Esta tesis estudia la reducción plena (`full reduction' en inglés) en distintos cálculos lambda. En esencia, la reducción plena consiste en evaluar los cuerpos de las funciones en los lenguajes de programación funcional con ligaduras. Se toma el cálculo lambda clásico (i.e., puro y sin tipos) como el sistema formal que modela el paradigma de programación funcional. La reducción plena es una técnica fundamental cuando se considera a los programas como datos, por ejemplo para la optimización de programas mediante evaluación parcial, o cuando algún atributo del programa se representa a su vez por un programa, como el tipo en los demostradores automáticos de teoremas actuales.

    Muchas semánticas operacionales que realizan reducción plena tienen naturaleza híbrida. Se introduce formalmente la noción de naturaleza híbrida, que constituye el hilo conductor de todo el trabajo. En el cálculo lambda la naturaleza híbrida se manifiesta como una `distinción de fase' en el tratamiento de las abstracciones, ya sean consideradas desde fuera o desde dentro de si mismas. Esta distinción de fase conlleva una estructura en capas en la que una semántica híbrida depende de una o más semánticas subsidiarias.

    Desde el punto de vista de los lenguajes de programación, la tesis muestra como derivar, mediante técnicas de transformación de programas, implementaciones de semánticas operacionales que reducen plenamente a partir de sus especificaciones. Las técnicas de transformación de programas consisten en transformaciones sintácticas que preservan la equivalencia semántica de los programas. Se ajustan las técnicas de transformación de programas existentes para trabajar con implementaciones de semánticas híbridas. Además, se muestra el impacto que tiene la reducción plena en las implementaciones que utilizan entornos. Los entornos son un ingrediente fundamental en las implementaciones realistas de una máquina abstracta.

    Desde el punto de vista de los sistemas formales, la tesis desvela una teoría novedosa para el cálculo lambda con paso por valor (`call-by-value lambda calculus' en inglés) que es consistente con la reducción plena. Dicha teoría induce una noción de equivalencia observacional que distingue más puntos que las teorías existentes para dicho cálculo. Esta contribución ayuda a establecer una `teoría estándar' en el cálculo lambda con paso por valor que es análoga a la `teoría estándar' del cálculo lambda clásico propugnada por Barendregt. Se presentan resultados de teoría de la demostración, y se sugiere como abordar el estudio de teoría de modelos.