Estructuras II Práctica 4

Consultas:
Ej 5 :  (PREGUNTAR SI HACE FALTA HACER LAS CLAUSULAS CONDICIONALES DE TODO EL ARMADO DEL ARBOL)
Ej 9:   (DEBERÍAMOS PROBAR DE ANTEMANO QUE alturaAGT DEVUELVE LA ALTURA)
        (PROBAR QUE map (f (map g xs)) = map (f o g) xs)
Ej 10:  PROBAR QUE map f (x ++ y) = map f x ++ map f y
Ej 11:  DEMOSTRAR QUE (x:xs) ++ join xss = x:(xs ++ join xss)
        DEMOSTRAR TODOS LOS PASOS TURBIOS QUE USAMOS
Ej 12:  Segùn Rabasedas y las autoridades de la cátedra, el 12 y 13 no son ejercicios para demostrar formalmente. Demostrar "con palabras".
Ej 13:  Ìdem anterior.


-- Ejercicio 1

tad lista (A:Set) where
    import Bool
    nil : lista A
    cons : A -> lista A -> lista A
    null : lista A -> Bool
    head : lista A -> A
    tail : lista A -> lista A

Especificación algebraica:
null nil = True
null (cons x xs) = False
head (cons x xs) = x
tail (cons x xs) = xs

Especificación con modelo de secuencias:
nil = <>
cons x <x1, ..., xn> = <x, x1, ..., xn>
null <x1, ..., xn> = True si n = 0
null <x1, ..., xn> = False en otro caso
head <x1, ..., xn> = x1
tail <x1, x2, ..., xn> = <x2, ..., xn>

inL : lista A -> A -> Bool
inL nil x = False
inL (cons y ys) x = or (y == x) (inL ys x)

del : lista A -> A -> lista A
del nil x = nil
del (cons y ys) x = if (y == x) then (del ys x) else (cons y (del ys x))




-- Ejercicio 2

tad Pila (A:Set) where
    import Bool
    empty : Pila A
    push : A -> Pila A -> Pila A
    isEmpty : Pila A -> Bool
    top : Pila A -> A
    pop : Pila A -> Pila A

Especificación algebraica:
isEmpty empty = True
isEmpty (push x xs) = False
top (push x xs) = x
pop (push x xs) = xs

Especificación con modelo de secuencias:
empty = <>
push x <x1, ..., xn> = <x, x1, ..., xn>
isEmpty <x1, ..., xn> = True si x = 0
isEmpty <x1, ..., xn> = False en otro caso
top <x1, ..., xn> = x1
pop <x1, x2, ..., xn> = <x2, ..., xn>




-- Ejercicio 3

tad Conjunto (A:Set) where
    import Bool
    vacio : Conjunto A
    insertar : A -> Conjunto A -> Conjunto A
    borrar : A -> Conjunto A -> Conjunto A
    esVacio : Conjunto A -> Bool
    union : Conjunto A -> Conjunto A -> Conjunto A
    interseccion : Conjunto A -> Conjunto A -> Conjunto A
    resta : Conjunto A -> Conjunto A -> Conjunto A

Especificación algebraica:
insertar x (insertar y c) = insertar y (insertar x c)
insertar x (insertar x' c) = insertar x c si x = x'
borrar x vacio = vacio
borrar x (insertar x' c) = c si x = x'
borrar x (insertar y c) = (insertar y (borrar x c))
esVacio vacio = True
esVacio (insertar x c) = False
union vacio y = y
union (insertar x c) y = insertar x (union c y)
inC vacio x = False
inC (insertar y c) x = if y == x then True else inC c x
interseccion vacio y = vacio
interseccion (insertar x c) y = if (inC y x) then insertar x (interseccion c y) else interseccion c y
resta y vacio = y
resta y (insertar x c) = borrar x (resta y c)

Si agregáramos la función choose mencionada, habría una inconsistencia que haría que no se supiera qué tendría que devolver.




-- Ejercicio 4
Especificación algebraica:
tad PQ (A: Set, B: Ordered Set) where
    import Bool
poner (e, p) (poner (e', p') q) = poner (e', max (p, p')) si e = e'
poner (e, p) (poner (e', p') q) = poner (e', p') (poner (e, p) q) si e != e'
poner (e, p) (poner (e', p') q) = (poner (e', p') q) si p = p'

maxPQ (e, p) vacia = (e, p)
maxPQ (e, p) (poner (e', p') q) = if p > p' then (maxPQ (e, p) q) else (maxPQ (e', p') q)

primero (poner (e, p) q) = maxPQ (e, p) q

eliminar (e, p) (poner (e', p') q) = if e == e' then q else (poner (e', p') (eliminar (e, p) q))

sacar (poner (e, p) q) = eliminar primero(poner (e, p) q) (poner (e, p) q)

esVacia vacia = True
esVacia (poner (e, p) q) = False

union vacia q' = q'
union (poner (e, p) q) q' = union q (poner (e, p) q')


