Teoría de mejoras con efectos

Abstract

Optimizar programas es difícil. Al aplicar una transformación a un programa uno debe mostrar que se preserva la semántica del programa, y además, se tiene que asegurar que la transformación es realmente una optimización. El estudio de transformaciones de programas que preserven la semántica de los programas es un área de mucha investigación. Seguimos una línea de trabajo que comienza con la equivalencia observacional de Morris, continúa con la relación de bisimulación aplicativa de Abramsky y el método de Howe, concluyendo finalmente con una línea más reciente donde se agregan efectos algebraicos a la relación de bisimulación aplicativa de Dal Lago, Gavazzo y Levy. Asegurar que una transformación es realmente una optimización, que realmente se mejora el programa, es un camino menos explorado con la teoría de mejoras de Sands como el ejemplo más prominente. En esta tesis, conectamos estos dos caminos obteniendo una teoría de mejoras abstracta basada en la relación de bisimulación aplicativa con efectos extendiendo la relación de mejoras a lenguajes con efectos.