{"id":6887,"date":"2019-11-07T15:43:19","date_gmt":"2019-11-07T14:43:19","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6887"},"modified":"2019-12-06T15:44:42","modified_gmt":"2019-12-06T14:44:42","slug":"ra2019-ejercicios-de-programacion-funcional-en-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-ejercicios-de-programacion-funcional-en-isabelle-hol\/","title":{"rendered":"RA2019: Ejercicios de programaci\u00f3n funcional en Isabelle\/HOL"},"content":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-19\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de la 1\u00aa relaci\u00f3n de ejercicios de razonamiento<br \/>\nsobre programaci\u00f3n funcional en Isabelle\/HOL.<\/p>\n<p>La teor\u00eda con las soluciones de los ejercicios es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039R1: Programaci\u00f3n funcional en Isabelle\u203a\n\ntheory R1_Programacion_funcional_en_Isabelle_sol\n\nimports Main \nbegin\n\ntext \u2039----------------------------------------------------------------\n  Ejercicio 1. Definir, por recursi\u00f3n, la funci\u00f3n\n     longitud :: 'a list \u21d2 nat\n  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,\n     longitud [a,b,c] = 3\n  -------------------------------------------------------------------\u203a\n\nfun longitud :: \"'a list \u21d2 nat\" where\n  \"longitud []     = 0\"\n| \"longitud (x#xs) = 1 + longitud xs\"\n   \nvalue \"longitud [a,b,c] = 3\" \n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n\n     fun intercambia :: 'a \u00d7 'b \u21d2 'b \u00d7 'a\n  tal que (intercambia p) es el par obtenido intercambiando las\n  componentes del par p. Por ejemplo,\n     intercambia (u,v) = (v,u)\n  ------------------------------------------------------------------\u203a\n\nfun intercambia :: \"'a \u00d7 'b \u21d2 'b \u00d7 'a\" where\n  \"intercambia (x,y) = (y,x)\"\n\nvalue \"intercambia (u,v) = (v,u)\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 3. Definir, por recursi\u00f3n, la funci\u00f3n\n     inversa :: 'a list \u21d2 'a list\n  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los\n  elementos de xs. Por ejemplo,\n     inversa [a,d,c] = [c,d,a]\n  ------------------------------------------------------------------\u203a\n\nfun inversa :: \"'a list \u21d2 'a list\" where\n  \"inversa []     = []\"\n| \"inversa (x#xs) = inversa xs @ [x]\"\n\nvalue \"inversa [a,d,c] = [c,d,a]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n\n     repite :: nat \u21d2 'a \u21d2 'a list\n  tal que (repite n x) es la lista formada por n copias del elemento\n  x. Por ejemplo, \n     repite 3 a = [a,a,a]\n  ------------------------------------------------------------------\u203a\n\nfun repite :: \"nat \u21d2 'a \u21d2 'a list\" where\n  \"repite 0 x       = []\"\n| \"repite (Suc n) x = x # (repite n x)\"\n\nvalue \"repite 3 a = [a,a,a]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 5. Definir la funci\u00f3n\n     conc :: 'a list \u21d2 'a list \u21d2 'a list\n  tal que (conc xs ys) es la concatenci\u00f3n de las listas xs e ys. Por\n  ejemplo, \n     conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]\n  ------------------------------------------------------------------\u203a\n\nfun conc :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"conc []     ys = ys\"\n| \"conc (x#xs) ys = x # (conc xs ys)\"\n\nvalue \"conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 6. Definir la funci\u00f3n\n     coge :: nat \u21d2 'a list \u21d2 'a list\n  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por \n  ejemplo, \n     coge 2 [a,c,d,b,e] = [a,c]\n  ------------------------------------------------------------------\u203a\n\nfun coge :: \"nat \u21d2 'a list \u21d2 'a list\" where\n  \"coge n []           = []\"\n| \"coge 0 xs           = []\"\n| \"coge (Suc n) (x#xs) = x # (coge n xs)\"\n\nvalue \"coge 2 [a,c,d,b,e] = [a,c]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 7. Definir la funci\u00f3n\n     elimina :: nat \u21d2 'a list \u21d2 'a list\n  tal que (elimina n xs) es la lista obtenida eliminando los n primeros\n  elementos de xs. Por ejemplo, \n     elimina 2 [a,c,d,b,e] = [d,b,e]\n  ------------------------------------------------------------------\u203a\n\nfun elimina :: \"nat \u21d2 'a list \u21d2 'a list\" where\n  \"elimina n []           = []\"\n| \"elimina 0 xs           = xs\"\n| \"elimina (Suc n) (x#xs) = elimina n xs\"\n\nvalue \"elimina 2 [a,c,d,b,e] = [d,b,e]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 8. Definir la funci\u00f3n\n     esVacia :: 'a list \u21d2 bool\n  tal que (esVacia xs) se verifica si xs es la lista vac\u00eda. Por ejemplo,\n     esVacia []  = True\n     esVacia [a] = False\n  ------------------------------------------------------------------\u203a\n\nfun esVacia :: \"'a list \u21d2 bool\" where\n  \"esVacia []     = True\"\n| \"esVacia (x#xs) = False\"\n\nvalue \"esVacia []  = True\"\nvalue \"esVacia [a] = False\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 9. Definir la funci\u00f3n\n     inversaAc :: 'a list \u21d2 'a list\n  tal que (inversaAc xs) es a inversa de xs calculada usando\n  acumuladores. Por ejemplo, \n     inversaAc [a,c,b,e] = [e,b,c,a]\n  ------------------------------------------------------------------\u203a\n\nfun inversaAcAux :: \"'a list \u21d2 'a list \u21d2 'a list\" where\n  \"inversaAcAux [] ys     = ys\"\n| \"inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)\"\n\nfun inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs = inversaAcAux xs []\"\n\nvalue \"inversaAc [a,c,b,e] = [e,b,c,a]\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 10. Definir la funci\u00f3n\n     sum :: nat list \u21d2 nat\n  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,\n     sum [3,2,5] = 10\n  ------------------------------------------------------------------\u203a\n\nfun sum :: \"nat list \u21d2 nat\" where\n  \"sum []     = 0\"\n| \"sum (x#xs) = x + sum xs\"\n\nvalue \"sum [3,2,5] = 10\"\n\ntext \u2039--------------------------------------------------------------- \n  Ejercicio 11. Definir la funci\u00f3n\n     map :: ('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\n  tal que (map f xs) es la lista obtenida aplicando la funci\u00f3n f a los\n  elementos de xs. Por ejemplo,\n     map (\u03bbx. 2*x) [3,2,5] = [6,4,10]\n  ------------------------------------------------------------------\u203a\n\nfun map :: \"('a \u21d2 'b) \u21d2 'a list \u21d2 'b list\" where\n  \"map f []     = []\"\n| \"map f (x#xs) = (f x) # map f xs\"\n\nvalue \"map (\u03bbx. 2*x) [3::nat,2,5] = [6,4,10]\"\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la segunda parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado las soluciones de la 1\u00aa relaci\u00f3n de ejercicios de razonamiento sobre programaci\u00f3n funcional en Isabelle\/HOL. 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":[333],"tags":[],"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\/6887"}],"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=6887"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6887\/revisions"}],"predecessor-version":[{"id":6890,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6887\/revisions\/6890"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6887"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6887"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6887"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}