RA2014: Árboles binarios completos
En primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de la relación 8. En dicha relación se definen funciones sobre árboles binarios completos y se demuestran con Isabelle/HOL algunas de sus propiedades.
Los ejercicios y sus soluciones se muestran a continuación
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 |
header {* R8: Arboles binarios completos *} theory R8 imports Main begin text {* --------------------------------------------------------------------- Ejercicio 1. Definir el tipo de datos arbol para representar los árboles binarios que no tienen información ni en los nodos y ni en las hojas. Por ejemplo, el árbol · / \ / \ · · / \ / \ · · · · se representa por "N (N H H) (N H H)". --------------------------------------------------------------------- *} datatype arbol = H | N arbol arbol value "N (N H H) (N H H)" text {* --------------------------------------------------------------------- Ejercicio 2. Definir la función hojas :: "arbol => nat" tal que (hojas a) es el número de hojas del árbol a. Por ejemplo, hojas (N (N H H) (N H H)) = 4 --------------------------------------------------------------------- *} fun hojas :: "arbol => nat" where "hojas H = 1" | "hojas (N i d) = hojas i + hojas d" value "hojas (N (N H H) (N H H))" -- "= 4" text {* --------------------------------------------------------------------- Ejercicio 4. Definir la función profundidad :: "arbol => nat" tal que (profundidad a) es la profundidad del árbol a. Por ejemplo, profundidad (N (N H H) (N H H)) = 2 --------------------------------------------------------------------- *} fun profundidad :: "arbol => nat" where "profundidad H = 0" | "profundidad (N i d) = 1 + max (profundidad i) (profundidad d)" value "profundidad (N (N H H) (N H H))" -- "= 2" text {* --------------------------------------------------------------------- Ejercicio 5. Definir la función abc :: "nat ⇒ arbol" tal que (abc n) es el árbol binario completo de profundidad n. Por ejemplo, abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H)) --------------------------------------------------------------------- *} fun abc :: "nat ⇒ arbol" where "abc 0 = H" | "abc (Suc n) = N (abc n) (abc n)" value "abc 3" -- "= N (N (N H H) (N H H)) (N (N H H) (N H H))" text {* --------------------------------------------------------------------- Ejercicio 6. Un árbol binario a es completo respecto de la medida f si a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i como d son árboles binarios completos respecto de f y, además, f(i) = f(d). Definir la función es_abc :: "(arbol => 'a) => arbol => bool tal que (es_abc f a) se verifica si a es un árbol binario completo respecto de f. --------------------------------------------------------------------- *} fun es_abc :: "(arbol => 'a) => arbol => bool" where "es_abc f H = True" | "es_abc f (N i d) = (es_abc f i ∧ es_abc f d ∧ f i = f d)" text {* --------------------------------------------------------------------- Nota. (size a) es el número de nodos del árbol a. Por ejemplo, size (N (N H H) (N H H)) = 3 --------------------------------------------------------------------- *} value "size (N (N H H) (N H H))" value "size (N (N (N H H) (N H H)) (N (N H H) (N H H)))" text {* --------------------------------------------------------------------- Nota. Tenemos 3 funciones de medida sobre los árboles: número de hojas, número de nodos y profundidad. A cada una le corresponde un concepto de completitud. En los siguientes ejercicios demostraremos que los tres conceptos de completitud son iguales. --------------------------------------------------------------------- *} text {* --------------------------------------------------------------------- Ejercicio 7. Demostrar que un árbol binario a es completo respecto de la profundidad syss es completo respecto del número de hojas. --------------------------------------------------------------------- *} text {* Si a es un árbol completo respecto de la profundidad, entonces el número de hojas de a es 2 elevado a la profundidad de a. *} lemma [simp]: "es_abc profundidad a ⟶ hojas a = 2 ^ (profundidad a)" by (induct a) auto theorem es_abc_profundidad_hojas: "es_abc profundidad a = es_abc hojas a" by (induct a) auto text {* --------------------------------------------------------------------- Ejercicio 8. Demostrar que un árbol binario a es completo respecto del número de hojas syss es completo respecto del número de nodos --------------------------------------------------------------------- *} text {* El número de hojas de un árbol binario a es igual al número de nodos de a más 1. *} lemma [simp]: "hojas a = size a + 1" by (induct a) auto theorem es_abc_hojas_size: "es_abc hojas a = es_abc size a" by (induct a) auto text {* --------------------------------------------------------------------- Ejercicio 9. Demostrar que un árbol binario a es completo respecto de la profundidad syss es completo respecto del número de nodos --------------------------------------------------------------------- *} corollary es_abc_size_profundidad: "es_abc size a = es_abc profundidad a" by (simp add: es_abc_profundidad_hojas es_abc_hojas_size) text {* --------------------------------------------------------------------- Ejercicio 10. Demostrar que (abc n) es un árbol binario completo. --------------------------------------------------------------------- *} lemma "es_abc f (abc n)" by (induct n) auto text {* --------------------------------------------------------------------- Ejercicio 11. Demostrar que si a es un árbolo binario completo respecto de la profundidad, entonces a es (abc (profundidad a)). --------------------------------------------------------------------- *} theorem "es_abc profundidad a ⟶ a = abc (profundidad a)" by (induct a) auto text {* --------------------------------------------------------------------- Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de (es_abc size). --------------------------------------------------------------------- *} text {* Basta tomar como f la función constante 0. *} value "es_abc size (N H (N H H))" -- "= False" value "es_abc (λt. 0) (N H (N H H))" -- "= True" lemma "es_abc (λt. 0::nat) ≠ es_abc size" proof assume "es_abc (λt. 0::nat) = es_abc size" hence "(es_abc (λt. 0::nat) (N H (N H H))) = (es_abc size (N H (N H H)))" by (simp add: fun_eq_iff) thus False by simp qed text {* Referencia: Este ejercicio es una adaptación del de Tobias Nipkow "Complete Binary Trees" que se encuentra en http://isabelle.in.tum.de/exercises/trees/complete/ex.pdf *} end |