Especificación con modelo de conjuntos:
vacia = {}
poner (e, p) {(e1, p1), ..., (en, pn)} = {(e, p)} U {(e1, p1), ..., (en, pn)} si e != ei y p != pi para todo i en [1,n]
poner (e, p) {(e1, p1), ..., (en, pn)} = {(e, max(p, pi)} U {(e1, p1), ...,  (e(i-1), p(i-1)), (e(i+1), p(i+1)), ..., (en, pn)} si e = ei para algún i en [1,n]
poner (e, p) {(e1, p1), ..., (en, pn)} = {(e1, p1), ..., (en, pn)} si p = pi para algún i en [1,n]
primero {(e1, p1), ..., (en, pn)} = (e, p) si p >= pi para todo i en [1,n]
sacar Q = Q - {primero Q}
esVacia Q = if #Q = 0 then True else False
union {} Q' = Q'
union {(e1, p1), (e2, p2), ..., (en, pn)} Q' = poner (e1, p1) (union {(e2, p2), ..., (en, pn)} Q')




-- Ejercicio 5

size empty = 0
size (join L Nothing R) = size L + size R
size (join L (Just x) R) = 1 + size L + size R

case expose t where
  Nothing -> t = empty
  Just (l,x,r) -> t = join l (Just x) r



-- Ejercicio 6

(uncurry zip) o zip = id

Para ello hacemos inducción en el largo de la lista.

Para n = 0:
(uncurry zip) o zip L = uncurry zip (unzip L) = uncurry zip ([], []) = []

Para n > 0:
(uncurry zip) o zip L = uncurry zip (unzip ((x,y):ps)) = uncurry zip (x:xs, y:ys) where ... = (x,y):(uncurry zip (unzip ps)) = (x,y):ps

-- Ejercicio 7

sum xs <= length xs * maxl xs

Para ello hacemos inducción en el largo de la lista.

Para n = 0:
sum xs = 0 <= 0 * 0 = length xs * maxl xs

Para n > 0:
sum (x:xs) = x + sum xs <= x + length xs * maxl xs
length (x:xs) * maxl (x:xs) = (1 + length xs) * (max x (maxl xs)) (Exp 1)

Si x <= maxl xs:
    (Exp 1) = (1 + length xs) * (maxl xs) = (maxl xs) + (length xs) * (maxl xs) >= x + (length xs) * (maxl xs)
    >= x + sum xs = sum (x:xs)
Si x > maxl xs:
    (Exp 1) = (1 + length xs) * x = x + (length xs) * x >= x + (length xs) * (maxl xs) >= x + (sum xs) = sum (x:xs)


-- Ejercicio 8

size :: Arbol a -> Int
size Hoja n = 1
size (Nodo d l r) = 1 + size l + size r

Hacemos una sexy inducción estructural:

Caso t = Hoja n :
size t = 1 = 2 * 0 + 1

