Practico 3 Ej 6 y 7

Practico 3 Ej 6 y 7

de Rodrigo Javier Vazquez Machado -
Número de respuestas: 1

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.

En respuesta a Rodrigo Javier Vazquez Machado

Re: Practico 3 Ej 6 y 7

de Carlos Luna -

Hola.

Hay varias formas posibles de definir los números naturales en el Cálculo Lambda. En particular, usando los números de Church. En el EVA hay unas notas de la Universidad de Rice, EEUU, que explican los numerales de Church:

http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf.

Teniendo en cuenta (de la letra del práctico):

Definition N := forall X : Set, X -> (X -> X) -> X. (* podemos ver luego de forall X : Set una codificación de los constructores de los naturales: X y X->X *)
Definition Zero (X : Set) (o : X) (f : X -> X) := o.
Definition Uno  (X : Set) (o : X) (f : X -> X) := f (Zero X o f).

Podemos representar un número natural n esencialmente como una función que toma una función f como parámetro y devuelve n veces f.

El número Dos podría ser:

Definition Dos (X : Set) (o : X) (f : X -> X) := f (Uno X o f). (* Dos debe aplicar f dos veces a su argumento: f f o *)

Luego,

Definition Succ : N -> N :=
  fun (n:N) (X:Set) (o:X) (f:X->X) => f (n X o f).

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.

Donde true (T) sería, por ejemplo:

Definition T (X:Set) (t:X) (f:X) := t. (* el primero *)

Y false (F):

Definition F (X:Set) (t:X) (f:X) := f. (* el segundo *)

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