{"id":5624,"date":"2016-11-24T18:52:33","date_gmt":"2016-11-24T17:52:33","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5624"},"modified":"2016-12-06T09:59:15","modified_gmt":"2016-12-06T08:59:15","slug":"ra2016-funciones-recursivas-generales-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2016-funciones-recursivas-generales-en-isabellehol\/","title":{"rendered":"RA2016: Funciones recursivas generales en Isabelle\/HOL"},"content":{"rendered":"

En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo definir en Isabelle\/HOL funciones recursivas que no son primitiva recursiva<\/a> y c\u00f3mo demostrar propiedades de dichas funciones. Como ejemplo, se ha usado la funci\u00f3n de Ackerman<\/a>.<\/p>\n

La teor\u00eda con las soluciones de los ejercicios es la siguiente
\n<\/p>\n

\nchapter {* Tema 4: Razonamiento por casos y por inducci\u00f3n *}\n\ntheory T4b\nimports Main \nbegin\n\nsection {* Recursi\u00f3n general. La funci\u00f3n de Ackermann *}\n\ntext {* \n  El objetivo de esta secci\u00f3n es mostrar el uso de las definiciones\n  recursivas generales y sus esquemas de inducci\u00f3n. Como ejemplo se usa la\n  funci\u00f3n de Ackermann (se puede consultar informaci\u00f3n sobre dicha funci\u00f3n en\n  http:\/\/en.wikipedia.org\/wiki\/Ackermann_function).\n\n  Definici\u00f3n.  La funci\u00f3n de Ackermann se define por\n    A(m,n) = n+1,             si m=0,\n             A(m-1,1),        si m>0 y n=0,\n             A(m-1,A(m,n-1)), si m>0 y n>0\n  para todo los n\u00fameros naturales. \n\n  La funci\u00f3n de Ackermann es recursiva, pero no es primitiva recursiva. \n*}\n\nfun ack :: \"nat \u21d2 nat \u21d2 nat\" where\n  \"ack 0       n       = n+1\" \n| \"ack (Suc m) 0       = ack m 1\" \n| \"ack (Suc m) (Suc n) = ack m (ack (Suc m) n)\"\n\n-- \"Ejemplo de evaluaci\u00f3n\"\nvalue \"ack 2 3\" (* devuelve 9 *)\n\ntext {*\n  Esquema de inducci\u00f3n correspondiente a una funci\u00f3n:\n  \u00b7 Al definir una funci\u00f3n recursiva general se genera una regla de\n    inducci\u00f3n. En la definici\u00f3n anterior, la regla generada es\n    ack.induct: \n       \u27e6\u22c0n. P 0 n; \n        \u22c0m. P m 1 \u27f9 P (Suc m) 0;\n        \u22c0m n. \u27e6P (Suc m) n; P m (ack (Suc m) n)\u27e7 \u27f9 P (Suc m) (Suc n)\u27e7\n       \u27f9 P a b\n*}\n\ntext {*\n  Ejemplo de demostraci\u00f3n por la inducci\u00f3n correspondiente a una funci\u00f3n:\n  Demostrar que para todos m y n, A(m,n) > n.\n*} \n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"ack m n > n\"\nproof (induct m n rule: ack.induct)\n  fix n\n  show \"ack 0 n > n\" by simp\nnext\n  fix m \n  assume \"ack m 1 > 1\"\n  then show \"ack (Suc m) 0 > 0\" by simp\nnext  \n  fix m n\n  assume \"n < ack (Suc m) n\" and \n         \"ack (Suc m) n < ack m (ack (Suc m) n)\"\n  then show \"Suc n < ack (Suc m) (Suc n)\" by simp\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (induct m n rule: ack.induct) indica que el m\u00e9todo de demostraci\u00f3n\n    es el esquema de recursi\u00f3n correspondiente a la definici\u00f3n de \n    (ack m n).\n  \u00b7 Se generan 3 casos:\n    1. \u22c0n. n < ack 0 n\n    2. \u22c0m. 1 < ack m 1 \u27f9 0 < ack (Suc m) 0\n    3. \u22c0m n. \u27e6n < ack (Suc m) n; \n              ack (Suc m) n < ack m (ack (Suc m) n)\u27e7\n             \u27f9 Suc n < ack (Suc m) (Suc n)\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"ack m n > n\"\nby (induct m n rule: ack.induct) auto\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo definir en Isabelle\/HOL funciones recursivas que no son primitiva recursiva y c\u00f3mo demostrar propiedades de dichas funciones. Como ejemplo, se ha usado la funci\u00f3n de Ackerman. La teor\u00eda con las soluciones de los ejercicios es la siguiente<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[261],"tags":[144,314],"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\/5624"}],"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=5624"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5624\/revisions"}],"predecessor-version":[{"id":5625,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5624\/revisions\/5625"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5624"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5624"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5624"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}