Buenas,
estamos teniendo dificultad para entender cómo definir tipos y/o funciones en ejercicios 6 y 7.
En particular sobre las definiciones del ejercicio 6, no estamos entendiendo la de Uno, ¿cómo deberíamos interpretarla?
También para los ejercicios 6.2, al querer definir la función Succ, y en el 7.1 al definir tipo Bool. No estamos seguros de estar razonándolos correctamente...
Agradecemos cualquier ayuda.
Saludos
Hola.
para entender los numerales de Church, recomiendo primero leer:
http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf.
Si las dudas siguen, vuelvan a preguntar y aclaro lo que haga falta.
Saludos, Carlos
A mi no me queda claro como definir Bool. Entendi como definir true y false.
Lo que se me ocurrio fue asi pero no esta bien.
Bool:= true:Bool | false: Bool.
Pensarlo como una funcion no se me ocurre.
Tengo exactamente la misma duda..
Creo que simplemente hay que definir el tipo, y no sería una función.
A mí me anduvo bien, hasta que me di cuenta que el IF es de tipo Bool->Bool->Bool->Bool, lo que me hace pensar en una cierta recursividad del tipo, pero no me parece que se pueda hacer eso porque no puedo definir Bool con Bool....
Podría ser algo así:
Definition Bool := forall X:Set, X -> X -> X.
Donde true (t) sería, por ejemplo:
Definition t (X:Set) (t:X) (f:X) := t.
Saludos, Carlos
Primero que nada, gracias.
Segundo, eso más o menos queda claro en el Pdf, pero lo que no me queda claro es el tema de los tipos. En el pdf se menciona la función test:
test=λb . λc . λa . b c a
El problema es que mapeando el if a la función test que se menciona en el PDF los tipos no coinciden.
The term "then'" has type "Bool" while it is expected to have type "Set".
No me queda del todo claro cómo es la idea de los booleanos. Teniendo la función if definida como Bool->Bool->Bool->Bool termina quedando:
(A->A->A)->(B->B->B)->(C->C->C)->(D->D->D).
Y no veo cómo poder realizar las instanciaciones.
Hola.
Los booleanos son definidos (están codificados) según los numerales de Church de la siguiente forma:
Definition Bool := forall X:Set, X->X->X.
Definition t (X:Set) (a:X) (b:X) := a.
Definition f (X:Set) (a:X) (b:X) := b.
Notar que este tipo es mucho más simple que el de los naturales, ya que básicamente consta de dos valores.
El If, según esta definición (y de acuerdo a los tipos) sería:
Definition If (o n m:Bool): Bool :=
fun (X:Set) (a:X) (b:X)=> o X (n X a b) (m X a b).
Saludos, Carlos
Analizando el código que pusiste ahora lo entendí. Realmente no se me había ocurrido estructurarlo así. Lo del t y el f me había quedado claro, pero no estaba dando en la tecla con el if.
Gracias !!
Gracias, entendimos un poco mejor.
Con respecto al tipo Bool nosotros lo pensamos más "genérico" como está N en ejercicio 6. En el artículo definen true/false, los cuales son Bool, en base a eso pudimos deducir el tipo.
