{"id":4111,"date":"2018-05-28T06:00:25","date_gmt":"2018-05-28T04:00:25","guid":{"rendered":"http:\/\/www.glc.us.es\/~jalonso\/exercitium\/?p=4111"},"modified":"2018-06-05T16:34:35","modified_gmt":"2018-06-05T14:34:35","slug":"numeros-de-church","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-de-church\/","title":{"rendered":"N\u00fameros de Church"},"content":{"rendered":"<p>Los n\u00fameros naturales pueden definirse de forma alternativa empleando los n\u00fameros de Church. Podemos representar un n\u00famero natural n como una funci\u00f3n que toma una funci\u00f3n f como par\u00e1metro y devuelve n veces f.<\/p>\n<p>Definimos por tanto los n\u00fameros naturales como<\/p>\n<pre lang=\"text\">\n   Type Nat = forall a. (a -> a) -> a -> a\n<\/pre>\n<p>De esta forma, para representar el n\u00famero uno, repetir una vez una funci\u00f3n es lo mismo que solamente aplicarla.<\/p>\n<pre lang=\"text\">\n   uno :: Nat\n   uno f x = f x\n<\/pre>\n<p>De manera similar, dos debe aplicar f dos veces a su argumento.<\/p>\n<pre lang=\"text\">\n   dos :: Nat\n   dos f x = f (f x)\n<\/pre>\n<p>Definir cero equivale por tanto a devolver el argumento sin modificar.<\/p>\n<pre lang=\"text\">\n   cero :: Nat\n   cero f x = x\n<\/pre>\n<p>Definir las funciones<\/p>\n<pre lang=\"text\">\n   cero    :: Nat\n   uno     :: Nat\n   dos     :: Nat\n   tres    :: Nat\n   nat2Int :: Nat -> Int\n   succ    :: Nat -> Nat\n   suma    :: Nat -> Nat -> Nat\n   mult    :: Nat -> Nat -> Nat\n   exp     :: Nat -> Nat -> Nat\n<\/pre>\n<p>tales que<\/p>\n<ul>\n<li>cero, uno y dos son definiciones alternativas a las ya dadas y tres es el n\u00famero natural 3 con esta representaci\u00f3n.<\/li>\n<li>(nat2Int n) es el n\u00famero entero correspondiente al n\u00famero natuaral n. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n    nat2Int cero == 0\n    nat2Int uno  == 1\n    nat2Int dos  == 2\n    nat2Int tres == 3\n<\/pre>\n<ul>\n<li>(succ n) es el sucesor del n\u00famero n. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n     nat2Int (succ dos)   ==  3\n     nat2Int (succ tres)  ==  4\n<\/pre>\n<ul>\n<li>(suma n m) es la suma de n y m. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n     nat2Int (suma dos tres)         ==  5\n     nat2Int (suma dos (succ tres))  ==  6\n<\/pre>\n<ul>\n<li>(mult n m) es el producto de n y m. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n     nat2Int (mult dos tres)         ==  6\n     nat2Int (mult dos (succ tres))  ==  8\n<\/pre>\n<ul>\n<li>(exp n m) es la potencia m-\u00e9sima de n. Por ejemplo,<\/li>\n<\/ul>\n<pre lang=\"text\">\n     nat2Int (exp dos tres)   ==  8\n     nat2Int (exp tres dos)   ==  9\n     nat2Int (exp tres cero)  ==  1\n     nat2Int (exp cero tres)  ==  0\n<\/pre>\n<p>Comprobar con QuickCheck las siguientes propiedades. Para ello importar la librer\u00eda Test.QuickCheck.Function y seguir el siguiente ejemplo:<\/p>\n<pre lang=\"text\">\n   prop_Succ1 :: Fun Int Int -> Int -> Bool\n   prop_Succ1 (Fun _ f) x = succ cero f x == uno f x\n\n   succ uno                   = dos\n   succ dos                   = tres\n   suma cero uno              = uno\n   suma dos tres              = suma tres dos\n   suma (suma dos dos) tres   = suma uno (suma tres tres)\n   mult uno uno               = uno\n   mult cero (suma tres tres) = cero\n   mult dos tres              = suma tres tres\n   exp dos dos                = suma dos dos\n   exp tres dos               = suma (mult dos (mult dos dos)) uno\n   exp tres cero              = uno\n<\/pre>\n<p><strong>Nota 1<\/strong>: A\u00f1adir al inicio del archivo del ejercicio los pragmas<\/p>\n<pre lang=\"text\">\n   {-# LANGUAGE RankNTypes #-}\n   {-# LANGUAGE TemplateHaskell #-}\n<\/pre>\n<p><strong>Nota 2<\/strong>: Este ejercicio ha sido propuesto por \u00c1ngel Ruiz Campos.<\/p>\n<h4>Soluciones<\/h4>\n<pre lang=\"haskell\">\n{-# LANGUAGE RankNTypes #-}\n{-# LANGUAGE TemplateHaskell #-}\n\nimport Prelude hiding (succ, exp)\nimport Test.QuickCheck\nimport Test.QuickCheck.Function\n\ntype Nat = forall a. (a -> a) -> a -> a\n\n-- 1\u00aa definici\u00f3n de cero\n-- =====================\n\ncero1 :: Nat\ncero1 f x = x\n\n-- 2\u00aa definici\u00f3n de cero\n-- =====================\n\ncero2 :: Nat\ncero2 = (\\ _ x -> x)\n\n-- 3\u00aa definici\u00f3n de cero\n-- =====================\n\ncero3 :: Nat\ncero3 _ x = x\n\n-- 4\u00aa definici\u00f3n de cero\n-- =====================\n\ncero4 :: Nat\ncero4 _ = id\n\n-- 5\u00aa definici\u00f3n de cero\n-- =====================\n\ncero5 :: Nat\ncero5 = seq\n\n-- 1\u00aa definici\u00f3n de uno\n-- ====================\n\nuno1 :: Nat\nuno1 f x = f x\n\n-- 2\u00aa definici\u00f3n de uno\n-- ====================\n\nuno2 :: Nat\nuno2 = (\\ f x -> f x)\n\n-- 3\u00aa definici\u00f3n de uno\n-- ====================\n\nuno3 :: Nat\nuno3 = ($)\n\n-- 4\u00aa definici\u00f3n de uno\n-- ====================\n\nuno4 :: Nat\nuno4 = id\n\n-- 1\u00aa definici\u00f3n de dos\n-- ====================\n\ndos1 :: Nat\ndos1 f x = f (f x)\n\n-- 2\u00aa definici\u00f3n de dos\n-- ====================\n\ndos2 :: Nat\ndos2 f = f . f\n\n-- 1\u00aa definici\u00f3n de tres\n-- =====================\n\ntres1 :: Nat\ntres1 f x = f (dos f x)\n\n-- 2\u00aa definici\u00f3n de tres\n-- =====================\n\ntres2 :: Nat\ntres2 f = f . (dos f)\n\n-- 3\u00aa definici\u00f3n de tres\n-- =====================\n\ntres3 :: Nat\ntres3 f = f . f . f\n\n-- Definici\u00f3n de nat2Int\n-- =====================\n\nnat2Int :: Nat -> Int\nnat2Int x = x (+1) 0\n\n-- 1\u00aa definici\u00f3n de succ\n-- =====================\n\nsucc1 :: Nat -> Nat\nsucc1 n f x = f (n f x)\n\n-- 2\u00aa definici\u00f3n de succ\n-- =====================\n\nsucc2 :: Nat -> Nat\nsucc2 n f = f . n f\n\n-- 1\u00aa definici\u00f3n de suma\n-- =====================\n\nsuma1 :: Nat -> Nat -> Nat\nsuma1 n m f x = n f (m f x)\n\n-- 2\u00aa definici\u00f3n de suma\n-- =====================\n\nsuma2 :: Nat -> Nat -> Nat\nsuma2 n m f = n f . m f\n\n-- 1\u00aa definici\u00f3n de mult\n-- =====================\n\nmult1 :: Nat -> Nat -> Nat\nmult1 n m f x = n (m f) x\n\n-- 2\u00aa definici\u00f3n de mult\n-- =====================\n\nmult2 :: Nat -> Nat -> Nat\nmult2 n m f = n (m f)\n\n-- 3\u00aa definici\u00f3n de mult\n-- =====================\n\nmult3 :: Nat -> Nat -> Nat\nmult3 n m = n . m\n\n-- 1\u00aa definici\u00f3n de exp\n-- ====================\n\nexp1 :: Nat -> Nat -> Nat\nexp1 n m f x = m (\\y -> (\\z -> (n y z))) f x\n\n-- 2\u00aa definici\u00f3n de exp\n-- ====================\n\nexp2 :: Nat -> Nat -> Nat\nexp2 n m f = m n f\n\n-- 3\u00aa definici\u00f3n de exp\n-- ====================\n\nexp3 :: Nat -> Nat -> Nat\nexp3 n m = m n\n\n-- Comprobaciones\n-- ==============\n\n-- Para las comprobaciones emplearemos las siguientes funciones:\n\ncero, uno, dos, tres :: Nat\ncero = cero5\nuno  = uno4\ndos  = dos2\ntres = tres3\nsucc = succ2\n\nsuma, mult, exp :: Nat -> Nat -> Nat\nsuma = suma2\nmult = mult3\nexp  = exp3\n\nprop_Succ1, prop_Succ2, prop_Succ3 :: Fun Int Int -> Int -> Bool\nprop_Succ1 (Fun _ f) x =\n  succ cero f x == uno  f x\nprop_Succ2 (Fun _ f) x =\n  succ uno  f x == dos  f x\nprop_Succ3 (Fun _ f) x =\n  succ dos  f x == tres f x\n\nprop_Suma1, prop_Suma2, prop_Suma3 :: Fun Int Int -> Int -> Bool\nprop_Suma1 (Fun _ f) x =\n  suma cero uno f x == uno f x\nprop_Suma2 (Fun _ f) x =\n  suma dos tres f x == suma tres dos f x\nprop_Suma3 (Fun _ f) x =\n  suma (suma dos dos) tres f x == suma uno (suma tres tres) f x\n\nprop_Mult1, prop_Mult2, prop_Mult3 :: Fun Int Int -> Int -> Bool\nprop_Mult1 (Fun _ f) x =\n  mult uno uno f x == uno f x\nprop_Mult2 (Fun _ f) x =\n  mult cero (suma tres tres) f x == cero f x\nprop_Mult3 (Fun _ f) x =\n  mult dos tres f x == suma tres tres f x\n\nprop_Exp1, prop_Exp2, prop_Exp3 :: Fun Int Int -> Int -> Bool\nprop_Exp1 (Fun _ f) x =\n  exp dos dos f x == suma dos dos f x\nprop_Exp2 (Fun _ f) x =\n  exp tres dos f x == suma (mult dos (mult dos dos)) uno f x\nprop_Exp3 (Fun _ f) x =\n  exp tres cero f x == uno f x\n  \nreturn []\nrunTests = $quickCheckAll\n\n-- La comprobaci\u00f3n es\n--    \u03bb> runTests\n--    === prop_Succ1 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Suma1 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Mult1 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Exp1 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Succ2 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Succ3 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Suma2 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Suma3 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Mult2 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Mult3 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Exp2 ===\n--    +++ OK, passed 100 tests.\n--    \n--    === prop_Exp3 ===\n--    +++ OK, passed 100 tests.\n--    \n--    True\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Los n\u00fameros naturales pueden definirse de forma alternativa empleando los n\u00fameros de Church. Podemos representar un n\u00famero natural n como una funci\u00f3n que toma una funci\u00f3n f como par\u00e1metro y devuelve n veces f. Definimos por tanto los n\u00fameros naturales como Type Nat = forall a. (a -> a) -> a -> a De esta&#8230;<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[7],"tags":[11,146],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts\/4111"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/comments?post=4111"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts\/4111\/revisions"}],"predecessor-version":[{"id":4136,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/posts\/4111\/revisions\/4136"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/media?parent=4111"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/categories?post=4111"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/wp-json\/wp\/v2\/tags?post=4111"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}