Caso t = (Nodo d l r):
size t = 1 + size l + size r = 1 + 2 k' + 1 + 2 k'' + 1 = 2k' + 2k'' + 2 + 1 = 2(k' + k'' + 1) + 1

mirror :: Arbol a -> Arbol a
mirror Hoja n = Hoja n
mirror (Nodo d l r) = Nodo d (mirror r) (mirror l)

Hacemos una sexy inducción estructural (Again):
Caso t = Hoja n :
mirror (mirror t) = mirror t = t

Caso t = (Nodo d l r):
mirror (mirror t) = mirror (Nodo d (mirror r) (mirror l)) = Nodo d (mirror (mirror l)) (mirror (mirror r)) =
Nodo d l r

Hacemos una sexy inducción estructural (Yet again):
Caso t = Hoja n :
hojas t = 1 < 2 = 2 ^ 1 = 2 ^ (altura t)

Caso t = (Nodo d l r):
hojas t = (hojas l) + (hojas r) < 2 ^ (altura l) + 2 ^ (altura r) <= 2 ^ (max (altura l) (altura r)) + 2 ^ (max (altura l) (altura r)) =
= 2 * 2 ^ (max (altura l) (altura r)) = 2 ^ (1 + (max (altura l) (altura r))) = 2 ^ (altura t)


-- Ejercicio 9

alturaAGT :: AGTree a -> Int
alturaAGT (Node d []) = 1
alturaAGT (Node d (x:xs)) = 1 + (maxl (map alturaAGT (x:xs)))

maxAGT :: Ord a => AGTree a -> a
maxAGT (Node d []) = d
maxAGT (Node d (x:xs)) = max (d (maxl (map maxAGT (x:xs)))


SUPONEMOS podría ser una idea conveniente hacer inducción en la altura:
Probaremos un resultado más fuerte que tiene como corolario el ejercicio. Veremos que:
alturaAGT + (p - 1) = maxAGT o ponerProfs p

Caso altura = 1:
En esta situación, vemos que t no debe tener hijos pues su altura sería mayor a 1. Es decir, t = Node d [].
alturaAGT t + (p - 1) = 1 + (p - 1) = p
maxAGT o ponerProfs p t = maxAGT (ponerProfs p t) = maxAGT (Node p (map (ponerProfs (p + 1)) [])) = maxAGT (Node p []) = p

Caso altura = n > 1:
En este caso, vemos que t = Node d xs, donde algún elemento de xs tiene altura n-1 y es la altura máxima entre él y sus hermanos.

alturaAGT t = n
maxAGT o ponerProfs p t = maxAGT (ponerProfs p (Node d xs)) = maxAGT (Node p (map (ponerProfs (p + 1)) xs)) =
max (p (maxl (map maxAGT (map (ponerProfs (p + 1)) xs))) = max (p (maxl (map (maxAGT (ponerProfs (p + 1))) xs))) =
max (p (maxl (map (maxAGT o ponerProfs (p + 1)) xs))) = max (p (maxl (map (alturaAGT + p) xs))) =
max (p (n - 1 + p)) = n - 1 + p = n + (p - 1) = alturaAGT t + (p - 1)


-- Ejercicio 10
Lo probaremos por inducción estructural en Tree:

Caso t = Leaf n:
map f (flatten t) = map f (flatten (Leaf n)) = map f [n] = [f n]
flatten (mapTree f n) = flatten (mapTree f (Leaf n)) = flatten (Leaf f n) = [f n]

Caso t = Node n l r:
map f (flatten t) =
map f (flatten (Node n l r)) =
map f (flatten l ++ [n] ++ flatten r) =
map f (flatten l) ++ map f [n] ++ map f (flatten r) =
flatten (mapTree f l) ++ map f [n] ++ flatten (mapTree f r) =
flatten (mapTree f l) ++ [f n] ++ flatten (mapTree f r) =
flatten (Node (f n) (mapTree f l) (mapTree f r)) =
flatten (mapTree f (Node n l r) =
flatten (mapTree f t)




-- Ejercicio 11
Probaremos por inducción estructural en listas:

Caso t = []:
join t = join [] = [] = concat [] = concat (map id [])

Caso t = (x:xs):
join t = join (x:xs) = x ++ join xs = x ++ concat (map id xs) =
map id x ++ concat (map id xs) = concat (map id (x:xs))


Probaremos (de nuevo) por inducción estructural en listas:
t:[[a]] (join.join) t = (join.map join) t

Caso t = []:
join (join []) = join [] = join (map join [])

Caso t = ((x:xs):xss):
join (join t) = join (join ((x:xs):xss)) = join ((x:xs) ++ join xss) =
join (x:(xs ++ join xss)) = x ++ join (xs ++ join xss) =
x ++ y ++ ... ++ z ++ join ([] ++ join xss) =
x ++ y ++ ... ++ z ++ join (join xss) =
x ++ y ++ ... ++ z ++ join (map join xss) =
join (x:xs) ++ join (map join xss)) =
join (join (x:xs) : (map join xss)) =
join (map join ((x:xs):xss))



-- Ejercicio 12
-- Ejercicio 13
-- Ejercicio 14
Dada una propiedad P sobre elementos de F, P(f) valdrá para todo f::F si:
    - Vale P (Zero).
    - Si vale P(n), entonces vale P(One n), con n::F.
    - Si valen P (f True) y P (f False), entonces vale P(Two f), con f::(Bool -> F).