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
|
1 |
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.
|
1 2 |
uno :: Nat uno f x = f x |
De manera similar, dos debe aplicar f dos veces a su argumento.
|
1 2 |
dos :: Nat dos f x = f (f x) |
Definir cero equivale por tanto a devolver el argumento sin modificar.
|
1 2 |
cero :: Nat cero f x = x |
Definir las funciones
|
1 2 3 4 5 6 7 8 9 |
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,
|
1 2 3 4 |
nat2Int cero == 0 nat2Int uno == 1 nat2Int dos == 2 nat2Int tres == 3 |
- (succ n) es el sucesor del número n. Por ejemplo,
|
1 2 |
nat2Int (succ dos) == 3 nat2Int (succ tres) == 4 |
- (suma n m) es la suma de n y m. Por ejemplo,
|
1 2 |
nat2Int (suma dos tres) == 5 nat2Int (suma dos (succ tres)) == 6 |
- (mult n m) es el producto de n y m. Por ejemplo,
|
1 2 |
nat2Int (mult dos tres) == 6 nat2Int (mult dos (succ tres)) == 8 |
- (exp n m) es la potencia m-ésima de n. Por ejemplo,
|
1 2 3 4 |
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:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
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
|
1 2 |
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TemplateHaskell #-} |
Nota 2: Este ejercicio ha sido propuesto por Ángel Ruiz Campos.
Soluciones
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 |
{-# 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 |