{"id":1238,"date":"2011-02-23T14:14:06","date_gmt":"2011-02-23T14:14:06","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1238"},"modified":"2011-02-24T06:13:49","modified_gmt":"2011-02-24T06:13:49","slug":"i1m2010-ejercicios-de-demostraciones-de-propiedades-de-funciones-haskell-relacion-20","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2010-ejercicios-de-demostraciones-de-propiedades-de-funciones-haskell-relacion-20\/","title":{"rendered":"I1M2010: Ejercicios de demostraciones de propiedades de funciones Haskell (relaci\u00f3n 20)"},"content":{"rendered":"<p>En la clase de hoy de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-10\">Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas<\/a> hemos comentado la resoluci\u00f3n de ejercicios de las relaci\u00f3n 20 en la que se demuestran por inducci\u00f3n propiedades de funciones Haskell.<\/p>\n<p>Las soluciones de los ejercicios se muestran a continuaci\u00f3n.<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\r\n-- ---------------------------------------------------------------------\r\n-- Importaci\u00f3n de librer\u00edas                                           --\r\n-- ---------------------------------------------------------------------\r\n\r\nimport Test.QuickCheck\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1a. Definir por recursi\u00f3n la funci\u00f3n\r\n--    sumaImpares :: Int -> Int\r\n-- tal que (sumaImpares n) es la suma de los n primeros n\u00fameros\r\n-- impares. Por ejemplo,\r\n--    *Main> sumaImpares 5  ==  25\r\n-- ---------------------------------------------------------------------\r\n\r\nsumaImpares :: Int -> Int\r\nsumaImpares 0     = 0\r\nsumaImpares (n+1) = sumaImpares n + (2*n+1) \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1b. Definir, sin usar recursi\u00f3n, la funci\u00f3n\r\n--    sumaImpares' :: Int -> Int\r\n-- tal que (sumaImpares' n) es la suma de los n primeros n\u00fameros\r\n-- impares. Por ejemplo,\r\n--    *Main> sumaImpares' 5  ==  25\r\n-- ---------------------------------------------------------------------\r\n\r\nsumaImpares' :: Int -> Int\r\nsumaImpares' n = sum [1,3..(2*n-1)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1c. Definir la funci\u00f3n\r\n--    sumaImparesIguales :: Int -> Int -> Bool\r\n-- tal que (sumaImparesIguales m n) se verifica si para todo x entre m y\r\n-- n se tiene que (sumaImpares x) y (sumaImpares' x) son iguales.\r\n-- \r\n-- Comprobar que (sumaImpares x) y (sumaImpares' x) son iguales para\r\n-- todos los n\u00fameros x entre 1 y 100.\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La definici\u00f3n es\r\nsumaImparesIguales :: Int -> Int -> Bool\r\nsumaImparesIguales m n = \r\n    and [sumaImpares x == sumaImpares' x | x <- [m..n]]\r\n\r\n-- La comprobaci\u00f3n es\r\n--    *Main>  sumaImparesIguales 1 100\r\n--    True\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1d. Definir la funci\u00f3n \r\n--    grafoSumaImpares :: Int -> Int -> [(Int,Int)]\r\n-- tal que (grafoSumaImpares m n) es la lista formadas por los n\u00fameros x\r\n-- entre m y n y los valores de (sumaImpares x).\r\n--\r\n-- Calcular (grafoSumaImpares 1 9).\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La definici\u00f3n es\r\ngrafoSumaImpares :: Int -> Int -> [(Int,Int)]\r\ngrafoSumaImpares m n =\r\n    [(x,sumaImpares x) | x <- [m..n]]\r\n\r\n-- El c\u00e1lculo es\r\n--    *Main> grafoSumaImpares 1 9\r\n--    [(1,1),(2,4),(3,9),(4,16),(5,25),(6,36),(7,49),(8,64),(9,81)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1e. Demostrar por inducci\u00f3n que para todo n, \r\n-- (sumaImpares n) es igual a n^2.\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Caso base: Hay que demostrar que\r\n    sumaImpares 0 = 0^2 \r\n En efecto,\r\n    sumaImpares 0   [por hip\u00f3tesis]  \r\n    = 0               [por sumaImpares.1]\r\n    = 0^2             [por aritm\u00e9tica]\r\n \r\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n (H.I.)\r\n     sumaImpares n = n^2\r\n  Hay que demostrar que\r\n     sumaImpares (n+1) = (n+1)^2\r\n  En efecto,\r\n     sumaImpares (n+1) = \r\n     = (sumaImpares n) + (2*n+1    )    [por sumaImpares.2]\r\n     = n^2 + (2*n+1)                    [por H.I.]\r\n     = (n+1)^2                          [por \u00e1lgebra]\r\n-} \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2a. Definir por recursi\u00f3n la funci\u00f3n\r\n--    sumaPotenciasDeDosMasUno :: Int -> Int\r\n-- tal que \r\n--    (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. \r\n-- Por ejemplo, \r\n--    sumaPotenciasDeDosMasUno 3  ==  16\r\n-- ---------------------------------------------------------------------\r\n\r\nsumaPotenciasDeDosMasUno :: Int -> Int\r\nsumaPotenciasDeDosMasUno 0     = 2\r\nsumaPotenciasDeDosMasUno (n+1) = sumaPotenciasDeDosMasUno n + 2^(n+1)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2b. Definir por comprensi\u00f3n la funci\u00f3n\r\n--    sumaPotenciasDeDosMasUno' :: Int -> Int\r\n-- tal que \r\n--    (sumaPotenciasDeDosMasUno' n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. \r\n-- Por ejemplo, \r\n--    sumaPotenciasDeDosMasUno' 3  ==  16\r\n-- ---------------------------------------------------------------------\r\n\r\nsumaPotenciasDeDosMasUno' :: Int -> Int\r\nsumaPotenciasDeDosMasUno' n = 1 + sum [2^x | x <- [0..n]]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2c. Demostrar por inducci\u00f3n que\r\n--    sumaPotenciasDeDosMasUno n = 2^(n+1)\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n  Caso base: Hay que demostrar que \r\n     sumaPotenciasDeDosMasUno 0 = 2^(0+1)\r\n  En efecto,\r\n       sumaPotenciasDeDosMasUno 0 \r\n     = 2                              [por sumaPotenciasDeDosMasUno.1]\r\n     = 2^(0+1)                        [por aritm\u00e9tica]\r\n\r\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n (H.I.)\r\n     sumaPotenciasDeDosMasUno n = 2^(n+1)\r\n  Hay que demostrar que \r\n     sumaPotenciasDeDosMasUno (n+1) = 2^((n+1)+1)\r\n  En efecto, \r\n       sumaPotenciasDeDosMasUno (n+1)\r\n     = (sumaPotenciasDeDosMasUno n) + 2^(n+1)  [por sumaPotenciasDeDosMasUno.2]\r\n     = 2^(n+1) + 2^(n+1)                       [por H.I.]\r\n     = 2^((n+1)+1)                             [por aritm\u00e9tica]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3a. Definir por recursi\u00f3n la funci\u00f3n\r\n--    copia :: Int -> a -> [a]\r\n-- tal que (copia n x) es la lista formado por n copias del elemento\r\n-- x. Por ejemplo, \r\n--    copia 3 2  ==  [2,2,2]\r\n-- ---------------------------------------------------------------------\r\n \r\ncopia :: Int -> a -> [a]\r\ncopia 0 _     = []              -- copia.1\r\ncopia (n+1) x = x : copia n x   -- copia.2\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3b. Definir por recursi\u00f3n la funci\u00f3n \r\n--    todos :: (a -> Bool) -> [a] -> Bool\r\n-- tal que (todos p xs) se verifica si todos los elementos de xs cumplen\r\n-- la propiedad p. Por ejemplo,\r\n--    todos even [2,6,4]  ==>  True\r\n--    todos even [2,5,4]  ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\ntodos :: (a -> Bool) -> [a] -> Bool\r\ntodos p []       = True                -- todos.1\r\ntodos p (x : xs) = p x && todos p xs   -- todos.2\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3c. Comprobar con QuickCheck que todos los elementos de \r\n-- (copia n x) son iguales a x.\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_copia :: Eq a => Int -> a -> Bool\r\nprop_copia n x =\r\n    todos (==x) (copia n' x)\r\n    where n' = abs n\r\n\r\n-- La comprobaci\u00f3n es\r\n--    *Main> quickCheck prop_copia\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3d. Demostrar, por inducci\u00f3n en n, que todos los elementos\r\n-- de (copia n x) son iguales a x.\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n  Hay que demostrar que para todo n y todo x,\r\n     todos (==x) (copia n x)\r\n\r\n  Caso base: Hay que demostrar que\r\n     todos (==x) (copia 0 x) = True \r\n  En efecto, \r\n       todos (== x) (copia 0 x)\r\n     = todos (== x) []            [por copia.1] \r\n     = True                       [por todos.1] \r\n\r\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n (H.I.)\r\n     todos (==x) (copia n x) = True\r\n  Hay que demostrar que\r\n     todos (==x) (copia (n+1) x) = True\r\n  En efecto, \r\n       todos (==x) (copia (n+1) x)\r\n     = todos (==x) (x : copia n x )         [por copia.2]\r\n     = x == x && todos (==x) (copia n x )   [por todos.2] \r\n     = True && todos (==x) (copia n x )     [por def. de ==] \r\n     = todos (==x) (copia n x )             [por def. de &&] \r\n     = True                                 [por H.I.]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3e. Definir por plegado la funci\u00f3n \r\n--    todos' :: (a -> Bool) -> [a] -> Bool\r\n-- tal que (todos' p xs) se verifica si todos los elementos de xs cumplen\r\n-- la propiedad p. Por ejemplo,\r\n--    todos' even [2,6,4]  ==>  True\r\n--    todos' even [2,5,4]  ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\ntodos' :: (a -> Bool) -> [a] -> Bool\r\ntodos' p = foldr ((&&) . p) True \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4. Definir la funci\u00f3n\r\n--    traspuesta :: [[a]] -> [[a]]\r\n-- tal que (traspuesta m) es la traspuesta de la matriz m. Por ejemplo,\r\n--    traspuesta [[1,2,3],[4,5,6]]    ==  [[1,4],[2,5],[3,6]]\r\n--    traspuesta [[1,4],[2,5],[3,6]]  ==  [[1,2,3],[4,5,6]]\r\n-- ---------------------------------------------------------------------\r\n\r\ntraspuesta :: [[a]] -> [[a]]\r\ntraspuesta []           = []\r\ntraspuesta ([]:xss)     = traspuesta xss\r\ntraspuesta ((x:xs):xss) = \r\n    (x:[h | (h:_) <- xss]) : traspuesta (xs : [t | (_:t) <- xss])\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy de Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas hemos comentado la resoluci\u00f3n de ejercicios de las relaci\u00f3n 20 en la que se demuestran por inducci\u00f3n propiedades de funciones Haskell. Las soluciones de los ejercicios se muestran a continuaci\u00f3n.<\/p>\n","protected":false},"author":2,"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":[133],"tags":[287],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1238"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=1238"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1238\/revisions"}],"predecessor-version":[{"id":1239,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1238\/revisions\/1239"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1238"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1238"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1238"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}