{"id":3660,"date":"2013-06-04T13:15:58","date_gmt":"2013-06-04T11:15:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3660"},"modified":"2013-09-21T13:18:16","modified_gmt":"2013-09-21T11:18:16","slug":"i1m2012-ejercicios-de-razonamiento-sobre-programas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2012-ejercicios-de-razonamiento-sobre-programas\/","title":{"rendered":"I1M2012: Ejercicios de razonamiento sobre programas"},"content":{"rendered":"<p>En las clases de ayer y hoy  <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-12\">Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas<\/a> hemos comentado las soluciones de la relaci\u00f3n 31 en la que se plantean ejercicios de demostraci\u00f3n por inducci\u00f3n de propiedades de programas. En concreto,<\/p>\n<ul>\n<li> la suma de los n primeros impares es n^2,\n<li> 1 + 2^0 + 2^1 + 2^2 + &#8230; + 2^n = 2^(n+1),\n<li> todos los elementos de (copia n x) son iguales a x,\n<li> la equivalencia de las definiciones de factorial con y sin\n<li> acumulador,\n<li> amplia xs y = xs ++ [y].\n<li> numeroDeListasConSuma n = 2^(n-1),\n<li> fibItAux n (fib k) (fib (k+1)) = fib (k+n),\n<li> potencia x n == x^n,\n<li> reverse (xs ++ ys) == reverse ys ++ reverse xs,\n<li> reverse (reverse xs) = xs,\n<\/ul>\n<p>y por inducci\u00f3n sobre \u00e1rboles binarios<\/p>\n<ul>\n<li> espejo (espejo x) = x,\n<li> postorden (espejo x) = reverse (preorden x),\n<li> reverse (preorden (espejo x)) = postorden x,\n<li> nNodos (espejo x) == nNodos x,\n<li> length (preorden x) == nNodos x,\n<li> nNodos x <= 2^(profundidad x) - 1,\n\n\n<li> nHojas x = nNodos x + 1,\n<li> preordenItAux x ys = preorden x ++ ys\n<\/ul>\n<p>Estos ejercicios corresponden al <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-12\/temas\/tema-8.pdf\">tema 8<\/a> del curso.<\/p>\n<p>Los ejercicios de la relaci\u00f3n, junto con sus soluciones, 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\nimport Control.Monad\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1.1. 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--    sumaImpares 5  ==  25\r\n-- ---------------------------------------------------------------------\r\n\r\nsumaImpares :: Int -> Int\r\nsumaImpares 0 = 0\r\nsumaImpares n = sumaImpares (n-1) + (2*n-1) \r\n\r\n\r\nsumaImpares2 :: Int -> Int\r\nsumaImpares2 0 = 0\r\nsumaImpares2 n = 2*n+1 + sumaImpares2 (n-1)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1.2. 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--    ghci> 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 1.3. 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--    ghci>  sumaImparesIguales 1 100\r\n--    True\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1.4. 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--    ghci> 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 1.5. 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 2.1. 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 = sumaPotenciasDeDosMasUno (n-1) + 2^n\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2.2. 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 2.3. 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 3.1. 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 x = x : copia (n-1) x   -- copia.2\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3.2. 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 3.3. 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--    ghci> quickCheck prop_copia\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3.4. 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 4.1. Definir por recursi\u00f3n la funci\u00f3n \r\n--   factR :: Integer -> Integer\r\n-- tal que (factR n) es el factorial de n. Por ejemplo,\r\n--   factR 4  ==  24\r\n-- ---------------------------------------------------------------------\r\n\r\nfactR :: Integer -> Integer\r\nfactR 0 = 1\r\nfactR n = n * factR (n-1)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4.2. Definir por comprensi\u00f3n la funci\u00f3n \r\n--   factC :: Integer -> Integer\r\n-- tal que (factR n) es el factorial de n. Por ejemplo,\r\n--   factC 4  ==  24\r\n-- ---------------------------------------------------------------------\r\n\r\nfactC :: Integer -> Integer\r\nfactC n = product [1..n]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4.3. Comprobar con QuickCheck que las funciones factR y\r\n-- factC son equivalentes sobre los n\u00fameros naturales.\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_factR_factC :: Integer -> Bool\r\nprop_factR_factC n = \r\n    factR n' == factC n'\r\n    where n' = abs n\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_factR_factC\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4.4. Comprobar con QuickCheck si las funciones factR y\r\n-- factC son equivalentes sobre los n\u00fameros enteros.\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_factR_factC_Int :: Integer -> Bool\r\nprop_factR_factC_Int n = \r\n    factR n == factC n\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_factR_factC_Int\r\n--    *** Exception: Non-exhaustive patterns in function factR\r\n\r\n-- No son iguales ya que factR no est\u00e1 definida para los n\u00fameros\r\n-- negativos y factC de cualquier n\u00famero negativo es 0.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4.5. Se considera la siguiente definici\u00f3n iterativa de la\r\n-- funci\u00f3n factorial \r\n--    factI :: Integer -> Integer\r\n--    factI n = factI' n 1\r\n--    \r\n--    factI' :: Integer -> Integer -> Integer\r\n--    factI' 0 x = x                  -- factI'.1\r\n--    factI' n x = factI' (n-1) n*x   -- factI'.2\r\n-- Comprobar con QuickCheck que factI y factR son equivalentes sobre los\r\n-- n\u00fameros naturales.\r\n-- ---------------------------------------------------------------------\r\n\r\nfactI :: Integer -> Integer\r\nfactI n = factI' n 1\r\n\r\nfactI' :: Integer -> Integer -> Integer\r\nfactI' 0 x = x\r\nfactI' n x = factI' (n-1) n*x \r\n\r\n-- La propiedad es\r\nprop_factI_factR n = \r\n    factI n' == factR n'\r\n    where n' = abs n\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_factI_factR\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4.6. Comprobar con QuickCheck que para todo n\u00famero natural\r\n-- n, (factI' n x) es igual al producto de x y (factR n).\r\n-- --------------------------------------------------------------------- \r\n\r\n-- La propiedad es\r\nprop_factI' :: Integer -> Integer -> Bool\r\nprop_factI' n  x =\r\n    factI' n' x == x * factR n'\r\n    where n' = abs n\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_factI'\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4.7. Demostrar por inducci\u00f3n que para todo n\u00famero natural\r\n-- n, (factI' n x) es igual x*n!\r\n-- --------------------------------------------------------------------- \r\n\r\n{-\r\n  Demostraci\u00f3n (por inducci\u00f3n en n)\r\n\r\n  Caso base: Hay que demostrar que factI' 0 x = x*0!\r\n  En efecto,\r\n     factI' 0 x \r\n     = x           [por factI'.1]\r\n     = x*0!        [por \u00e1lgebra]\r\n\r\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n: para todo x,\r\n     factI' n x = x*n!\r\n  hay que demostrar que para todo x\r\n     factI' (n+1) x = x*(n+1)!\r\n  En efecto,\r\n     factI' (n+1) x\r\n     = factI' n (n+1)*x    [por factI'.2]\r\n     = (n+1)*x*n!          [por hip\u00f3tesis de inducci\u00f3n]\r\n     = x*(n+1)!            [por \u00e1lgebra]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5.1. Definir, recursivamente y sin usar (++). la funci\u00f3n\r\n--    amplia :: [a] -> a -> [a]\r\n-- tal que (amplia xs y) es la lista obtenida a\u00f1adiendo el elemento y al\r\n-- final de la lista xs. Por ejemplo,\r\n--    amplia [2,5] 3  ==  [2,5,3]\r\n-- ---------------------------------------------------------------------\r\n\r\namplia :: [a] -> a -> [a]\r\namplia []     y = [y]               -- amplia.1\r\namplia (x:xs) y = x : amplia xs y   -- amplia.2\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5.2. Definir, mediante plegado. la funci\u00f3n\r\n--    ampliaF :: [a] -> a -> [a]\r\n-- tal que (ampliaF xs y) es la lista obtenida a\u00f1adiendo el elemento y al\r\n-- final de la lista xs. Por ejemplo,\r\n--    ampliaF [2,5] 3  ==  [2,5,3]\r\n-- ---------------------------------------------------------------------\r\n\r\nampliaF :: [a] -> a -> [a]\r\nampliaF xs y = foldr (:) [y] xs\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5.3. Comprobar con QuickCheck que amplia y ampliaF son\r\n-- equivalentes. \r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_amplia_ampliaF :: Eq a => [a] -> a -> Bool\r\nprop_amplia_ampliaF xs y =\r\n    amplia xs y == ampliaF xs y\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_amplia_ampliaF\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5.4. Comprobar con QuickCheck que\r\n--    amplia xs y = xs ++ [y]\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_amplia :: Eq a => [a] -> a -> Bool\r\nprop_amplia xs y =\r\n    amplia xs y == xs ++ [y]\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_amplia\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5.5. Demostrar por inducci\u00f3n que\r\n--    amplia xs y = xs ++ [y]\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n  Demostraci\u00f3n: Por inducci\u00f3n en xs.\r\n\r\n  Caso base: Hay que demostrar que \r\n     amplia [] y = [] ++ [y]\r\n  En efecto,\r\n     amplia [] y \r\n     = [y]         [por amplia.1]\r\n     = [] ++ [y]   [por (++).1]\r\n\r\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n     amplia xs y = xs ++ [y]\r\n  Hay que demostrar que\r\n     amplia (x:xs) y = (x:xs) ++ [y]\r\n  En efecto,\r\n     amplia (x:xs) y\r\n     = x : amplia xs y    [por amplia.2]\r\n     = x : (xs ++ [y])    [por hip\u00f3tesis de inducci\u00f3n]\r\n     = (x:xs) ++ [y]      [por (++).2]\r\n-}\r\n\r\n-- ----------------------------------------------------------------------\r\n-- Ejercicio 6.1. Definir la funci\u00f3n \r\n--    listaConSuma :: Int -> [[Int]] \r\n-- que, dado un n\u00famero natural n, devuelve todas las listas de enteros\r\n-- positivos (esto es, enteros mayores o iguales que 1) cuya suma sea\r\n-- n. Por ejemplo,\r\n--    Main> listaConSuma 4\r\n--    [[1,1,1,1],[1,1,2],[1,2,1],[1,3],[2,1,1],[2,2],[3,1],[4]]\r\n-- ---------------------------------------------------------------------\r\n\r\nlistaConSuma :: Int -> [[Int]]\r\nlistaConSuma 0 = [[]]\r\nlistaConSuma n = [x:xs | x <- [1..n], xs <- listaConSuma (n-x)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6.2. Definir la funci\u00f3n\r\n--    numeroDeListasConSuma :: Int -> Int\r\n-- tal que (numeroDeListasConSuma n) es el n\u00famero de elementos de\r\n-- (listaConSuma n). Por ejemplo,\r\n--    numeroDeListasConSuma 10  =  512\r\n-- ---------------------------------------------------------------------\r\n\r\nnumeroDeListasConSuma :: Int -> Int\r\nnumeroDeListasConSuma = length . listaConSuma\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6.2. Definir la constante\r\n--    numerosDeListasConSuma :: [(Int,Int)]\r\n-- tal que numerosDeListasConSuma es la lista de los pares formado por un\r\n-- n\u00famero natural n mayor que 0 y el n\u00famero de elementos de \r\n-- (listaConSuma n). \r\n--\r\n-- Calcular el valor de\r\n--    take 10 numerosDeListasConSuma\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La constante es\r\nnumerosDeListasConSuma :: [(Int,Int)]\r\nnumerosDeListasConSuma = [(n,numeroDeListasConSuma n) | n <- [1..]] \r\n\r\n-- El c\u00e1lculo es\r\n--    ghci> take 10 numerosDeListasConSuma\r\n--    [(1,1),(2,2),(3,4),(4,8),(5,16),(6,32),(7,64),(8,128),(9,256),(10,512)]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6.4. A partir del ejercicio anterior, encontrar una f\u00f3rmula\r\n-- para calcular el valor de (numeroDeListasConSuma n) paras los\r\n-- n\u00fameros n mayores que 0. \r\n-- \r\n-- Demostrar dicha f\u00f3rmula por inducci\u00f3n fuerte.\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n La f\u00f3rmula es\r\n    numeroDeListasConSuma n = 2^(n-1)\r\n La demostraci\u00f3n, por inducci\u00f3n fuerte en n, es la siguiente:\r\n\r\n Caso base (n=1):\r\n    numeroDeListasConSuma 1 \r\n    = length (listaConSuma 1)    \r\n         [por numeroDeListasConSuma]\r\n    = length [[x:xs | x <- [1..1], xs <- listaConSuma [[]]]\r\n         [por listaConSuma.2]\r\n    = length [[1]]\r\n         [por def. de listas de comprensi\u00f3n]\r\n    = 1\r\n         [por def. de length] \r\n    = 2^(1-1)\r\n         [por aritm\u00e9tica] \r\n\r\n Paso de inducci\u00f3n: Se supone que\r\n    para todo x en [1..n-1], \r\n       numeroDeListasConSuma x = 2^(x-1)\r\n Hay que demostrar que\r\n    numeroDeListasConSuma n = 2^(n-1)\r\n En efecto,\r\n    numeroDeListasConSuma n\r\n    = length (listaConSuma n)   \r\n         [por numeroDeListasConSuma]\r\n    = length [x:xs | x <- [1..n], xs <- listaConSuma (n-x)]\r\n         [por listaConSuma.2]\r\n    = sum [numeroDeListasConSuma (n-x) | x <- [1..n]]\r\n         [por length y listas de comprensi\u00f3n]\r\n    = sum [2^(n-x-1) | x <- [1..n-1]] + 1\r\n         [por hip. de inducci\u00f3n y numeroDeListasConSuma]\r\n    = 2^(n-2) + 2^(n-3) + ... + 2^1 + 2^0 + 1\r\n    = 2^(n-1)\r\n         [por el ejercicio 2c de la relaci\u00f3n 15]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6.4. A partir del ejercicio anterior, definir de manera m\u00e1s\r\n-- eficiente la funci\u00f3n numeroDeListasConSuma.\r\n-- ---------------------------------------------------------------------\r\n\r\nnumeroDeListasConSuma' :: Int -> Int\r\nnumeroDeListasConSuma' 0 = 1\r\nnumeroDeListasConSuma' n = 2^(n-1)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6.5. Comparar la eficiencia de las dos definiciones\r\n-- comparando el tiempo y el espacio usado para calcular \r\n-- (numeroDeListasConSuma 20) y (numeroDeListasConSuma' 20).\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La comparaci\u00f3n es\r\n--    ghci> :set +s\r\n--    ghci> numeroDeListasConSuma 20\r\n--    524288\r\n--    (9.99 secs, 519419824 bytes)\r\n--    ghci> numeroDeListasConSuma' 20\r\n--    524288\r\n--    (0.01 secs, 0 bytes)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7.0. La sucesi\u00f3n de Fibonacci \r\n--    0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, ...\r\n-- puede definirse por recursi\u00f3n como\r\n--    fib :: Int -> Int\r\n--    fib 0 = 0                           -- fib.1\r\n--    fib 1 = 1                           -- fib.2\r\n--    fib n = (fib (n-11)) + fib (n-2)    -- fib.3\r\n-- Tambi\u00e9n puede definirse por recursici\u00f3n iterativa como\r\n--    fibIt :: Int -> Int\r\n--    fibIt n = fibItAux n 0 1\r\n-- donde la funci\u00f3n auxiliar se define por\r\n--    fibItAux :: Int -> Int -> Int -> Int\r\n--    fibItAux 0 a b = a                        -- fibItAux.1\r\n--    fibItAux n a b = fibItAux (n-1) b (a+b)   -- fibItAux.2 \r\n-- ---------------------------------------------------------------------\r\n\r\nfib :: Int -> Int\r\nfib 0 = 0\r\nfib 1 = 1\r\nfib n = fib (n-1) + fib (n-2) \r\n\r\nfibIt :: Int -> Int\r\nfibIt n = fibItAux n 0 1\r\n\r\nfibItAux :: Int -> Int -> Int -> Int\r\nfibItAux 0 a b = a\r\nfibItAux n a b = fibItAux (n-1) b (a+b) \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7.1. Comprobar con QuickCheck que para todo n\u00famero natural\r\n-- n tal que n <= 20, se tiene que\r\n--    fib n = fibIt n\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_fib :: Int -> Property\r\nprop_fib n =\r\n    n >= 0 && n <= 20 ==> fib n == fibIt n\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_fib\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7.2. Sea f la funci\u00f3n definida por\r\n--    f :: Int -> Int -> Int\r\n--    f n k = fibItAux n (fib k) (fib (k+1))\r\n-- Definir la funci\u00f3n \r\n--    grafoDeF :: Int -> [(Int,Int)]\r\n-- tal que (grafoDeF n)\r\n--    ghci> take 7 (grafoDeF 3)\r\n--    [(1,3),(2,5),(3,8),(4,13),(5,21),(6,34),(7,55)]\r\n--    ghci> take 7 (grafoDeF 5)\r\n--    [(1,8),(2,13),(3,21),(4,34),(5,55),(6,89),(7,144)]\r\n-- ---------------------------------------------------------------------\r\n\r\nf :: Int -> Int -> Int\r\nf n k = fibItAux n (fib k) (fib (k+1))\r\n\r\ngrafoDeF :: Int -> [(Int,Int)]\r\ngrafoDeF n = [(k, f n k) | k <- [1..]]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7.3. Comprobar con QuickCheck que para todo par de n\u00fameros\r\n-- naturales n, k tales que n+k <= 20, se tiene que\r\n--    fibItAux n (fib k) (fib (k+1)) = fib (k+n)\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_fibItAux :: Int -> Int -> Property\r\nprop_fibItAux n k =\r\n    n >= 0 && k >= 0 && n+k <= 20 ==>\r\n    fibItAux n (fib k) (fib (k+1)) == fib (k+n)\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_fibItAux\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7.4. Demostrar por inducci\u00f3n que para todo n y todo k,\r\n--    fibItAux n (fib k) (fib (k+1)) = fib (k+n)\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n: Por inducci\u00f3n en n se prueba que\r\n    para todo k, fibItAux n (fib k) (fib (k+1)) = fib (k+n)\r\n\r\n Caso base (n=0): Hay que demostrar que\r\n    para todo k, fibItAux 0 (fib k) (fib (k+1)) = fib k\r\n En efecto, sea k un n\u00famero natural. Se tiene\r\n    fibItAux 0 (fib k) (fib (k+1))\r\n    = fib k                          [por fibItAux.1]\r\n\r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    para todo k, fibItAux n (fib k) (fib (k+1)) = fib (k+n)\r\n Hay que demostrar que\r\n    para todo k, fibItAux (n+1) (fib k) (fib (k+1)) = fib (k+n+1)\r\n En efecto. Sea k un n\u00famero natural,\r\n    fibItAux (n+1) (fib k) (fib (k+1))\r\n    = fibItAux n (fib (k+1)) ((fib k) + (fib (k+1)))\r\n         [por fibItAux.2]\r\n    = fibItAux n (fib (k+1)) (fib (k+2))\r\n         [por fib.3]\r\n    = fib (n+k+1)\r\n         [por hip\u00f3tesis de inducci\u00f3n]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7.5. Demostrar que para todo n,\r\n--    fibIt n = fib n\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n\r\n    fibIt n \r\n    = fibItAux n 0 1               [por fibIt]\r\n    = fibItAux n (fib 0) (fib 1)   [por fib.1 y fib.2]\r\n    = fib n                        [por ejercicio 5.4]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 8.1. La funci\u00f3n potencia puede definirse por\r\n--    potencia :: Int -> Int -> Int\r\n--    potencia x 0 = 1\r\n--    potencia x n | even n    = potencia (x*x) (div n 2)\r\n--                 | otherwise = x * potencia (x*x) (div n 2)\r\n-- Comprobar con QuickCheck que para todo n\u00famero natural n y todo\r\n-- n\u00famero entero x, (potencia x n) es x^n.\r\n-- ---------------------------------------------------------------------\r\n\r\npotencia :: Integer -> Integer -> Integer\r\npotencia x 0 = 1\r\npotencia x n | even n    = potencia (x*x) (div n 2)\r\n             | otherwise = x * potencia (x*x) (div n 2)\r\n\r\n-- La propiedad es\r\nprop_potencia :: Integer -> Integer -> Property\r\nprop_potencia x n =\r\n    n >= 0 ==> potencia x n == x^n\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_potencia\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 8.2. Demostrar por inducci\u00f3n que que para todo n\u00famero\r\n-- natural n y todo n\u00famero entero x, (potencia x n) es x^n\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n: Por inducci\u00f3n en n.\r\n\r\n Caso base: Hay que demostrar que \r\n    para todo x, potencia x 0 = 2^0\r\n Sea x un n\u00famero entero, entonces\r\n    potencia x 0 \r\n    = 1              [por potencia.1]\r\n    = 2^0            [por aritm\u00e9tica]\r\n\r\n Paso de inducci\u00f3n: Se supone que n>0 y la hip\u00f3tesis de inducci\u00f3n: \r\n    para todo m<n y para todo x, potencia x (n-1) = x^(n-1)\r\n Tenemos que demostrar que \r\n    para todo x, potencia x n = x^n\r\n Lo haremos distinguiendo casos seg\u00fan la paridad de n.\r\n\r\n Caso 1: Supongamos que n es par. Entonces, existe un k tal que \r\n    n = 2*k.                    (1)\r\n Por tanto, \r\n    potencia  n \r\n    = potencia (x*x) (div n 2)  [por potencia.2]\r\n    = potencia (x*x) k          [por (1)]\r\n    = (x*x)^k                   [por hip. de inducci\u00f3n]\r\n    = x^(2*k)                   [por aritm\u00e9tica]\r\n    = x^n                       [por (1)]\r\n\r\n Caso 2: Supongamos que n es impar. Entonces, existe un k tal que \r\n    n = 2*k+1.                       (2)\r\n Por tanto, \r\n    potencia  n \r\n    = x * potencia (x*x) (div n 2)   [por potencia.3]\r\n    = x * potencia (x*x) k           [por (1)]\r\n    = x * (x*x)^k                    [por hip. de inducci\u00f3n]\r\n    = x^(2*k+1)                      [por aritm\u00e9tica]\r\n    = x^n                            [por (1)]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 9.1. Comprobar con QuickCheck que para todo par de listas\r\n-- xs, ys se tiene que\r\n--    reverse (xs ++ ys) == reverse ys ++ reverse xs\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_reverse_conc :: [Int] -> [Int] -> Bool\r\nprop_reverse_conc xs ys =\r\n    reverse (xs ++ ys) == reverse ys ++ reverse xs\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_reverse_conc\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 9.2. Demostrar por inducci\u00f3n que para todo par de listas\r\n-- xs, ys se tiene que\r\n--    reverse (xs ++ ys) == reverse ys ++ reverse xs\r\n-- \r\n-- Las definiciones de reverse y (++) son\r\n--    reverse [] = []                      -- reverse.1\r\n--    reverse (x:xs) = reverse xs ++ [x]   -- reverse.2\r\n-- \r\n--    [] ++ ys     = ys                    -- ++.1\r\n--    (x:xs) ++ ys = x : (xs ++ ys)        -- ++.2\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n por inducci\u00f3n en xs.\r\n\r\n Caso base: Hay que demostrar que para toda ys,\r\n    reverse ([] ++ ys) == reverse ys ++ reverse []\r\n En efecto,\r\n    reverse ([] ++ ys)\r\n    = reverse ys                  [por ++.1] \r\n    = reverse ys ++ []            [por propiedad de ++]\r\n    = reverse ys ++ reverse []    [por reverse.1]\r\n\r\n Paso de inducci\u00f3n: Se supone que para todo ys,\r\n    reverse (xs ++ ys) == reverse ys ++ reverse xs\r\n Hay que demostrar que para todo ys,   \r\n    reverse ((x:xs) ++ ys) == reverse ys ++ reverse (x:xs)\r\n En efecto,\r\n    reverse ((x:xs) ++ ys)\r\n    = reverse (x:(xs ++ ys))               [por ++.2]\r\n    = reverse (xs ++ ys) ++ [x]            [por reverse.2]\r\n    = (reverse ys ++ reverse xs) ++ [x]    [por hip. de inducci\u00f3n]\r\n    = reverse ys ++ (reverse xs ++ [x])    [por asociativa de ++]\r\n    = reverse ys ++ reverse (x:xs)         [por reverse.2]  \r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 9.3. Demostrar por inducci\u00f3n que para toda lista xs,\r\n--    reverse (reverse xs) = xs\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n por inducci\u00f3n en xs.\r\n\r\n Caso Base: Hay que demostrar que \r\n    reverse (reverse []) = []\r\n En efecto, \r\n    reverse (reverse [])\r\n    = reverse []           [por reverse.1]\r\n    = []                   [por reverse.1]\r\n\r\n Paso de inducci\u00f3n: Se supone que\r\n    reverse (reverse xs) = xs\r\n Hay que demostrar que\r\n    reverse (reverse (x:xs)) = x:xs\r\n En efecto,\r\n    reverse (reverse (x:xs))\r\n    = reverse (reverse xs ++ [x])           [por reverse.2]\r\n    = reverse [x] ++ reverse (reverse xs)   [por ejercicio 7.2]\r\n    = [x] ++ reverse (reverse xs)           [por reverse]\r\n    = [x] ++ xs                             [por hip. de inducci\u00f3n]\r\n    = x:xs                                  [por ++.2]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.0. En los siguientes ejercicios se demostrar\u00e1n\r\n-- propiedades de los \u00e1rboles binarios definidos como sigue\r\n--    data Arbol a = Hoja \r\n--                 | Nodo a (Arbol a) (Arbol a)\r\n--                 deriving (Show, Eq)\r\n-- En los ejemplos se usar\u00e1 el siguiente \u00e1rbol\r\n--    arbol = Nodo 9\r\n--                   (Nodo 3 \r\n--                         (Nodo 2 Hoja Hoja) \r\n--                         (Nodo 4 Hoja Hoja)) \r\n--                   (Nodo 7 Hoja Hoja)\r\n-- ---------------------------------------------------------------------\r\n\r\ndata Arbol a = Hoja \r\n             | Nodo a (Arbol a) (Arbol a)\r\n             deriving (Show, Eq)\r\n\r\narbol = Nodo 9\r\n               (Nodo 3 \r\n                     (Nodo 2 Hoja Hoja) \r\n                     (Nodo 4 Hoja Hoja)) \r\n               (Nodo 7 Hoja Hoja)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Nota. Para comprobar propiedades de \u00e1rboles con QuickCheck se\r\n-- utilizar\u00e1 el siguiente generador.\r\n-- ---------------------------------------------------------------------\r\n\r\ninstance Arbitrary a => Arbitrary (Arbol a) where\r\n  arbitrary = sized arbol\r\n    where\r\n      arbol 0       = return Hoja \r\n      arbol n | n>0 = oneof [return Hoja,\r\n                             liftM3 Nodo arbitrary subarbol subarbol]\r\n                      where subarbol = arbol (div n 2)\r\n  -- coarbitrary = undefined\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.1. Definir la funci\u00f3n\r\n--    espejo :: Arbol a -> Arbol a\r\n-- tal que (espejo x) es la imagen especular del \u00e1rbol x. Por ejemplo,\r\n--    ghci> espejo arbol\r\n--    Nodo 9 \r\n--         (Nodo 7 Hoja Hoja) \r\n--         (Nodo 3 \r\n--               (Nodo 4 Hoja Hoja) \r\n--               (Nodo 2 Hoja Hoja))\r\n-- ---------------------------------------------------------------------\r\n\r\nespejo :: Arbol a -> Arbol a\r\nespejo Hoja         = Hoja\r\nespejo (Nodo x i d) = Nodo x (espejo d) (espejo i)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.2. Comprobar con QuickCheck que para todo \u00e1rbol x,\r\n--    espejo (espejo x) = x\r\n-- ---------------------------------------------------------------------\r\n\r\nprop_espejo :: Arbol Int -> Bool\r\nprop_espejo x =\r\n    espejo (espejo x) == x\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.3. Demostrar por inducci\u00f3n que para todo \u00e1rbol x,\r\n--    espejo (espejo x) = x\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n por inducci\u00f3n en x\r\n\r\n Caso base: Hay que demostrar que\r\n    espejo (espejo Hoja) = Hoja\r\n En efecto,\r\n    espejo (espejo Hoja)\r\n    = espejo Hoja          [por espejo.1]\r\n    = Hoja                 [por espejo.1]\r\n\r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    espejo (espejo i) = i\r\n    espejo (espejo d) = d\r\n Hay que demostrar que\r\n    espejo (espejo (Nodo x i d)) = Nodo x i d\r\n En efecto,\r\n    espejo (espejo (Nodo x i d))\r\n    = espejo (Nodo x (espejo d) (espejo i))             [por espejo.2]\r\n    = Nodo x (espejo (espejo i)) (espejo (espejo d))    [por espejo.2]\r\n    = Nodo x i d                                        [por hip. inducci\u00f3n]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.4. Definir la funci\u00f3n\r\n--    preorden :: Arbol a -> [a]\r\n-- tal que (preorden x) es la lista correspondiente al recorrido\r\n-- preorden del \u00e1rbol x; es decir, primero visita la ra\u00edz del \u00e1rbol, a\r\n-- continuaci\u00f3n recorre el sub\u00e1rbol izquierdo y, finalmente, recorre el\r\n-- sub\u00e1rbol derecho. Por ejemplo,\r\n--    ghci> arbol\r\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\r\n--    ghci> preorden arbol\r\n--    [9,3,2,4,7]\r\n-- ---------------------------------------------------------------------\r\n\r\npreorden :: Arbol a -> [a]\r\npreorden Hoja         = []\r\npreorden (Nodo x i d) = x : (preorden i ++ preorden d)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.5. Definir la funci\u00f3n\r\n--    postorden :: Arbol a -> [a]\r\n-- tal que (postorden x) es la lista correspondiente al recorrido\r\n-- postorden del \u00e1rbol x; es decir, primero recorre el sub\u00e1rbol\r\n-- izquierdo, a continuaci\u00f3n el sub\u00e1rbol derecho y, finalmente, la ra\u00edz\r\n-- del \u00e1rbol. Por ejemplo,\r\n--    ghci> arbol\r\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\r\n--    ghci> postorden arbol\r\n--    [2,4,3,7,9]\r\n-- ---------------------------------------------------------------------\r\n\r\npostorden :: Arbol a -> [a]\r\npostorden Hoja         = []\r\npostorden (Nodo x i d) = postorden i ++ postorden d ++ [x]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.6. Comprobar con QuickCheck que para todo \u00e1rbol x,\r\n--    postorden (espejo x) = reverse (preorden x)\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_recorrido :: Arbol Int -> Bool\r\nprop_recorrido x =\r\n   postorden (espejo x) == reverse (preorden x)\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_recorrido\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.7. Demostrar por inducci\u00f3n que para todo \u00e1rbol x,\r\n--    postorden (espejo x) = reverse (preorden x)\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n por inducci\u00f3n en x.\r\n\r\n Caso base: Hay que demostrar que \r\n    postorden (espejo Hoja) = reverse (preorden Hoja)\r\n En efecto,\r\n    postorden (espejo Hoja)\r\n    = postorden Hoja           [por espejo.1]\r\n    = []                       [por postorden.1]\r\n    = reverse []               [por reverse.1]\r\n    = reverse (preorden Hoja)  [por preorden.1]\r\n\r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    postorden (espejo i) = reverse (preorden i)\r\n    postorden (espejo d) = reverse (preorden d)\r\n Hay que demostrar que\r\n    postorden (espejo (Nodo x i d)) = reverse (preorden (Nodo x i d))\r\n En efecto,\r\n    postorden (espejo (Nodo x i d))\r\n    = postorden (Nodo x (espejo d) (espejo i))   [por espejo.2]\r\n    = postorden (espejo d) ++ postorden (espejo i) ++ [x]                \r\n                                                 [por postorden.2]\r\n    = reverse (preorden d) ++ reverse (preorden i) ++ [x]\r\n                                                 [por hip. inducci\u00f3n]\r\n    = reverse ([x] ++ preorden (espejo i) ++ preorden (espejo d))      \r\n                                                 [por ejercicio 7.1]\r\n    = reverse (preorden (Nodo x i d))            [por preorden.1]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.8. Comprobar con QuickCheck que para todo \u00e1rbol binario\r\n-- x, se tiene que\r\n--    reverse (preorden (espejo x)) = postorden x\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_reverse_preorden_espejo :: Arbol Int -> Bool\r\nprop_reverse_preorden_espejo x =\r\n   reverse (preorden (espejo x)) == postorden x\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_reverse_preorden_espejo\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.9. Demostrar que para todo \u00e1rbol binario x, se tiene que\r\n--    reverse (preorden (espejo x)) = preorden x\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n:\r\n    reverse (preorden (espejo x))\r\n    = postorden (espejo (espejo x))    [por ejercicio 8.7]\r\n    = postorden x                      [por ejercicio 8.3]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.10. Definir la funci\u00f3n\r\n--    nNodos :: Arbol a -> Int\r\n-- tal que (nNodos x) es el n\u00famero de nodos del \u00e1rbol x. Por ejemplo,\r\n--    ghci> arbol\r\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\r\n--    ghci> nNodos arbol\r\n--    5\r\n-- ---------------------------------------------------------------------\r\n\r\nnNodos :: Arbol a -> Int\r\nnNodos Hoja         = 0\r\nnNodos (Nodo x i d) = 1 + nNodos i + nNodos d\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.11. Comprobar con QuickCheck que el n\u00famero de nodos de la\r\n-- imagen especular de un \u00e1rbol es el mismo que el n\u00famero de nodos del\r\n-- \u00e1rbol. \r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_nNodos_espejo :: Arbol Int -> Bool\r\nprop_nNodos_espejo x =\r\n   nNodos (espejo x) == nNodos x\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_nNodos_espejo\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.12. Demostrar por inducci\u00f3n que el n\u00famero de nodos de la\r\n-- imagen especular de un \u00e1rbol es el mismo que el n\u00famero de nodos del\r\n-- \u00e1rbol. \r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n: Hay que demostrar, por inducci\u00f3n en x, que \r\n    nNodos (espejo x) == nNodos x\r\n \r\n Caso base: Hay que demostrar que\r\n    nNodos (espejo Hoja) == nNodos Hoja\r\n En efecto,\r\n    nNodos (espejo Hoja)\r\n    = nNodos Hoja          [por espejo.1]\r\n\r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    nNodos (espejo i) == nNodos i\r\n    nNodos (espejo d) == nNodos d\r\n Hay que demostrar que\r\n    nNodos (espejo (Nodo x i d)) == nNodos (Nodo x i d)\r\n En esfecto,\r\n    nNodos (espejo (Nodo x i d))\r\n    = nNodos (Nodo x (espejo d) (espejo i))       [por espejo.2]\r\n    = 1 + nNodos (espejo d) + nNodos (espejo i)   [por nNodos.2]\r\n    = 1 + nNodos d + nNodos i                     [por hip.de inducci\u00f3n]\r\n    = 1 + nNodos i + nNodos d                     [por aritm\u00e9tica]\r\n    = nNodos (Nodo x i d)                         [por nNodos.2]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.13. Comprobar con QuickCheck que la longitud de la lista\r\n-- obtenida recorriendo un \u00e1rbol en sentido preorden es igual al n\u00famero\r\n-- de nodos del \u00e1rbol.\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_length_preorden :: Arbol Int -> Bool\r\nprop_length_preorden x =\r\n   length (preorden x) == nNodos x\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_length_preorden\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.14. Demostrar por inducci\u00f3n que la longitud de la lista\r\n-- obtenida recorriendo un \u00e1rbol en sentido preorden es igual al n\u00famero\r\n-- de nodos del \u00e1rbol.\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n: Por inducci\u00f3n en x, hay que demostrar que\r\n    length (preorden x) == nNodos x\r\n  \r\n Caso base: Hay que demostrar que \r\n    length (preorden Hoja) = nNodos Hoja\r\n En efecto,\r\n    length (preorden Hoja)\r\n    = length []              [por preorden.1]\r\n    = 0                      [por length.1]\r\n    = nNodos Hoja            [por nNodos.1]\r\n\r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    length (preorden i) == nNodos i\r\n    length (preorden d) == nNodos d\r\n Hay que demostrar que\r\n    length (preorden (Nodo x i d)) == nNodos (Nodo x i d)\r\n En efecto,\r\n    length (preorden (Nodo x i d))\r\n    = length ([x] ++ (peorden i) ++ (preorden d))   \r\n         [por preorden.2]\r\n    = length [x] + length (preorden i) + length (preorden d) \r\n         [propiedad de length: length (xs++ys) = length xs + length ys]\r\n    = 1 + length (preorden i) + length (preorden d) \r\n         [por def. de length]\r\n    = 1 + nNodos i + nNodos d\r\n         [por hip. de inducci\u00f3n]\r\n    = nNodos (x i d)\r\n         [por nNodos.2]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.15. Definir la funci\u00f3n\r\n--    profundidad :: Arbol a -> Int\r\n-- tal que (profundidad x) es la profundidad del \u00e1rbol x. Por ejemplo,\r\n--    ghci> arbol\r\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\r\n--    ghci> profundidad arbol\r\n--    3\r\n-- ---------------------------------------------------------------------\r\n\r\nprofundidad :: Arbol a -> Int\r\nprofundidad Hoja = 0\r\nprofundidad (Nodo x i d) = 1 + max (profundidad i) (profundidad d)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.16. Comprobar con QuickCheck que para todo \u00e1rbol biario\r\n-- x, se tiene que\r\n--    nNodos x <= 2^(profundidad x) - 1\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_nNodosProfundidad :: Arbol Int -> Bool\r\nprop_nNodosProfundidad x =\r\n   nNodos x <= 2^(profundidad x) - 1\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_nNodosProfundidad\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.17. Demostrar por inducci\u00f3n que para todo \u00e1rbol binario\r\n-- x, se tiene que\r\n--    nNodos x <= 2^(profundidad x) - 1\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n por inducci\u00f3n en x\r\n \r\n Caso base: Hay que demostrar que \r\n    nNodos Hoja <= 2^(profundidad Hoja) - 1\r\n En efecto,\r\n    nNodos Hoja\r\n    = 0                            [por nNodos.1]\r\n    = 2^0 - 1                      [por aritm\u00e9tica]\r\n    = 2^(profundidad Hoja) - 1     [por profundidad.1]\r\n\r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    nNodos i <= 2^(profundidad i) - 1    \r\n    nNodos d <= 2^(profundidad d) - 1    \r\n Hay que demostrar que \r\n    nNodos (Nodo x i d) <= 2^(profundidad (Nodo x i d)) - 1    \r\n En efecto,\r\n    nNodos (Nodo x i d)\r\n    =  1 + nNodos i + nNodos d    \r\n          [por nNodos.1]\r\n    <= 1 + (2^(profundidad i) - 1) + (2^(profundidad d) - 1)\r\n          [por hip. de inducci\u00f3n]\r\n    =  2^(profundidad i) + 2^(profundidad d) - 1   \r\n          [por aritm\u00e9tica]\r\n    <= 2^m\u00e1x(profundidad i,profundidad d)+2^m\u00e1x(profundidad i,profundidad d)-1\r\n          [por aritm\u00e9tica]\r\n    =  2*2^m\u00e1x(profundidad i,profundidad d) - 1\r\n          [por aritm\u00e9tica]\r\n    =  2^(1+m\u00e1x(profundidad i,profundidad d)) - 1\r\n          [por aritm\u00e9tica]\r\n    =  2^profundidad(Nodo x i d) - 1\r\n          [por profundidad.2]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.18. Definir la funci\u00f3n\r\n--    nHojas :: Arbol a -> Int\r\n-- tal que (nHojas x) es el n\u00famero de hojas del \u00e1rbol x. Por ejemplo,\r\n--    ghci> arbol\r\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\r\n--    ghci> nHojas arbol\r\n--    6\r\n-- ---------------------------------------------------------------------\r\n\r\nnHojas :: Arbol a -> Int\r\nnHojas Hoja         = 1\r\nnHojas (Nodo x i d) = nHojas i + nHojas d\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.19. Comprobar con QuickCheck que en todo \u00e1rbol binario el\r\n-- n\u00famero de sus hojas es igual al n\u00famero de sus nodos m\u00e1s uno.\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_nHojas :: Arbol Int -> Bool\r\nprop_nHojas x =\r\n    nHojas x == nNodos x + 1\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_nHojas\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.20. Demostrar por inducci\u00f3n que en todo \u00e1rbol binario el\r\n-- n\u00famero de sus hojas es igual al n\u00famero de sus nodos m\u00e1s uno.\r\n-- ---------------------------------------------------------------------\r\n\r\n{-\r\n Demostraci\u00f3n: Hay que demostrar, por inducci\u00f3n en x, que\r\n    nHojas x = nNodos x + 1\r\n\r\n Caso base: Hay que demotrar que\r\n    nHojas Hoja = nNodos Hoja + 1\r\n En efecto, \r\n    nHojas Hoja\r\n    = 1                 [por nHojas.1]\r\n    = 0 + 1             [por aritm\u00e9tica]\r\n    = nNodos Hoja + 1   [por nNodos.1]\r\n\r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    nHojas i = nNodos i + 1\r\n    nHojas d = nNodos d + 1\r\n Hay que demostrar que\r\n    nHojas (Nodo x i d) = nNodos (Nodo x i d) + 1\r\n En efecto,\r\n    nHojas (Nodo x i d)\r\n    = nHojas i + nHojas d               [por nHojas.2]\r\n    = (nNodos i + 1) + (nNodos d +1)    [por hip. de inducci\u00f3n]\r\n    = (1 + nNodos i + nNodos d) + 1     [por aritm\u00e9tica]\r\n    = nNodos (Nodo x i d) + 1           [por nNodos.2]\r\n-}\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.21. Definir, usando un acumulador, la funci\u00f3n\r\n--    preordenIt :: Arbol a -> [a]\r\n-- tal que (preordenIt x) es la lista correspondiente al recorrido\r\n-- preorden del \u00e1rbol x; es decir, primero visita la ra\u00edz del \u00e1rbol, a\r\n-- continuaci\u00f3n recorre el sub\u00e1rbol izquierdo y, finalmente, recorre el\r\n-- sub\u00e1rbol derecho. Por ejemplo,\r\n--    ghci> arbol\r\n--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)\r\n--    ghci> preordenIt arbol\r\n--    [9,3,2,4,7]\r\n-- Nota: No usar (++) en la definici\u00f3n\r\n-- ---------------------------------------------------------------------\r\n\r\npreordenIt :: Arbol a -> [a]\r\npreordenIt x = preordenItAux x []\r\n\r\npreordenItAux :: Arbol a -> [a] -> [a]\r\npreordenItAux Hoja xs         = xs\r\npreordenItAux (Nodo x i d) xs = x : preordenItAux i (preordenItAux d xs)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.22. Comprobar con QuickCheck que preordenIt es\r\n-- equivalente a preorden.\r\n-- ---------------------------------------------------------------------\r\n\r\n-- La propiedad es\r\nprop_preordenIt :: Arbol Int -> Bool\r\nprop_preordenIt x =\r\n    preordenIt x == preorden x\r\n\r\n-- La comprobaci\u00f3n es\r\n--    ghci> quickCheck prop_preordenIt\r\n--    OK, passed 100 tests.\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10.22. Demostrar que preordenIt es equivalente a preorden.\r\n-- ---------------------------------------------------------------------\r\n\r\nprop_preordenItAux :: Arbol Int -> [Int] -> Bool\r\nprop_preordenItAux x ys =\r\n   preordenItAux x ys == preorden x ++ ys\r\n\r\n{-\r\n Demostraci\u00f3n: La propiedad es consecuencia del siguiente lema:\r\n \r\n Lema: Para todo \u00e1rbol binario x, se tiene que \r\n    para toda ys, preordenItAux x ys = preorden x ++ ys\r\n\r\n Demostraci\u00f3n de la propiedad usando el lema:\r\n    preordenIt x\r\n    = preordenItAux x []    [por preordnIt]\r\n    = preorden x ++ []      [por el lema]\r\n    = preorden x            [propiedad de ++]\r\n\r\n Demostraci\u00f3n del lema: Por inducci\u00f3n en x.\r\n\r\n Caso base: Hay que demotrar que\r\n    para toda ys, preordenItAux Hoja ys = preorden Hoja ++ ys\r\n En efecto, \r\n    preordenItAux Hoja ys\r\n    = ys                     [por preordenItAux.1]\r\n    = [] ++ ys               [por propiedad de ++]\r\n    = preorden Hoja ++ ys    [por preorden.1]\r\n    \r\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\r\n    para toda ys, preordenItAux i ys = preorden i ++ ys\r\n    para toda ys, preordenItAux d ys = preorden d ++ ys\r\n Hay que demostrar que\r\n    para toda ys, preordenItAux (Nodo x i d) ys = preorden (Nodo x i d) ++ ys\r\n En efecto,\r\n    preordenItAux (Nodo x i d) ys\r\n    = x : (preordenItAux i (preordenItAux d ys))   [por preordenItAux.2]\r\n    = x : (preordenItAux i (preorden d ++ ys))     [por hip. de inducci\u00f3n]\r\n    = x : (preorden i ++ (preorden d ++ ys))       [por hip. de inducci\u00f3n]\r\n    = ([x] ++ preorden i ++ preorden d) ++ ys      [por prop. de listas]\r\n    = preorden (Nodo x i d) ++ ys                  [por preorden.2]\r\n-}\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En las clases de ayer y hoy Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas hemos comentado las soluciones de la relaci\u00f3n 31 en la que se plantean ejercicios de demostraci\u00f3n por inducci\u00f3n de propiedades de programas. En concreto, la suma de los n primeros impares es n^2, 1 + 2^0 + 2^1 + 2^2 +&#8230;<\/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":[1],"tags":[270,298],"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\/3660"}],"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=3660"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3660\/revisions"}],"predecessor-version":[{"id":3662,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3660\/revisions\/3662"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3660"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3660"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3660"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}