Título: Un cálculo-lambda cronometrado
Director: Pablo Barenbaum
Jurado: Sergio Abriola y Rafael Romero

Resumen:
El cálculo-lambda permite estudiar la noción de función computable desde un
punto de vista matemático, modelando la abstracción y la aplicación de una
función a un argumento. El mecanismo de cómputo por el cual se realiza esta
aplicación se conoce como beta-reducción. En este trabajo extendemos el
cálculo-lambda a una variante «cronometrada», a la que llamamos cálculo-lambda
cronometrado. Extendemos la sintaxis, la semántica y el sistema de tipos para
reflejar el hecho de que la aplicación de una función a un argumento tiene un
costo temporal. Para esto se incorpora un constructor de términos que
representa una demora de una unidad de tiempo, y un operador que modela la
acción de esperar hasta que el resultado de un cómputo esté listo. Modificamos
el mecanismo de cómputo para que cada paso de beta-reducción introduzca una
demora. Demostramos que este cálculo preserva propiedades como la confluencia y
la normalización fuerte del fragmento tipado. Damos un argumento de terminación
débil, bajo ciertas hipótesis de tipabilidad, que exhibe una cota explícita
para la longitud de la reducción a forma normal, basado en las características
del nuevo cálculo, usando la noción de costo definida. Finalmente, demostramos
que hay términos tipables en el cálculo-lambda a los que no se les puede hacer
corresponder un término tipable en el cálculo-lambda cronometrado. Este
resultado se obtiene por medio de un sistema de tipos auxiliar en el que los
juicios de tipado vienen acompañados de restricciones ecuacionales.