En un seminario anterior, Francisco Trucco presentó el isomorfismo de Curry-Howard y para ello introdujo el cálculo lambda. La noción de cómputo en el cálculo lambda es sintáctica y consiste en reducir paso a paso expresiones. En este seminario, presentaré cómo podemos encontrar la forma normal de una expresión a través de un modelo (en el sentido algebraico); para ello, además de una función de evaluación tendremos una función (parcial) del modelo a términos. El trabajo será mostrar que la composición de esas dos funciones nos devuelve la forma normal del argumento.
(source)