Buenas, no me estaría quedando del todo claro los números de Church y los booleans, específicamente al trabajarlos en coq.
Mi noción sobre los números de Church es que básicamente son una lambda abstracción donde dado un tipo X : Set, valor x : X (representación del cero) y una función f : X->X (función sucesora), nos retorna un valor y : X que corresponde el número en cuestión pero:
- ¿en algún momento se realiza una instanciación para el tipo X, el valor x o la función f ?, o estos simplemente existen para poder realizar las definiciones, pero en realidad no importa cual sea el tipo, el valor x o la función f dado que siempre se comporta igual.
Con respecto a los booleans de Church me sucede algo parecido cuando defino la función If:
Definition If (b th el : Bool) : Bool :=
fun (X : Set) (x : X) (y : X) => (b X (th X x y) (el X x y)).
- A base de la definición del If, no entiendo que valores podrían ser (x) e (y).
Espero se entiendan las dudas, cualquier cosa vuelvo a formular la pregunta, gracias y saludos.