Números de Church
Los números naturales pueden definirse de forma alternativa empleando los números de Church. Podemos representar un número natural n como una función que toma una función f como parámetro y devuelve n veces f.
Definimos por tanto los números naturales como
Type Nat = forall a. (a -> a) -> a -> a
De esta forma, para representar el número uno, repetir una vez una función es lo mismo que solamente aplicarla.
uno :: Nat uno f x = f x
De manera similar, dos debe aplicar f dos veces a su argumento.
dos :: Nat dos f x = f (f x)
Definir cero equivale por tanto a devolver el argumento sin modificar.
cero :: Nat cero f x = x
Definir las funciones
cero :: Nat uno :: Nat dos :: Nat tres :: Nat nat2Int :: Nat -> Int succ :: Nat -> Nat suma :: Nat -> Nat -> Nat mult :: Nat -> Nat -> Nat exp :: Nat -> Nat -> Nat
tales que
- cero, uno y dos son definiciones alternativas a las ya dadas y tres es el número natural 3 con esta representación.
- (nat2Int n) es el número entero correspondiente al número natuaral n. Por ejemplo,
nat2Int cero == 0 nat2Int uno == 1 nat2Int dos == 2 nat2Int tres == 3
- (succ n) es el sucesor del número n. Por ejemplo,
nat2Int (succ dos) == 3 nat2Int (succ tres) == 4
- (suma n m) es la suma de n y m. Por ejemplo,
nat2Int (suma dos tres) == 5 nat2Int (suma dos (succ tres)) == 6
- (mult n m) es el producto de n y m. Por ejemplo,
nat2Int (mult dos tres) == 6 nat2Int (mult dos (succ tres)) == 8
- (exp n m) es la potencia m-ésima de n. Por ejemplo,
nat2Int (exp dos tres) == 8 nat2Int (exp tres dos) == 9 nat2Int (exp tres cero) == 1 nat2Int (exp cero tres) == 0
Comprobar con QuickCheck las siguientes propiedades. Para ello importar la librería Test.QuickCheck.Function y seguir el siguiente ejemplo:
prop_Succ1 :: Fun Int Int -> Int -> Bool prop_Succ1 (Fun _ f) x = succ cero f x == uno f x succ uno = dos succ dos = tres suma cero uno = uno suma dos tres = suma tres dos suma (suma dos dos) tres = suma uno (suma tres tres) mult uno uno = uno mult cero (suma tres tres) = cero mult dos tres = suma tres tres exp dos dos = suma dos dos exp tres dos = suma (mult dos (mult dos dos)) uno exp tres cero = uno
Nota 1: Añadir al inicio del archivo del ejercicio los pragmas
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TemplateHaskell #-}
Nota 2: Este ejercicio ha sido propuesto por Ángel Ruiz Campos.
Soluciones
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TemplateHaskell #-} import Prelude hiding (succ, exp) import Test.QuickCheck import Test.QuickCheck.Function type Nat = forall a. (a -> a) -> a -> a -- 1ª definición de cero -- ===================== cero1 :: Nat cero1 f x = x -- 2ª definición de cero -- ===================== cero2 :: Nat cero2 = (\ _ x -> x) -- 3ª definición de cero -- ===================== cero3 :: Nat cero3 _ x = x -- 4ª definición de cero -- ===================== cero4 :: Nat cero4 _ = id -- 5ª definición de cero -- ===================== cero5 :: Nat cero5 = seq -- 1ª definición de uno -- ==================== uno1 :: Nat uno1 f x = f x -- 2ª definición de uno -- ==================== uno2 :: Nat uno2 = (\ f x -> f x) -- 3ª definición de uno -- ==================== uno3 :: Nat uno3 = ($) -- 4ª definición de uno -- ==================== uno4 :: Nat uno4 = id -- 1ª definición de dos -- ==================== dos1 :: Nat dos1 f x = f (f x) -- 2ª definición de dos -- ==================== dos2 :: Nat dos2 f = f . f -- 1ª definición de tres -- ===================== tres1 :: Nat tres1 f x = f (dos f x) -- 2ª definición de tres -- ===================== tres2 :: Nat tres2 f = f . (dos f) -- 3ª definición de tres -- ===================== tres3 :: Nat tres3 f = f . f . f -- Definición de nat2Int -- ===================== nat2Int :: Nat -> Int nat2Int x = x (+1) 0 -- 1ª definición de succ -- ===================== succ1 :: Nat -> Nat succ1 n f x = f (n f x) -- 2ª definición de succ -- ===================== succ2 :: Nat -> Nat succ2 n f = f . n f -- 1ª definición de suma -- ===================== suma1 :: Nat -> Nat -> Nat suma1 n m f x = n f (m f x) -- 2ª definición de suma -- ===================== suma2 :: Nat -> Nat -> Nat suma2 n m f = n f . m f -- 1ª definición de mult -- ===================== mult1 :: Nat -> Nat -> Nat mult1 n m f x = n (m f) x -- 2ª definición de mult -- ===================== mult2 :: Nat -> Nat -> Nat mult2 n m f = n (m f) -- 3ª definición de mult -- ===================== mult3 :: Nat -> Nat -> Nat mult3 n m = n . m -- 1ª definición de exp -- ==================== exp1 :: Nat -> Nat -> Nat exp1 n m f x = m (\y -> (\z -> (n y z))) f x -- 2ª definición de exp -- ==================== exp2 :: Nat -> Nat -> Nat exp2 n m f = m n f -- 3ª definición de exp -- ==================== exp3 :: Nat -> Nat -> Nat exp3 n m = m n -- Comprobaciones -- ============== -- Para las comprobaciones emplearemos las siguientes funciones: cero, uno, dos, tres :: Nat cero = cero5 uno = uno4 dos = dos2 tres = tres3 succ = succ2 suma, mult, exp :: Nat -> Nat -> Nat suma = suma2 mult = mult3 exp = exp3 prop_Succ1, prop_Succ2, prop_Succ3 :: Fun Int Int -> Int -> Bool prop_Succ1 (Fun _ f) x = succ cero f x == uno f x prop_Succ2 (Fun _ f) x = succ uno f x == dos f x prop_Succ3 (Fun _ f) x = succ dos f x == tres f x prop_Suma1, prop_Suma2, prop_Suma3 :: Fun Int Int -> Int -> Bool prop_Suma1 (Fun _ f) x = suma cero uno f x == uno f x prop_Suma2 (Fun _ f) x = suma dos tres f x == suma tres dos f x prop_Suma3 (Fun _ f) x = suma (suma dos dos) tres f x == suma uno (suma tres tres) f x prop_Mult1, prop_Mult2, prop_Mult3 :: Fun Int Int -> Int -> Bool prop_Mult1 (Fun _ f) x = mult uno uno f x == uno f x prop_Mult2 (Fun _ f) x = mult cero (suma tres tres) f x == cero f x prop_Mult3 (Fun _ f) x = mult dos tres f x == suma tres tres f x prop_Exp1, prop_Exp2, prop_Exp3 :: Fun Int Int -> Int -> Bool prop_Exp1 (Fun _ f) x = exp dos dos f x == suma dos dos f x prop_Exp2 (Fun _ f) x = exp tres dos f x == suma (mult dos (mult dos dos)) uno f x prop_Exp3 (Fun _ f) x = exp tres cero f x == uno f x return [] runTests = $quickCheckAll -- La comprobación es -- λ> runTests -- === prop_Succ1 === -- +++ OK, passed 100 tests. -- -- === prop_Suma1 === -- +++ OK, passed 100 tests. -- -- === prop_Mult1 === -- +++ OK, passed 100 tests. -- -- === prop_Exp1 === -- +++ OK, passed 100 tests. -- -- === prop_Succ2 === -- +++ OK, passed 100 tests. -- -- === prop_Succ3 === -- +++ OK, passed 100 tests. -- -- === prop_Suma2 === -- +++ OK, passed 100 tests. -- -- === prop_Suma3 === -- +++ OK, passed 100 tests. -- -- === prop_Mult2 === -- +++ OK, passed 100 tests. -- -- === prop_Mult3 === -- +++ OK, passed 100 tests. -- -- === prop_Exp2 === -- +++ OK, passed 100 tests. -- -- === prop_Exp3 === -- +++ OK, passed 100 tests. -- -- True