Librería auxiliares
import Test.QuickCheck
import Test.QuickCheck.Function
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
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.
inversa :: [a] -> [a]
inversa [] = [] -- inversa.1
inversa (x:xs) = inversa xs ++ [x] -- inversa.2
inversa [x] = [x]
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.
not :: Bool -> Bool
not False = True
not True = False
Prop.: not (not x) = x
Demostración por casos: Caso 1: x = True
:
not (not True)
= not False [not.2]
= True [not.1]
x = False
: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.
Para demostrar que todos los números naturales tienen una propiedad P
basta probar:
n=0
: P(0)
.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]
replicate :: Int -> a -> [a]
replicate 0 _ = []
replicate n x = x : replicate (n-1) x
Prop.: length (replicate n x) = n
Demostracion del caso base (n=0
):
length (replicate 0 x)
= length [] [por replicate.1]
= 0 [por def. length]
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 +]
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.
Para demostrar que todas las listas finitas tienen una propiedad P
basta probar:
xs=[]
: P([])
.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.
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys -- ++.1
(x:xs) ++ ys = x : (xs ++ ys) -- ++.2
Propiedad: xs ++ (ys ++ zs)=(xs ++ ys) ++ zs
Especificación con QuickCheck:
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.
Demostración por inducción en xs
:
Caso base xs=[]
: Reduciendo el lado izquierdo
xs ++ (ys ++ zs)
= [] ++ (ys ++ zs) [por hipótesis]
= ys ++ zs [por ++ .1]
= ([] ++ ys) ++ zs [por ++ .1]
= (xs ++ ys) ++ zs [por hipótesis]
xs = a:as
: Suponiendo la hipótesis de inducciónas ++ (ys ++ zs) = (as ++ ys) ++ zs
(a:as) ++ (ys ++ zs) = ((a:as) ++ ys) ++ zs
(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
Especificación con QuickCheck:
prop_identidad_concatenacion :: [Int] -> Bool
prop_identidad_concatenacion xs = xs ++ [] == xs
ghci> quickCheck prop_identidad_concatenacion
OK, passed 100 tests.
Demostración por inducción en xs
:
Caso base xs = []
:
xs ++ []
= [] ++ []
= [] [por ++.1]
xs = a:as
: Suponiendo la hipótesis de inducciónas ++ [] = as
(a:as) ++ []=(a:as)
(a:as) ++ []
= a:(as ++ []) [por ++.2]
= a:as [por hip. ind.]
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)
Especificación con QuickCheck:
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.
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]
xs = a:as
: Suponiendo la hipótesis de inducciónlength(as ++ ys) = (length as)+(length ys)
length((a:as) ++ ys) = (length (a:as))+(length ys)
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]
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
Especificación con QuickCheck:
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.
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
take m xs ++ drop m xs = xs
hay que demostrar que
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]
xs = a:as
: Suponiendo la hip. de inducción 2take (m+1) as ++ drop (m+1) as = as
take (m+1) (a:as) ++ drop (m+1) (a:as) = (a:as)
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]
null :: [a] -> Bool
null [] = True -- null.1
null (_:_) = False -- null.2
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys -- (++).1
(x:xs) ++ ys = x : (xs ++ ys) -- (++).2
Propiedad: null xs = null (xs ++ xs)
.
Demostración por inducción en xs
:
Caso 1: xs = []
: Reduciendo ambos lados:
null xs
= null [] [por hipótesis]
= True [por null.1]
null (xs ++ xs)
= null ([] ++ []) [por hipótesis]
= null [] [por (++).1]
= True [por null.1]
xs = y:ys
: Reduciendo ambos lados: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
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
Propiedad: inversa1 xs = inversa2 xs
Especificación con QuickCheck:
prop_equiv_inversa :: [Int] -> Bool
prop_equiv_inversa xs = inversa1 xs == inversa2 xs
inversa1 xs ++ ys = inversa2Aux xs ys
inversa1 xs
= inversa1 xs ++ [] [por identidad de ++]
= inversa2Aux xs ++ [] [por el lema]
= inversa2 xs [por el inversa2.1]
Demostración del lema: Por inducción en xs
:
Caso base xs = []
:
inversa1 [] ++ ys
= [] ++ ys [por inversa1.1]
= ys [por ++.1]
= inversa2Aux [] ys [por inversa2Aux.1]
xs=(a:as)
: La hipótesis de inducción esinversa1 as ++ ys = inversa2Aux as ys
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]
Relación entre sum y map
sum
:sum :: [Int] -> Int
sum [] = 0
sum (x:xs) = x + sum xs
Propiedad: sum (map (2*) xs) = 2 * sum xs
Especificación con QuickCheck:
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.
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]
xs = y:ys
: Entonces,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
Comprobación
ghci> quickCheck prop_map_length
+++ OK, passed 100 tests.
H.C. Cunningham. Notes on Functional Programming with Haskell.
J. Fokker. Programación funcional.
E.P. Wentworth. Introduction to funcional programming.