El ejercicio del teórico:
(a->b->c)->b->a->c
Es el tipo del termino es (λaλbλc)λbλaλx\c ?
Saludos
En respuesta a Alejandro Sebastian Flocken Rodriguez
Re: duda ejercicio visto en teórico
de Gustavo Betarte -
Hola de nuevo.
No termino de entender muy bien el termino que escribiste, qué denota \c? Además si mirás con atención ese termino contiene 6 (o 7?) abstracciones, lo que se corresponde con una función de 6 (o 7?) parámetros.
El tipo (a->b->c)->b->a->c es el de un función que toma 3 argumentos: una funcion de tipo a->b->c, un elemento de tipo b y otro de tipo a para retonar un elemento de tipo c. Un termino lambda con ese tipo es el siguiente: \f.\x.\y. ((f y) x)
Para verificarlo, te recomiendo probar que [] |- \f.\x.\y. ((f y) x) : (a->b->c)->b->a->c
Saludos
El tipo (a->b->c)->b->a->c es el de un función que toma 3 argumentos: una funcion de tipo a->b->c, un elemento de tipo b y otro de tipo a para retonar un elemento de tipo c. Un termino lambda con ese tipo es el siguiente: \f.\x.\y. ((f y) x)
Para verificarlo, te recomiendo probar que [] |- \f.\x.\y. ((f y) x) : (a->b->c)->b->a->c
Saludos
En respuesta a Alejandro Sebastian Flocken Rodriguez
Re: duda ejercicio visto en teórico
de Carlos Luna -
Hola.
No, un término de este tipo (omitendo los tipos en el término) sería:
λf.λt1.λt2. ((f t2) t1)
En Coq:
Variable A B C: Set.
Definition term := fun (f: A -> B -> C) (t1: B) (t2: A) => f t2 t1.
Check term. (* (A -> B -> C) -> B -> A -> C *)
Saludos, Carlos