Tema 8: Razonamiento sobre programas

• Definición de longitud

  longitud []     = 0                 -- longitud.1
  longitud (_:xs) = 1 + longitud xs   -- longitud.2
  

• Propiedad: longitud [2,3,1] = 3

• Demostración:

  longitud [2,3,1]
  = 1 + longitud [2,3]          [por longitud.2]
  = 1 + (1 + longitud [3])      [por longitud.2]
  = 1 + (1 + (1 + longitud [])) [por longitud.2]
  = 1 + (1 + (1 + 0)            [por longitud.1]
  = 3
  

• Definición de intercambia:

  intercambia :: (a,b) -> (b,a)
  intercambia (x,y) = (y,x)       -- intercambia
  

• Propiedad: intercambia (intercambia (x,y)) = (x,y)

• Demostración:

  intercambia (intercambia (x,y))
  = intercambia (y,x)      [por intercambia]
  = (x,y)                  [por intercambia]
  

• Propiedad en QuickCheck:

  prop_intercambia :: Eq a => a -> a -> Bool
  prop_intercambia x y = intercambia (intercambia (x,y)) == (x,y)
  

• Comprobación:

  λ> quickCheck prop_intercambia
  +++ OK, passed 100 tests.
  

• Nota: Para usar la librería QuickCheck hay que importarla escribiendo al principio del fichero

  import Test.QuickCheck
  

• Inversa de una lista:

  inversa :: [a] -> [a]
  inversa []     = []                  -- inversa.1
  inversa (x:xs) = inversa xs ++ [x]   -- inversa.2
  

• Propiedad: inversa [x] = [x]

  inversa [x]
  = inversa (x:[])      [notación de lista]
  = (inversa []) ++ [x] [inversa.2]
  = [] ++ [x]           [inversa.1]
  = [x]                 [def. de ++]
  

• Propiedad en QuickCheck:

  prop_inversa_unitaria :: Eq a => a -> Bool
  prop_inversa_unitaria x = inversa [x] == [x]
  

• Comprobación:

  λ> quickCheck prop_inversa_unitaria
  +++ OK, passed 100 tests.
  

Para demostrar que todos los números naturales tienen una propiedad P basta probar:

• Caso base n=0: P(0).
• Caso inductivo n=(m+1): Suponiendo P(m) demostrar P(m+1).

En el caso inductivo, la propiedad P(n) se llama la hipótesis de inducción.

• (replicate n x) es la lista formda por n elementos iguales a x. Por ejemplo,

  replicate 3 5  ==  [5,5,5]
  

  Su definición es

  replicate :: Int -> a -> [a]
  replicate 0 _ = []
  replicate n x = x : replicate (n-1) x
  

• Prop.: length (replicate n x) = n
• Demostración por inducción en n:

  • Caso base (n=0):

    length (replicate 0 x)
    = length []            [por replicate.1]
    = 0                    [por def. length]
    

  • Caso inductivo (n=m+1):

    length (replicate (m+1) x)
    = length (x:(replicate m x))  [por replicate.2]
    = 1 + length (replicate m x)  [por def. length]
    = 1 + m                       [por hip. ind.]
    = m + 1                       [por conmutativa de +]
    

• Propiedad en QuickCheck:

  prop_length_replicate :: Int -> Int -> Bool
  prop_length_replicate n xs =
    length (replicate m xs) == m
    where m = abs n
  

• Comprobación de la propiedad:

  λ> quickCheck prop_length_replicate
  OK, passed 100 tests.
  

Para demostrar que todas las listas finitas tienen una propiedad P basta probar:

• Caso base xs=[]: P([]).
• Caso inductivo xs=(y:ys): Suponiendo P(ys) demostrar P(y:ys).

En el caso inductivo, la propiedad P(ys) se llama la hipótesis de inducción.

• Definición de ++:

  (++) :: [a] -> [a] -> [a]
  []     ++ ys = ys             -- ++.1
  (x:xs) ++ ys = x : (xs ++ ys) -- ++.2
  

• Propiedad:

  xs ++ (ys ++ zs)=(xs ++ ys) ++ zs
  

• Propiedad con QuickCheck:

  prop_asociativa_conc :: [Int] -> [Int] -> [Int] -> Bool
  prop_asociativa_conc xs ys zs =
      xs ++ (ys ++ zs)==(xs ++ ys) ++ zs
  

• Comprobación:

  λ> quickCheck prop_asociatividad_conc
  OK, passed 100 tests.
  

• Demostración por inducción en xs:

  • Caso base xs = []:

    xs ++ (ys ++ zs)
    = [] ++ (ys ++ zs)   [por hipótesis]
    = ys ++ zs           [por  ++ .1]
    = ([] ++ ys) ++ zs   [por  ++ .1]
    = (xs ++ ys) ++ zs   [por hipótesis]
    

  • Caso inductivo xs = a:as: Suponiendo la hipótesis de inducción

    as ++ (ys ++ zs) = (as ++ ys) ++ zs
    

    hay que demostrar que

    (a:as) ++ (ys ++ zs) = ((a:as) ++ ys) ++ zs
    

    La demostración es

    (a:as) ++ (ys ++ zs)
    = a:(as ++ (ys ++ zs))  [por  ++ .2]
    = a:((as ++ ys) ++ zs)  [por hip. ind.]
    = (a:(as ++ ys)) ++ zs  [por ++.2]
    = ((a:as) ++ ys) ++ zs  [por ++.2]
    

• Propiedad: xs ++ []=xs

• Propiedad con QuickCheck:

  prop_identidad_concatenacion :: [Int] -> Bool
  prop_identidad_concatenacion xs = xs ++ [] == xs
  

• Comprobación:

  λ> quickCheck prop_identidad_concatenacion
  OK, passed 100 tests.
  

• Demostración por inducción en xs:

  • Caso base xs = []:

    xs ++ []
    = [] ++ []
    = []         [por ++.1]
    

  • Caso inductivo xs = a:as: Suponiendo la hipótesis de inducción

    as ++ [] = as
    

    hay que demostrar que

    (a:as) ++ [] = (a:as)
    

    La demostración es

    (a:as) ++ []
    = a:(as ++ [])   [por ++.2]
    = a:as           [por hip. ind.]
    

• Definiciones de length y ++:

  length :: [a] -> Int
  length []     = 0                 -- length.1
  length (x:xs) = 1 + n_length xs   -- length.2
  
  (++) :: [a] -> [a] -> [a]
  []     ++ ys = ys                 -- ++.1
  (x:xs) ++ ys = x : (xs ++ ys)     -- ++.2
  

• Propiedad: length(xs ++ ys) = (length xs)+(length ys)

• Propiedad con QuickCheck:

  prop_length_append :: [Int] -> [Int] -> Bool
  prop_length_append xs ys =
     length(xs ++ ys)==(length xs)+(length ys)
  

• Comprobación:

  λ> quickCheck prop_length_append
  OK, passed 100 tests.
  

• Demostración por inducción en xs:

  • Caso base xs = []:

    length([] ++ ys)
    = length ys                [por ++.1]
    = 0+(length ys)            [por aritmética]
    = (length [])+(length ys)  [por length.1]
    

  • Caso inductivo xs = a:as: Suponiendo la hipótesis de inducción

    length(as ++ ys) = (length as)+(length ys)
    

    hay que demostrar que

    length((a:as) ++ ys) = (length (a:as))+(length ys)
    

    La demostración es

    length((a:as) ++ ys)
    = length(a:(as ++ ys))              [por ++.2]
    = 1 + length(as ++ ys)              [por length.2]
    = 1 + ((length as) + (length ys))   [por hip. ind.]
    = (1 + (length as)) + (length ys)   [por aritmética]
    = (length (a:as)) + (length ys)     [por length.2]
    

• Definición de take, drop y (++):

  take :: Int -> [a] -> [a]
  take 0 _       = []                  -- take.1
  take _ []      = []                  -- take.2
  take n (x:xs)  = x : take (n-1) xs   -- take.3
  
  drop :: Int -> [a] -> [a]
  drop 0 xs      = xs                  -- drop.1
  drop _ []      = []                  -- drop,2
  drop n (_:xs)  = drop (n-1) xs       -- drop.3
  
  (++) :: [a] -> [a] -> [a]
  []     ++ ys = ys                    -- ++.1
  (x:xs) ++ ys = x : (xs ++ ys)        -- ++.2
  

• Propiedad: take n xs ++ drop n xs = xs

• Propiedad con QuickCheck:

  prop_take_drop :: Int -> [Int] -> Property
  prop_take_drop n xs =
    n >= 0 ==> take n xs ++ drop n xs == xs
  

• Comprobación:

  λ> quickCheck prop_take_drop
  OK, passed 100 tests.
  

• Demostración por inducción en n:

  • Caso base n = 0:

    take 0 xs ++ drop 0 xs
    = [] ++ xs              [por take.1 y drop.1]
    = xs                    [por ++.1]
    

• Caso inductivo n = m+1: Suponiendo la hipótesis de inducción 1

  (∀ xs :: [a]) take m xs ++ drop m xs = xs
  

  hay que demostrar que

  (∀ xs :: [a]) take (m+1) xs ++ drop (m+1) xs = xs
  

  Lo demostraremos por inducción en xs:

  • Caso base xs = []:

    take (m+1) [] ++ drop (m+1) []
    = [] ++ []                        [por take.2 y drop.2]
    = []                              [por ++.1]
    

  • Caso inductivo xs = a:as: Suponiendo la hip. de inducción 2

    take (m+1) as ++ drop (m+1) as = as
    

    hay que demostrar que

    take (m+1) (a:as) ++ drop (m+1) (a:as) = (a:as)
    

    Demostración

    take (m+1) (a:as) ++ drop (m+1) (a:as)
    = (a:(take m as)) ++ (drop m as)     [take.3 y drop.3]
    = (a:((take m as) ++ (drop m as))    [por ++.2]
    = a:as                               [por hip. de ind. 1]
    

• Definición de la función sum:

  sum :: [Int] -> Int
  sum []     = 0
  sum (x:xs) = x + sum xs
  

• Propiedad: sum (map (2*) xs) = 2 * sum xs

• Propiedad con QuickCheck:

  prop_sum_map :: [Int] -> Bool
  prop_sum_map xs = sum (map (2*) xs) == 2 * sum xs
  

• Comprobación:

  λ> quickCheck prop_sum_map
  +++ OK, passed 100 tests.
  

• Demostración de la propiedad por inducción en xs

  • Caso []:

    sum (map (2*) xs)
    = sum (map (2*) [])  [por hipótesis]
    = sum []             [por map.1]
    = 0                  [por sum.1]
    = 2 * 0              [por aritmética]
    = 2 * sum []         [por sum.1]
    = 2 * sum xs         [por hipótesis]
    

• Caso xs = y:ys:

  sum (map (2*) xs)
  = sum (map (2*) (y:ys))         [por hipótesis]
  = sum ((2*) y : (map (2*) ys))  [por map.2]
  = (2*) y + (sum (map (2*) ys))  [por sum.2]
  = (2*) y + (2 * sum ys)         [por hip. de inducción]
  = (2 * y) + (2 * sum ys)        [por (2*)]
  = 2 * (y + sum ys)              [por aritmética]
  = 2 * sum (y:ys)                [por sum.2]
  = 2 * sum xs                    [por hipótesis]
  

• La aplicación de una función a los elementos de una lista conserva su longitud:

  prop_map_length (Fun _ f) xs =
    length (map f xs) == length xs
  

• En el inicio del fichero hay que escribir

  import Test.QuickCheck.Function
  

• Comprobación

  λ> quickCheck prop_map_length
  +++ OK, passed 100 tests.