{"id":4680,"date":"2014-12-18T17:39:04","date_gmt":"2014-12-18T16:39:04","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4680"},"modified":"2014-12-19T12:41:09","modified_gmt":"2014-12-19T11:41:09","slug":"ra2014-arboles-binarios-completos","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-arboles-binarios-completos\/","title":{"rendered":"RA2014: \u00c1rboles binarios completos"},"content":{"rendered":"<p>En primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-14\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de los ejercicios de la relaci\u00f3n 8. En dicha relaci\u00f3n se definen funciones sobre \u00e1rboles binarios completos y se demuestran con Isabelle\/HOL algunas de sus propiedades.<\/p>\n<p>Los ejercicios y sus soluciones se muestran a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* R8: Arboles binarios completos *}\n\ntheory R8\nimports Main \nbegin \n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir el tipo de datos arbol para representar los\n  \u00e1rboles binarios que no tienen informaci\u00f3n ni en los nodos y ni en las\n  hojas. Por ejemplo, el \u00e1rbol\n          \u00b7\n         \/ \\\n        \/   \\\n       \u00b7     \u00b7\n      \/ \\   \/ \\\n     \u00b7   \u00b7   \u00b7   \u00b7 \n  se representa por \"N (N H H) (N H H)\".\n  --------------------------------------------------------------------- \n*}\n\ndatatype arbol = H | N arbol arbol\n\nvalue \"N (N H H) (N H H)\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n\n     hojas :: \"arbol => nat\" \n  tal que (hojas a) es el n\u00famero de hojas del \u00e1rbol a. Por ejemplo,\n     hojas (N (N H H) (N H H)) = 4\n  --------------------------------------------------------------------- \n*}\n\nfun hojas :: \"arbol => nat\" where\n  \"hojas H       = 1\"\n| \"hojas (N i d) = hojas i + hojas d\"\n\nvalue \"hojas (N (N H H) (N H H))\" -- \"= 4\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n\n     profundidad :: \"arbol => nat\" \n  tal que (profundidad a) es la profundidad del \u00e1rbol a. Por ejemplo,\n     profundidad (N (N H H) (N H H)) = 2\n  --------------------------------------------------------------------- \n*}\n\nfun profundidad :: \"arbol => nat\" where\n  \"profundidad H       = 0\"\n| \"profundidad (N i d) = 1 + max (profundidad i) (profundidad d)\"\n\nvalue \"profundidad (N (N H H) (N H H))\" -- \"= 2\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 5. Definir la funci\u00f3n\n     abc :: \"nat \u21d2 arbol\" \n  tal que (abc n) es el \u00e1rbol binario completo de profundidad n. Por\n  ejemplo,  \n     abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))\n  --------------------------------------------------------------------- \n*}\n\nfun abc :: \"nat \u21d2 arbol\" where\n  \"abc 0       = H\"\n| \"abc (Suc n) = N (abc n) (abc n)\"\n\nvalue \"abc 3\" -- \"= N (N (N H H) (N H H)) (N (N H H) (N H H))\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Un \u00e1rbol binario a es completo respecto de la medida f si\n  a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i\n  como d son \u00e1rboles binarios completos respecto de f y, adem\u00e1s, \n  f(i) = f(d).\n\n  Definir la funci\u00f3n\n     es_abc :: \"(arbol => 'a) => arbol => bool\n  tal que (es_abc f a) se verifica si a es un \u00e1rbol binario completo\n  respecto de f.\n  --------------------------------------------------------------------- \n*}\n\nfun es_abc :: \"(arbol => 'a) => arbol => bool\" where\n  \"es_abc f H       = True\"\n| \"es_abc f (N i d) = (es_abc f i \u2227 es_abc f d \u2227 f i = f d)\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Nota. (size a) es el n\u00famero de nodos del \u00e1rbol a. Por ejemplo,\n     size (N (N H H) (N H H)) = 3\n  --------------------------------------------------------------------- \n*}\n\nvalue \"size (N (N H H) (N H H))\"\nvalue \"size (N (N (N H H) (N H H)) (N (N H H) (N H H)))\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Nota. Tenemos 3 funciones de medida sobre los \u00e1rboles: n\u00famero de\n  hojas, n\u00famero de nodos y profundidad. A cada una le corresponde un\n  concepto de completitud. En los siguientes ejercicios demostraremos\n  que los tres conceptos de completitud son iguales.\n  --------------------------------------------------------------------- \n*}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 7. Demostrar que un \u00e1rbol binario a es completo respecto de\n  la profundidad syss es completo respecto del n\u00famero de hojas.\n  --------------------------------------------------------------------- \n*}\n\ntext {* Si a es un \u00e1rbol completo respecto de la profundidad, entonces\n  el n\u00famero de hojas de a es 2 elevado a la profundidad de a. *}\nlemma [simp]: \"es_abc profundidad a \u27f6 hojas a = 2 ^ (profundidad a)\"\nby (induct a) auto\n\ntheorem es_abc_profundidad_hojas: \"es_abc profundidad a = es_abc hojas a\"\nby (induct a) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 8. Demostrar que un \u00e1rbol binario a es completo respecto del\n  n\u00famero de hojas syss es completo respecto del n\u00famero de nodos\n  --------------------------------------------------------------------- \n*}\n\ntext {* El n\u00famero de hojas de un \u00e1rbol binario a es igual al n\u00famero de\n  nodos de a m\u00e1s 1. *}\nlemma [simp]: \"hojas a = size a + 1\"\nby (induct a) auto\n\ntheorem es_abc_hojas_size: \"es_abc hojas a = es_abc size a\"\nby (induct a) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 9. Demostrar que un \u00e1rbol binario a es completo respecto de\n  la profundidad syss es completo respecto del n\u00famero de nodos\n  --------------------------------------------------------------------- \n*}\n\ncorollary es_abc_size_profundidad: \n  \"es_abc size a = es_abc profundidad a\"\nby (simp add: es_abc_profundidad_hojas es_abc_hojas_size)\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 10. Demostrar que (abc n) es un \u00e1rbol binario completo.\n  --------------------------------------------------------------------- \n*}\n\nlemma \"es_abc f (abc n)\"\nby (induct n) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 11. Demostrar que si a es un \u00e1rbolo binario completo\n  respecto de la profundidad, entonces a es (abc (profundidad a)).\n  --------------------------------------------------------------------- \n*}\n\ntheorem \"es_abc profundidad a \u27f6 a = abc (profundidad a)\"\nby (induct a) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de \n  (es_abc size).\n  --------------------------------------------------------------------- \n*}\n\ntext {* Basta tomar como f la funci\u00f3n constante 0. *}\n\nvalue \"es_abc size (N H (N H H))\"     -- \"= False\"\nvalue \"es_abc (\u03bbt. 0) (N H (N H H))\" -- \"= True\"\n\nlemma \"es_abc (\u03bbt. 0::nat) \u2260 es_abc size\"\nproof \n  assume \"es_abc (\u03bbt. 0::nat) = es_abc size\"\n  hence \"(es_abc (\u03bbt. 0::nat) (N H (N H H))) = (es_abc size (N H (N H H)))\"\n    by (simp add: fun_eq_iff)\n  thus False by simp\nqed\n\ntext {*\n  Referencia: Este ejercicio es una adaptaci\u00f3n del de Tobias Nipkow\n  \"Complete Binary Trees\" que se encuentra en \n  <p><a href=\"http:\/\/isabelle.in.tum.de\/exercises\/trees\/complete\/ex.pdf\" target=\"_blank\" rel=\"noopener noreferrer nofollow\">Click to access ex.pdf<\/a><\/p>\n*}\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado las soluciones de los ejercicios de la relaci\u00f3n 8. En dicha relaci\u00f3n se definen funciones sobre \u00e1rboles binarios completos y se demuestran con Isabelle\/HOL algunas de sus propiedades. Los ejercicios y sus soluciones se muestran a continuaci\u00f3n<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[240],"tags":[144,307],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4680"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4680"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4680\/revisions"}],"predecessor-version":[{"id":4682,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4680\/revisions\/4682"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4680"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4680"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4680"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}