Miguel Pagano, 2019-10-30: “Modelos para sintacticalidades”

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.

Leave a Reply

Your email address will not be published. Required fields are marked *