Ir al contenido principal

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