Practico 3.2

Practico 3.2

de Alejandro Sebastian Flocken Rodriguez -
Número de respuestas: 3

Hola, no estoy seguro de si lo estoy haciendo bien.

Se que pidieron que no mandemos código pero preciso que me verifiquen si están bien estos 2 ejemplos para saber si lo estoy entendiendo bien. COQ me dice que están bien, pero el tema es que no estoy seguro si los estoy escribiendo bien en COQ.

Section Ejercicio2.

Variable A B C: Set.

 (*   [x:?][y:?][z:?]((x y)z)   *) 

Definition term_3_2_1 := fun (x: A -> B -> C) (y: A) (z: B) => x y z.

Check term_3_2_1. (* (A -> B -> C) -> A -> B -> C *)

(*   [x:?][y:?][z:?](x (y z))   *)

Definition term_3_2_2 := fun (x: B -> C) (y: A -> B) (z: A) => x (y z).

Check term_3_2_2. (* (B -> C) -> (A -> B) -> A -> C *)

End Ejercicio2.

Y con este 

[z:?]([x:?][y:?](x y) z) me perdí, no se cual es la diferencia con el primero al cambiar el paréntesis curvo.

Que notación es esta? Yo pensaba que era lo mismo que λz.λx.λy((x y) z) pero con los paréntesis curvos me descoloco.


Saludos

En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: Practico 3.2

de Carlos Luna -

Hola.

Los primeros están bien.

Los paréntesis curvos establecen alcance. En este caso el término: 

fun (z: A) => fun (x: B -> A -> C) (y: B) => (x y) z.

tiene tipo: A -> (B -> A -> C) -> B -> C. (indistintamente: A -> ((B -> A -> C) -> B -> C))

Saludos, Carlos 

En respuesta a Carlos Luna

Re: Practico 3.2

de Alejandro Sebastian Flocken Rodriguez -
Buenas Carlos, estoy con duda con el ultimo del ejercicio 3.2
Lo resolví de dos maneras y no se si esta bien una, las dos o ninguna.

(* ([x:?]x[y:?]y) *)
Definition term_3_2_4 := fun (f: A -> B)(x: A)(y: B) => (f x).
Check term_3_2_4. (* (A -> B) -> A -> B -> B *)

(* ([x:?]x[y:?]y) *)
Definition term_3_2_4_b := fun (f: A -> A -> B)(x: A)(y: B) => (f x) x.
Check term_3_2_4_b. (* (A -> A -> B) -> A -> B -> B *)

Cual de los dos esta bien? Como verifico que esta bien lo que hice?

Saludos
En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: Practico 3.2

de Carlos Luna -

Hola.

Es es una función aplicada a una función:

Definition term4 := fun (f: (A -> B) -> C) (g: A -> B) => f g.

Check term4. (* ((A -> B) -> C) -> (A -> B) -> C *)

Saludos, Carlos