Estaba mirando la grabación de la clase y me surgió la siguiente duda:
El profesor dice que para resolver el tipo de λx.λy.x aplicamos la regla de la abstracción y luego la regla de la variable. No nombraron ninguna regla de la variable. Las reglas son Abstracción, Aplicación y Constante.
Me podrían aclarar como se calcula el tipo?
Saludos
Hola Alejandro,
Efectivamente hay 3 reglas, pero la tercera no es la de Constante es la de Contexto (ctxt la nombramos), y es la que te permite probar que una variable x tiene un tipo Alpha si x:Alpha pertenece al contexto Gamma.
Entonces si, para probar [] |- \x.\y.x : Alpha -> Beta -> Alpha aplicamos 2 veces la regla de abstracción, quedando por probar que [x:Alpha,y:Beta] |- x:Alpha, y en ese paso aplicamos la regla del contexto (o de la variable también es llamada).
Saludos
Hola Gustavo,
Perdón la demora en responder, eso que me decís lo entendí ok, lo que no entiendo es como es el razonamiento para deducir que lo que quiero probar es que es de tipo Alpha -> Beta -> Alpha.
O sea la prueba la entiendo, lo que no entiendo es como saber cual es el tipo que tengo que probar. Si bien en este caso es medio trivial no se como razonarlo para otro ejercicio.
Me podrás explicar como es el razonamiento?
Perdón la demora en responder, eso que me decís lo entendí ok, lo que no entiendo es como es el razonamiento para deducir que lo que quiero probar es que es de tipo Alpha -> Beta -> Alpha.
O sea la prueba la entiendo, lo que no entiendo es como saber cual es el tipo que tengo que probar. Si bien en este caso es medio trivial no se como razonarlo para otro ejercicio.
Me podrás explicar como es el razonamiento?