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.
Miguel Pagano, 2019-10-30: “Modelos para sintacticalidades”
- Martín Moroni, 2019-10-09: “Problemas de clasificación y reducciones Borel”
- Facundo Bustos, 2019-11-06: “Introducción a Planning Clásico y su Complejidad”