Tema 19: El tipo abstracto de los árboles binarios de búsqueda

Cabecera del módulo:

module Tema_19.ArbolBin
  (ABB,
   vacio,      -- ABB
   inserta,    -- (Ord a, Show a) => a -> ABB a -> ABB a
   elimina,    -- (Ord a, Show a) => a -> ABB a -> ABB a
   crea,       -- (Ord a, Show a) => [a] -> ABB a
   crea',      -- (Ord a, Show a) => [a] -> ABB a
   menor,      -- Ord a => ABB a -> a
   elementos,  -- (Ord a, Show a) => ABB a -> [a]
   pertenece,  -- (Ord a, Show a) => a -> ABB a -> Bool
   valido,     -- (Ord a, Show a) => ABB a -> Bool
   escribeABB, -- Show a => ABB a -> String
   ejemploABB  -- Int -> ABB Int
  ) where

Los ABB como tipo de dato algebraico.

data Ord a => ABB a = Vacio
                    | Nodo a (ABB a) (ABB a)
  deriving (Show, Eq)

(escribeABB a) es la cadena correspondiente al ABB a. Por ejemplo,

λ> escribeABB (crea (reverse [5,2,6,4,8,3,9]))
" (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))"
λ> escribeABB (foldr inserta vacio (reverse [5,2,4,3,8,6,7,10,9,11]))
" (5 (2 - (4 (3 - -) -)) (8 (6 - (7 - -)) (10 (9 - -) (11 - -))))"

Su definición es

escribeABB :: Show a => ABB a -> String
escribeABB Vacio        = " -"
escribeABB (Nodo x i d) = " (" ++ show x ++ escribeABB i ++ escribeABB d ++ ")"

Procedimiento de escritura de ABB.

instance Show a => Show (ABB a) where
  show = escribeABB

Ejemplos de ABB

λ> ejemploABB 1
 (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))
λ> ejemploABB 2
 (5 (2 - (4 (3 - -) -)) (8 (6 - (7 - -)) (10 (9 - -) (11 - -))))

Su definición es

ejemploABB :: Int -> ABB Int
ejemploABB 1 = crea (reverse [5,2,6,4,8,3,9])
ejemploABB 2 = foldr inserta vacio (reverse [5,2,4,3,8,6,7,10,9,11])
ejemploABB _ = error "No definido"

vacio es el ABB vacío. Por ejemplo,

λ> vacio
 -

Su definición es

vacio :: ABB a
vacio = Vacio

(pertenece v a) se verifica si v es el valor de algún nodo del ABB a. Por ejemplo,

pertenece 3 (ejemploABB 1)  ==  True
pertenece 7 (ejemploABB 1)  ==  False

Su definición es

pertenece :: (Ord a, Show a) => a -> ABB a -> Bool
pertenece v' Vacio        = False
pertenece v' (Nodo v i d) | v' == v = True
                          | v' <  v = pertenece v' i
                          | v' >  v = pertenece v' d

(inserta v a) es el árbol obtenido añadiendo el valor v al ABB a, si no es uno de sus valores. Por ejemplo,

λ> inserta 7 (ejemploABB 1)
 (5 (2 - (4 (3 - -) -)) (6 - (8 (7 - -) (9 - -))))

Su definición es

inserta :: (Ord a, Show a) => a -> ABB a -> ABB a
inserta v' Vacio        = Nodo v' Vacio Vacio
inserta v' (Nodo v i d) | v' == v   = Nodo v i d
                        | v' <  v   = Nodo v (inserta v' i) d
                        | otherwise = Nodo v i (inserta v' d)

(crea vs) es el ABB cuyos valores son vs. Por ejemplo

λ> crea [3,7,2]
 (2 - (7 (3 - -) -))

Su definición es

crea :: (Ord a, Show a) => [a] -> ABB a
crea = foldr inserta Vacio

(crea' vs) es el ABB de menor profundidad cuyos valores son los de la lista ordenada vs. Por ejemplo,

λ> crea' [2,3,7]
(~3 (2 ~-~ -) (7 -~ ~-)) ~~~

Su definición es

crea' :: (Ord a, Show a) => [a] -> ABB a
crea' [] = Vacio
crea' vs = Nodo x (crea' l1) (crea' l2)
  where n      = length vs `div` 2
        l1     = take n vs
        (x:l2) = drop n vs

(elementos a) es la lista de los valores de los nodos del ABB a en el recorrido inorden. Por ejemplo,

elementos (ejemploABB 1)  ==  [2,3,4,5,6,8,9]
elementos (ejemploABB 2)  ==  [2,3,4,5,6,7,8,9,10,11]

Su definición es

elementos :: (Ord a, Show a) => ABB a -> [a]
elementos Vacio        = []
elementos (Nodo v i d) = elementos i ++ [v] ++ elementos d

(elimina v a) el ABB obtenido eliminando el valor v del ABB a. Por ejemplo,

λ> elimina 3 (ejemploABB 1)
λ> (ejemploABB 1)
 (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))
λ> elimina 3 (ejemploABB 1)
 (5 (2 - (4 - -)) (6 - (8 - (9 - -))))
λ> elimina 2 (ejemploABB 1)
 (5 (4 (3 - -) -) (6 - (8 - (9 - -))))
λ> elimina 5 (ejemploABB 1)
 (6 (2 - (4 (3 - -) -)) (8 - (9 - -)))
λ> elimina 7 (ejemploABB 1)
 (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))

