Biortogonalidad para Corrección de Compiladores y Adecuación Computacional
Resumen
Definir un lenguaje de programación implica definir su sintaxis (abstracta y alguna concreta), junto con una interpretación de las expresiones (en el caso de lenguajes declarativos) o sentencias (para lenguajes imperativos). Hoy en día la mayor parte de los lenguajes de programación definen esa interpretación o bien de manera informal, con prosa en lenguaje natural, o bien de forma implícita mediante un compilador o intérprete del lenguaje. La carencia de una definición formal de la semántica dificulta en gran medida el uso de métodos formales para razonar acerca del lenguaje, por ejemplo para probar que una determinada expresión computa una cierta función matemática. Los dos enfoques comunes para definir formalmente la semántica de un lenguaje de programación son la semántica denotacional iniciada por Dana Scott y Christopher Strachey, y la semántica operacional popularizada por Gordon Plotkin. La semántica denotacional permite justificar más fácilmente que una cierta expresión es la implementación de una función matemática mientras que la semántica operacional resulta más apropiada para definir máquinas abstractas.
La programación es realizada por lo general en un lenguaje de alto nivel el cual es conveniente ya que dispone de abstracciones que facilitan el razonamiento, luego un compilador traduce ese programa fuente a un lenguaje de bajo nivel (por ejemplo, de una máquina abstracta) y se asume que el programa objeto resultante se comporta como el programa original. La única manera de tener certeza es probando la corrección del compilador; es decir, que la semántica del programa fuente es preservada por el proceso de compilación.
Los primeros esfuerzos en el área de certificación de compiladores comienzan en 1967 con la corrección de un compilador para expresiones aritméticas de John McCarthy y James Painter, desde entonces el área a estado en constante crecimiento, en particular en el año 2009 se realiza probablemente uno de los trabajos más importantes en el área al certificar un compilador para un fragmento del lenguaje C a un lenguaje ensamblador, desarrolado por el proyecto CompCert. Respecto a la corrección de compiladores de lenguajes funcionales, en 2007 Adam Chlipala presenta la certificación de un compilador del cálculo lambda simplemente tipado hacia código ensamblador, recientemente en 2016 Yong Kiam Tan et al. desarrollaron un compilador certificado para el lenguaje CakeML con respecto a diferentes arquitecturas. La corrección de compiladores para lenguajes con evaluación lazy parece un área menos explorada; los trabajos más relacionados involucran la prueba de adecuación entre una semántica denotacional y operacional desarrollado en 1993 por John Launchbury y su reciente mecanización llevada a cabo por Joachim Breitner en Isabelle.
Durante el doctorado hemos estudiado en profundidad los métodos de biortogonalidad y step-indexing para probar tanto adecuación computacional como corrección de compiladores. Un primer aporte es la prueba de corrección de una semántica denotacional con respecto a una operacional para un lenguaje lazy definido por John Launchbury; la prueba original propuesta contiene ciertas irregularidades que corregimos dando nuevas definiciones que nos permiten dar una prueba exhaustiva. Otro aporte es la prueba de adecuación computacional de una semántica operacional con respecto a una denotacional para un lenguaje funcional con un sistema de tipos simple extendido con subtipado y estrategia de evaluación call-by-value. Para este mismo lenguaje probamos la coincidencia entre una semántica denotacional extrínseca y una intrínseca. Este aporte incluye la mecanización completa en Coq de todos los resultados; hasta donde sabemos realizamos la primera mecanización del teorema de bracketing enunciado por John Reynolds. Finalmente damos una prueba de corrección de un compilador para un lenguaje lazy con recursión generando código para una máquina abstracta, este aporte extiende significativamente un trabajo previo desarrollado por Leonardo Rodríguez. Incluimos también la mecanización completa en Coq.
Mecanización
La mecanización completa realizada Coq versión 8.8.1 (Agosto 2018) esta disponible para descargar, al igual que la documentación generada con coqdoc. Además se puede descargar una versión preliminar de la tesis.