Tema 8: Razonamiento sobre programas

Librería auxiliares

import Test.QuickCheck
import Test.QuickCheck.Function

1 Razonamiento ecuacional

1.1 Cálculo con longitud

longitud []     = 0                 -- longitud.1
longitud (_:xs) = 1 + longitud xs   -- longitud.2
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

1.2 Propiedad de intercambia

intercambia :: (a,b) -> (b,a)
intercambia (x,y) = (y,x)       -- intercambia
intercambia (intercambia (x,y)) = (x,y)
intercambia (intercambia (x,y))
= intercambia (y,x)      [por intercambia] 
= (x,y)                  [por intercambia]
prop_intercambia :: Eq a => a -> a -> Bool
prop_intercambia x y = 
    intercambia (intercambia (x,y)) == (x,y)
ghci> quickCheck prop_intercambia
+++ OK, passed 100 tests.

1.3 Inversa de listas unitarias

inversa :: [a] -> [a]
inversa []     = []                  -- inversa.1
inversa (x:xs) = inversa xs ++ [x]   -- inversa.2
inversa [x] 
= inversa (x:[])      [notación de lista] 
= (inversa []) ++ [x] [inversa.2] 
= [] ++ [x]           [inversa.1] 
= [x]                 [def. de ++] 
prop_inversa_unitaria :: Eq a => a -> Bool
prop_inversa_unitaria x =
    inversa [x] == [x]
ghci> quickCheck prop_inversa_unitaria
+++ OK, passed 100 tests.

1.4 Razonamiento ecuacional con análisis de casos

not :: Bool -> Bool
not False = True
not True  = False
not (not True) 
= not False      [not.2] 
= True           [not.1]
not (not False) 
= not True      [not.1] 
= False         [not.2]  
prop_doble_negacion :: Bool -> Bool
prop_doble_negacion x =
  not (not x) == x
ghci> quickCheck prop_doble_negacion
+++ OK, passed 100 tests.

2 Razonamiento por inducción sobre los naturales

2.1 Esquema de inducción sobre los naturales

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

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

2.2 Ejemplo de inducción sobre los naturales

replicate 3 5  ==  [5,5,5]  
replicate :: Int -> a -> [a]
replicate 0 _ = []
replicate n x = x : replicate (n-1) x
length (replicate 0 x) 
= length []            [por replicate.1]
= 0                    [por def. length]
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 +]
prop_length_replicate :: Int -> Int -> Bool
prop_length_replicate n xs =
    length (replicate m xs) == m
    where m = abs n
ghci> quickCheck prop_length_replicate
OK, passed 100 tests.

3 Razonamiento por inducción sobre listas

3.1 Esquema de inducción sobre listas

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

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

3.2 Asociatividad de ++

(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys             -- ++.1
(x:xs) ++ ys = x : (xs ++ ys) -- ++.2
prop_asociativa_conc :: [Int] -> [Int] -> [Int] -> Bool
prop_asociativa_conc xs ys zs = 
    xs ++ (ys ++ zs)==(xs ++ ys) ++ zs
ghci> quickCheck prop_asociatividad_conc
OK, passed 100 tests.
xs ++ (ys ++ zs) 
= [] ++ (ys ++ zs)   [por hipótesis] 
= ys ++ zs           [por  ++ .1]
= ([] ++ ys) ++ zs   [por  ++ .1]
= (xs ++ ys) ++ zs   [por hipótesis] 
(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] 

3.3 [] es la identidad para ++ por la derecha

prop_identidad_concatenacion :: [Int] -> Bool
prop_identidad_concatenacion xs = xs ++ [] == xs  
ghci> quickCheck prop_identidad_concatenacion
OK, passed 100 tests.
xs ++ [] 
= [] ++ [] 
= []         [por ++.1] 
(a:as) ++ [] 
= a:(as ++ [])   [por ++.2] 
= a:as           [por hip. ind.]

3.4 Relación entre 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
prop_length_append :: [Int] -> [Int] -> Bool
prop_length_append xs ys = 
   length(xs ++ ys)==(length xs)+(length ys) 
ghci> quickCheck prop_length_append
OK, passed 100 tests.
length([] ++ ys)
= length ys                [por ++.1] 
= 0+(length ys)            [por aritmética] 
= (length [])+(length ys)  [por length.1]
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]