Su definición es

elimina  :: (Ord a, Show a) => a -> ABB a -> ABB a
elimina _  Vacio = Vacio
elimina v' (Nodo v i Vacio) | v'==v = i
elimina v' (Nodo v Vacio d) | v'==v = d
elimina v' (Nodo v i d)     | v' < v    = Nodo v (elimina v' i) d
                            | v' > v    = Nodo v i (elimina v' d)
                            | otherwise = Nodo k i (elimina k d)
  where k = menor d

(menor a) es el mínimo valor del ABB a. Por ejemplo,

menor (ejemploABB 1)  ==  2

Su definición es

menor :: Ord a => ABB a -> a
menor (Nodo v Vacio _) = v
menor (Nodo _ i     _) = menor i

(menorTodos v a) se verifica si v es menor que todos los elementos del ABB a.

menorTodos :: (Ord a, Show a) => a -> ABB a -> Bool
menorTodos v Vacio = True
menorTodos v a     = v < minimum (elementos a)

(mayorTodos v a) se verifica si v es mayor que todos los elementos del ABB a.

mayorTodos :: (Ord a, Show a) => a -> ABB a -> Bool
mayorTodos v Vacio = True
mayorTodos v a     = v > maximum (elementos a)

(valido a) se verifica si a es un ABB correcto. Por ejemplo,

valido (ejemploABB 1) == True

Su definición es

valido :: (Ord a, Show a) => ABB a -> Bool
valido Vacio        = True
valido (Nodo v i d) = mayorTodos v i &&
                      menorTodos v d &&
                      valido i &&
                      valido d

Al principio del fichero se añade

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

Importación de la implementación de los ABB que se desea verificar.

import Tema_19.ArbolBin
-- import I1M.ArbolBin

Importación de librerías auxiliares.

import Data.List (nub, sort)
import Test.QuickCheck

genABB es un generador de árboles binarios de búsqueda. Por ejemplo,

λ> sample genABB
 -
 (1 (-1 - -) -)
 (1 - -)
 (-1 (-3 - -) (1 - (4 - -)))

Su definición es

genABB :: Gen (ABB Int)
genABB = do
  xs <- listOf arbitrary
  return (foldr inserta vacio xs)

instance Arbitrary (ABB Int) where
  arbitrary = genABB

Propiedad. Todo los elementos generados por genABB son árboles binarios de búsqueda.

prop_genABB_correcto :: ABB Int -> Bool
prop_genABB_correcto = valido

listaOrdenada es un generador de listas ordenadas de números enteros. Por ejemplo,

λ> sample listaOrdenada
[1]
[-2,-1,0]

Su definición es

listaOrdenada :: Gen [Int]
listaOrdenada =
  frequency [(1,return []),
             (4,do xs <- orderedList
                   n <- arbitrary
                   return (nub ((case xs of
                                   []  -> n
                                   x:_ -> n `min` x)
                                :xs)))]

(ordenada xs) se verifica si xs es una lista ordenada creciente. Por ejemplo,

ordenada [3,5,9]  ==  True
ordenada [3,9,5]  ==  False

Su definición es

ordenada :: [Int] -> Bool
ordenada xs = and [x < y | (x,y) <- zip xs (tail xs)]

Propiedad. El generador listaOrdenada produce listas ordenadas.

prop_listaOrdenada_correcta :: [Int] -> Property
prop_listaOrdenada_correcta xs =
  forAll listaOrdenada ordenada

vacio es un ABB.

prop_vacio_es_ABB :: Bool
prop_vacio_es_ABB =
  valido (vacio :: ABB Int)

Si a es un ABB, entonces (inserta v a) también lo es.

prop_inserta_es_valida :: Int -> ABB Int -> Bool
prop_inserta_es_valida v a =
  valido (inserta v a)

El árbol que resulta de añadir un elemento a un ABB es no vacío.

prop_inserta_es_no_vacio :: Int -> ABB Int -> Bool
prop_inserta_es_no_vacio x a =
  inserta x a /= vacio

