Consultas de Práctico

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