Practico 3.1

Practico 3.1

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

Entendí como crear los términos en COQ a partir del tipo. Pero tengo problema para escribir el termino fuera de COQ.

Estos dos ejercicios los trato de escribir y me quedan iguales pero no puede ser que el mismo termino corresponda a dos tipos diferentes.

(* λf.λt1.t1 *)

Definition term_teo1 := fun (f: A) (t1: B) => t1.

Check term_teo1. (* A -> B -> B *)

(* λf.λt1.t1 *)

Definition term_3_1_1 := fun (f: A -> A -> A) (t1: A) => t1.

Check term_3_1_1. (* (A -> A -> A) -> A -> A *)


Seguro el term_3_1_1  es el que esta mal la representación λf.λt1.t1.

Me pueden decir donde esta el error?

Saludos

En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: Practico 3.1

de Carlos Luna -
Hola.
El término ( λf.λt1.t1 ) no está tipado, ya que las variables f y t1 no tienen tipo. Al poner los tipos los términos son diferentes en un cálculo tipado.
El término term_3_1_1 está bien para el práctico. Notar que el siguiente término también tiene el mismo tipo: fun (f: A -> A -> A) (t1: A) => f t1 t1. (* (A -> A -> A) -> A -> A *)
Focalizate en el cálculo lambda tipado en el marco de Coq.
Saludos, Carlos
En respuesta a Carlos Luna

Re: Practico 3.1

de Alejandro Sebastian Flocken Rodriguez -
Hola Carlos, si bien me dijiste que me focalice en el marco de Coq sino obtengo la representación del correctamente fuera de Coq no puedo saber si están en β forma normal ya que preciso aplicar reducciones hasta llegar a un termino sin reducciones.
Por ejemplo:

(* λf1.λf2.λt1.λt2.(f2 (f1 t1)) *)
Definition term_3_1_2 := fun (f1: A -> B) (f2: B -> C) (t1: A) (t2: B) => f2 (f1 t1).
Check term_3_1_2. (* (A -> B) -> (B -> C) -> A -> B -> C *)

No se si lo represente bien ya que no se como aplicar las reducciones.
Me podes decir como se prueba que esta en β forma normal?

Saludos
En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: Practico 3.1

de Carlos Luna -

Hola.

Esta bien.

Se encuentra en forma normal si no es posible realizar reducciones (ver el teórico). 

Seguí con los ejercicios de la entrega ahora.

Saludos, Carlos