Para todo x y a, x es un elemento de (inserta x a).

prop_elemento_de_inserta :: Int -> ABB Int -> Bool
prop_elemento_de_inserta x a =
  pertenece x (inserta x a)

En un árbol vacio no hay ningún elemento.

prop_vacio_sin_elementos :: Int -> Bool
prop_vacio_sin_elementos x =
  not (pertenece x vacio)

Los elementos de (inserta x a) son x y los elementos de a.

prop_elementos_de_inserta :: Int -> Int -> ABB Int -> Bool
prop_elementos_de_inserta x y a =
  pertenece y (inserta x a)
  == (x == y) || pertenece y a

Si a es un ABB, entonces (elimina v a) también lo es.

prop_elimina_es_valida :: Int -> ABB Int -> Bool
prop_elimina_es_valida v a =
  valido (elimina v a)

El resultado de eliminar el elemento x en (inserta x a) es (elimina x a).

prop_elimina_agrega :: Int -> ABB Int -> Bool
prop_elimina_agrega x a =
  elimina (inserta x a) == elimina x a

(crea xs) es un ABB.

prop_crea_es_valida :: [Int] -> Bool
prop_crea_es_valida xs =
  valido (crea xs)

Para todas las listas ordenadas xs, se tiene que (crea' xs) es un ABB.

prop_crea'_es_valida :: [Int] -> Property
prop_crea'_es_valida xs =
  forAll listaOrdenada (valido . crea')

(elementos (crea xs)) es igual a la lista xs ordenada y sin repeticiones.

prop_elementos_crea :: [Int] -> Bool
prop_elementos_crea xs =
  elementos (crea xs) == sort (nub xs)

Si ys es una lista ordenada sin repeticiones, entonces (elementos (crea' ys)) es igual ys.

prop_elementos_crea' :: [Int] -> Bool
prop_elementos_crea' xs =
  elementos (crea' ys) == ys
  where ys = sort (nub xs)

Un elemento pertenece a (elementos a) syss es un valor de a.

prop_en_elementos :: Int -> ABB Int -> Bool
prop_en_elementos v a =
  pertenece v a == elem v (elementos a)

(menor a) es menor o igual que todos los elementos de ABB a.

prop_menoresMinimo ::Int -> ABB Int -> Bool
prop_menoresMinimo v a =
  and [menor a <= v | v <- elementos a]

Para verificar todas las propiedades se escribe

return []

verificaABB :: IO Bool
verificaABB = $quickCheckAll

Comprobación de las propiedades de los ABB

λ> verificaABB
=== prop_genABB_correcto from ArbolBinPropiedades.hs:44 ===
+++ OK, passed 100 tests.

=== prop_listaOrdenada_correcta from ArbolBinPropiedades.hs:83 ===
+++ OK, passed 100 tests.

=== prop_orderedList_correcta from ArbolBinPropiedades.hs:93 ===
+++ OK, passed 100 tests.

=== prop_vacio_es_ABB from ArbolBinPropiedades.hs:109 ===
+++ OK, passed 1 test.

=== prop_inserta_es_valida from ArbolBinPropiedades.hs:121 ===
+++ OK, passed 100 tests.

=== prop_inserta_es_no_vacio from ArbolBinPropiedades.hs:131 ===
+++ OK, passed 100 tests.

=== prop_elemento_de_inserta from ArbolBinPropiedades.hs:140 ===
+++ OK, passed 100 tests.

=== prop_vacio_sin_elementos from ArbolBinPropiedades.hs:152 ===
+++ OK, passed 100 tests.

=== prop_elementos_de_inserta from ArbolBinPropiedades.hs:162 ===
+++ OK, passed 100 tests.

=== prop_elimina_es_valida from ArbolBinPropiedades.hs:174 ===
+++ OK, passed 100 tests.

=== prop_elimina_agrega from ArbolBinPropiedades.hs:184 ===
+++ OK, passed 100 tests.

=== prop_crea_es_valida from ArbolBinPropiedades.hs:196 ===
+++ OK, passed 100 tests.

=== prop_crea'_es_valida from ArbolBinPropiedades.hs:209 ===
+++ OK, passed 100 tests.

=== prop_elementos_crea from ArbolBinPropiedades.hs:222 ===
+++ OK, passed 100 tests.

=== prop_elementos_crea' from ArbolBinPropiedades.hs:232 ===
+++ OK, passed 100 tests.

=== prop_en_elementos from ArbolBinPropiedades.hs:242 ===
+++ OK, passed 100 tests.

=== prop_menoresMinimo from ArbolBinPropiedades.hs:255 ===
+++ OK, passed 100 tests.

True