3.5 Relación entre take y drop

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
prop_take_drop :: Int -> [Int] -> Property
prop_take_drop n xs = 
    n >= 0 ==> take n xs ++ drop n xs == xs
ghci> quickCheck prop_take_drop
OK, passed 100 tests.
take 0 xs ++ drop 0 xs 
= [] ++ xs              [por take.1 y drop.1] 
= xs                    [por ++.1]
take (m+1) [] ++ drop (m+1) [] 
= [] ++ []                        [por take.2 y drop.2]
= []                              [por ++.1]
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]

3.6 La concatenación de listas vacías es vacía

null :: [a] -> Bool
null []           = True            -- null.1
null (_:_)        = False           -- null.2

(++) :: [a] -> [a] -> [a]
[]     ++ ys      = ys              -- (++).1
(x:xs) ++ ys      = x : (xs ++ ys)  -- (++).2
null xs 
= null []          [por hipótesis] 
= True             [por null.1] 

null (xs ++ xs) 
= null ([] ++ [])  [por hipótesis]
= null []          [por (++).1]
= True             [por null.1] 
null xs 
= null (y:ys)              [por hipótesis] 
= False                    [por null.2

null (xs ++ xs) 
= null ((y:ys) ++ (y:ys))  [por hipótesis]
= null (y:(ys ++ (y:ys))   [por (++).2]
= False                    [por null.2

4 Equivalencia de funciones

inversa1, inversa2 :: [a] -> [a]
inversa1 []     = []                                      -- inversa1.1
inversa1 (x:xs) = inversa1 xs ++ [x]                      -- inversa1.2

inversa2 xs = inversa2Aux xs []                           -- inversa2.1
    where inversa2Aux []     ys = ys                      -- inversa2Aux.1
          inversa2Aux (x:xs) ys = inversa2Aux xs (x:ys)   -- inversa2Aux.2
prop_equiv_inversa :: [Int] -> Bool
prop_equiv_inversa xs = inversa1 xs == inversa2 xs
inversa1 xs 
= inversa1 xs ++ []     [por identidad de ++] 
= inversa2Aux xs ++ []  [por el lema] 
= inversa2 xs           [por el inversa2.1] 
inversa1 [] ++ ys
= [] ++ ys              [por inversa1.1] 
= ys                    [por ++.1] 
= inversa2Aux [] ys     [por inversa2Aux.1]
inversa1 (a:as) ++ ys
= (inversa1 as ++ [a]) ++ ys    [por inversa1.2] 
= (inversa1 as) ++ ([a] ++ ys)  [por asociativa de ++]
= (inversa1 as) ++ (a:ys)       [por ley unitaria] 
= (inversa2Aux as (a:ys)        [por hip. de inducción] 
= inversa2Aux (a:as) ys         [por inversa2Aux.2]

5 Propiedades de funciones de orden superior

Relación entre sum y map

sum :: [Int] -> Int
sum []     = 0                
sum (x:xs) = x + sum xs       
prop_sum_map :: [Int] -> Bool
prop_sum_map xs = sum (map (2*) xs) == 2 * sum xs
ghci> quickCheck prop_sum_map
+++ OK, passed 100 tests.
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] 
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]

Comprobación de propiedades con argumentos funcionales

prop_map_length (Fun _ f) xs =
    length (map f xs) == length xs
import Test.QuickCheck.Function

6 Bibliografía



Universidad de Sevilla

José A. Alonso Jiménez
Grupo de Lógica Computacional
Dpto. de Ciencias de la Computación e I.A.
Universidad de Sevilla