{"id":5589,"date":"2016-11-03T17:10:12","date_gmt":"2016-11-03T16:10:12","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5589"},"modified":"2016-11-05T10:11:09","modified_gmt":"2016-11-05T09:11:09","slug":"ra2016-ejercicios-de-programacion-funcional-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2016-ejercicios-de-programacion-funcional-con-isabellehol\/","title":{"rendered":"RA2016: Ejercicios de programaci\u00f3n funcional con Isabelle\/HOL"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-16\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de la primera relaci\u00f3n de ejercicios sobre 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 {* R1: Programaci\u00f3n funcional en Isabelle *}\n\ntheory R1_Programacion_funcional_en_Isabelle_sol\n\nimports Main \nbegin\n\ntext {* ----------------------------------------------------------------\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 [4,2,5] = 3\n  ------------------------------------------------------------------- *}\n\nfun longitud :: \"'a list \u21d2 nat\" where\n  \"longitud []     = 0\"\n| \"longitud (x#xs) = 1 + longitud xs\"\n   \nvalue \"longitud [4,2,5]\" -- \"= 3\"\n\ntext {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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 [1] = False\n  ------------------------------------------------------------------ *}\n\nfun esVacia :: \"'a list \u21d2 bool\" where\n  \"esVacia []     = True\"\n| \"esVacia (x#xs) = False\"\n\nvalue \"esVacia []\"  -- \"= True\"\nvalue \"esVacia [1]\" -- \"= False\"\n\ntext {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 {* --------------------------------------------------------------- \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  ------------------------------------------------------------------ *}\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 primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado las soluciones de la primera relaci\u00f3n de ejercicios 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":[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\/5589"}],"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=5589"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5589\/revisions"}],"predecessor-version":[{"id":5590,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5589\/revisions\/5590"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5589"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5589"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5589"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}