{"id":7132,"date":"2020-04-16T14:02:17","date_gmt":"2020-04-16T12:02:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7132"},"modified":"2020-04-29T12:29:11","modified_gmt":"2020-04-29T10:29:11","slug":"lmf019-razonamiento-sobre-programas-con-isabelle-hol-1o-parte","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf019-razonamiento-sobre-programas-con-isabelle-hol-1o-parte\/","title":{"rendered":"LMF2019: Razonamiento sobre programas con Isabelle\/HOL (1\u00ba parte)"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-19\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se ha estudiado c\u00f3mo se pueden demostrar manualmente propiedades de programas Haskell y c\u00f3mo traducir dichas demostraciones a Isabelle\/HOL.<\/p>\n<p>Para ello, se han usado las <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-19\/tema\/tema-8.pdf\">transparencias del tema 8<\/a> del curso de <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-19\/\">Inform\u00e1tica<\/a> (de 1\u00ba del Grado en Matem\u00e1tica). Como lectura complementaria se recomienda el cap\u00edtulo 13 del libro de G. Hutton <a href=\"http:\/\/bit.ly\/1gMqK0X\">Programming in Haskell<\/a>.<\/p>\n<p>La traducci\u00f3n de los enunciado de las propiedades es inmediato: basta escribir la palabra <strong>lemma<\/strong> y a continuaci\u00f3n la propiedad entre comillas dobles; por ejemplo,<\/p>\n<pre lang=\"isar\">\nlemma \"longitud (repite n x) = n\"\n<\/pre>\n<p>Tambi\u00e9n se puede poner un nombre al lema, por ejemplo,<\/p>\n<pre lang=\"isar\">\nlemma inversaAcAux_es_inversa:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\n<\/pre>\n<p>De cada propiedad se han presentados distintas demostracciones:<\/p>\n<ul>\n<li>autom\u00e1tica,<\/li>\n<li>aplicativa estructurada (usando <code>simp<\/code>)<\/li>\n<li>aplicativa detallada (usando <code>simp only<\/code>)<\/li>\n<li>declarativa estructurada (usando <code>simp<\/code>)<\/li>\n<li>declarativa detallada (usando <code>simp only<\/code>)<\/li>\n<\/ul>\n<p>La clase se ha dado mediante videoconferencia y el v\u00eddeo correspondiente a la primera parte es<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/1SsdIYcCrmA\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>y el de la segunda parte es<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/L6neWUbAUso\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>Las transparencia utilizadas son las 28 primeras p\u00e1ginas del tema<br \/>\n\n<!-- iframe plugin v.5.0 wordpress.org\/plugins\/iframe\/ -->\n<iframe loading=\"lazy\" src=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/temas\/tema-8.pdf\" width=\"100%\" frameborder=\"1\" height=\"500\" scrolling=\"yes\" class=\"iframe-class\"><\/iframe>\n<\/p>\n<p>La teor\u00eda con los ejemplos presentados en la clase es la siguiente:<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter \u2039Tema 6: Razonamiento sobre programas\u203a\n\ntheory T6_Razonamiento_sobre_programas\nimports Main \nbegin\n\ntext \u2039En este tema se demuestra con Isabelle las propiedades de los\n  programas funcionales de tema 6 http:\/\/bit.ly\/2Za6YWY\n\n  Para cada propiedades se presentan distintos tipos de demostraciones:\n  autom\u00e1ticas, aplicativas y declarativas.\u203a \n\nsection \u2039Razonamiento ecuacional\u203a\n\ntext \u2039-----------------------------------------------------------------\n  Ejemplo 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,c,d] = 3\n  --------------------------------------------------------------------\u203a\n\nfun longitud :: \"'a list \u21d2 nat\" where\n  \"longitud []     = 0\"\n| \"longitud (_#xs) = 1 + longitud xs\"\n   \nvalue \"longitud [a,c,d]\"\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 2. Demostrar que \n     longitud [a,c,d] = 3\n  ------------------------------------------------------------------- \u203a\n\nlemma \"longitud [a,c,d] = 3\"\n  apply simp\n  done\n\nlemma \"longitud [a,c,d] = 3\"\n  by simp\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 3. 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)\"\n\ntext \u2039La definici\u00f3n de la funci\u00f3n intercambia genera una regla de\n  simplificaci\u00f3n\n  \u00b7 intercambia.simps: intercambia (x,y) = (y,x)\n  \n  Se puede ver con \n  \u00b7 thm intercambia.simps \n\u203a\n\nthm intercambia.simps(1)\n(* da intercambia (?x, ?y) = (?y, ?x) *)\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 4. (p.6) Demostrar que \n     intercambia (intercambia (x,y)) = (x,y)\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  by auto\n\n(* Demostraci\u00f3n autom\u00e1tica 1 *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  by simp \n\n(* Demostraci\u00f3n autom\u00e1tica 2 *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  by (simp only: intercambia.simps)\n\n(* Demostraci\u00f3n aplicativa *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  apply (simp only: intercambia.simps)\n  done\n\n(* Demostraci\u00f3n declarativa 1 *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\nproof -\n  have \"intercambia (intercambia (x,y)) = intercambia (y,x)\"  \n    by simp\n  also have \"\u2026 = (x,y)\" \n    by simp \n  finally show \"intercambia (intercambia (x,y)) = (x,y)\" \n    by simp\nqed\n\n(* Demostraci\u00f3n detallada *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\nproof -\n  have \"intercambia (intercambia (x,y)) = intercambia (y,x)\"  \n    by (simp only: intercambia.simps)\n  also have \"\u2026 = (x,y)\" \n    by (simp only: intercambia.simps)\n  finally show \"intercambia (intercambia (x,y)) = (x,y)\" \n    by this\nqed\n\ntext \u2039Notas sobre el lenguaje: En la demostraci\u00f3n anterior se ha usado\n  \u00b7 \"proof\" para iniciar la prueba,\n  \u00b7 \"-\" (despu\u00e9s de \"proof\") para no usar el m\u00e9todo por defecto,\n  \u00b7 \"have\" para establecer un paso,\n  \u00b7 \"by (simp only: intercambia.simps)\" para indicar que s\u00f3lo se usa\n    como regla de escritura la correspondiente a la definici\u00f3n de\n    intercambia,\n  \u00b7 \"also\" para encadenar pasos ecuacionales,\n  \u00b7 \"\u2026\" para representar la derecha de la igualdad anterior en un\n    razonamiento ecuacional,\n  \u00b7 \"finally\" para indicar el \u00faltimo pasa de un razonamiento ecuacional,\n  \u00b7 \"show\" para establecer la conclusi\u00f3n.\n  \u00b7 \"by simp\" para indicar el m\u00e9todo de demostraci\u00f3n por simplificaci\u00f3n y \n  \u00b7 \"qed\" para terminar la pruebas.\u203a\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 5. 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  Ejemplo 6. (p. 9) Demostrar que \n     inversa [x] = [x]\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"inversa [x] = [x]\"\n  by simp\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"inversa [x] = [x]\"\n  apply simp\n  done\n\ntext \u2039En la demostraci\u00f3n anterior se usaron las siguientes reglas:\n  \u00b7 inversa.simps(1): inversa [] = []\n  \u00b7 inversa.simps(2): inversa (x#xs) = inversa xs @ [x]\n  \u00b7 append_Nil:       [] @ ys = ys\n  Vamos a explicitar su aplicaci\u00f3n.\n\u203a\n\nthm inversa.simps(2)\nthm append_Nil\nthm append.simps\nthm append.simps(1)\n\nfind_theorems\nfind_theorems \"_ @ _ = _\"\nfind_theorems \"[] @ _ = _\"\n\n(* La demostraci\u00f3n aplicativa detallada es *)\nlemma \"inversa [x] = [x]\"\n  apply (simp only: inversa.simps(2)) (* inversa [] @ [x] = [x] *)\n  apply (simp only: inversa.simps(1)) (* [] @ [x] = [x] *)\n  apply (simp only: append_Nil)       (* No subgoals! *)\n  done\n\n(* La demostraci\u00f3n declarativa simplificada es *)\nlemma \"inversa [x] = [x]\"\nproof -\n  have \"inversa [x] = inversa (x#[])\" \n    by simp\n  also have \"\u2026 = (inversa []) @ [x]\" \n    by simp\n  also have \"\u2026 = [] @ [x]\" \n    by simp\n  also have \"\u2026 = [x]\" \n    by simp \n  finally show \"inversa [x] = [x]\" \n    by simp\nqed\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"inversa [x] = [x]\"\nproof -\n  have \"inversa [x] = (inversa []) @ [x]\" \n    by (simp only: inversa.simps(2))\n  also have \"\u2026 = [] @ [x]\" \n    by (simp only: inversa.simps(1))\n  also have \"\u2026 = [x]\" \n    by (simp only: append_Nil) \n  finally show \"inversa [x] = [x]\" \n    by this\nqed\n\nsection \u2039Razonamiento por inducci\u00f3n sobre los naturales \u203a\n\ntext \u2039[Principio de inducci\u00f3n sobre los naturales] Para demostrar una\n  propiedad P para todos los n\u00fameros naturales basta probar que el 0\n  tiene la propiedad P y que si n tiene la propiedad P, entonces n+1\n  tambi\u00e9n la tiene.  \n     \u27e6P 0; \u22c0n. P n \u27f9 P (Suc n)\u27e7 \u27f9 P m\n\n  En Isabelle el principio de inducci\u00f3n sobre los naturales est\u00e1\n  formalizado en el teorema nat.induct y puede verse con\n     thm nat.induct\u203a\n\nthm nat.induct\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 7. 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  Ejemplo 8. (p. 18) Demostrar que \n     longitud (repite n x) = n\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"longitud (repite n x) = n\"\n  apply (induct n) (* 1. longitud (repite 0 x) = 0\n                      2. \u22c0n. longitud (repite n x) = n \u27f9\n                         longitud (repite (Suc n) x) = Suc n *)\n   apply simp      (* 1. \u22c0n. longitud (repite n x) = n \u27f9\n                         longitud (repite (Suc n) x) = Suc n *)\n  apply simp       (* No subgoals *)\n  done\n\n(* La demostraci\u00f3n aplicativa con simp_all es *)\nlemma \"longitud (repite n x) = n\"\n  apply (induct n) (* 1. longitud (repite 0 x) = 0\n                      2. \u22c0n. longitud (repite n x) = n \u27f9\n                         longitud (repite (Suc n) x) = Suc n *)\n   apply simp_all  (* No subgoals *)\n  done\n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"longitud (repite n x) = n\"\n  by (induct n) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"longitud (repite n x) = n\"\nproof (induct n)\n  show \"longitud (repite 0 x) = 0\" \n    by simp\nnext \n  fix n\n  assume HI: \"longitud (repite n x) = n\"\n  have \"longitud (repite (Suc n) x) = longitud (x # (repite n x))\" \n    by simp\n  also have \"\u2026 = 1 + longitud (repite n x)\" \n    by simp\n  also have \"\u2026 = 1 + n\" \n    using HI by simp\n  finally show \"longitud (repite (Suc n) x) = Suc n\" \n    by simp\nqed\n\ntext \u2039Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 A la derecha de proof se indica el m\u00e9todo de la demostraci\u00f3n.\n  \u00b7 (induct n) indica que la demostraci\u00f3n se har\u00e1 por inducci\u00f3n en n.\n  \u00b7 Se generan dos subobjetivos correspondientes a la base y el paso de\n    inducci\u00f3n:\n    1. longitud (repite 0 x) = 0\n    2. \u22c0n. longitud (repite n x) = n \u27f9 \n            longitud (repite (Suc n) x) = Suc n\n    donde \u22c0n se lee \"para todo n\".  \n  \u00b7 \"next\" indica el siguiente subobjetivo.\n  \u00b7 \"fix n\" indica \"sea n un n\u00famero natural cualquiera\"\n  \u00b7 assume HI: \"longitud (repite n x) = n\" indica \u00absupongamos que \n    \"longitud (repite n x) = n\" y sea HI la etiqueta de este supuesto\u00bb.\n  \u00b7 \"using HI\" usando la propiedad etiquetada con HI. \u203a\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"longitud (repite n x) = n\"\nproof (induct n)\n  show \"longitud (repite 0 x) = 0\"\n    by (simp only: repite.simps(1)\n                   longitud.simps(1))\nnext \n  fix n\n  assume HI: \"longitud (repite n x) = n\"\n  have \"longitud (repite (Suc n) x) = longitud (x # (repite n x))\" \n    by (simp only: repite.simps(2))\n  also have \"\u2026 = 1 + longitud (repite n x)\" \n    by (simp only: longitud.simps(2))\n  also have \"\u2026 = 1 + n\" \n    using HI by (simp only:)\n  also have \"\u2026 = Suc n\"\n    (* find_theorems \"Suc _ = _ + _\" *)\n    by (simp only: Suc_eq_plus1_left)\n  finally show \"longitud (repite (Suc n) x) = Suc n\" \n    by this\nqed\n\nsection \u2039Razonamiento por inducci\u00f3n sobre listas \u203a\n\ntext \u2039Para demostrar una propiedad para todas las listas basta demostrar\n  que la lista vac\u00eda tiene la propiedad y que al a\u00f1adir un elemento a\n  una lista que tiene la propiedad se obtiene otra lista que tambi\u00e9n\n  tiene la propiedad. \n\n  En Isabelle el principio de inducci\u00f3n sobre listas est\u00e1 formalizado\n  mediante el teorema list.induct \n     \u27e6P []; \n      \u22c0x xs. P xs \u27f9 P (x#xs)\u27e7 \n     \u27f9 P xs\n\u203a\n\nthm list.induct\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 9. 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  Ejemplo 10. (p. 24) Demostrar que \n     conc xs (conc ys zs) = (conc xs ys) zs\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\n  apply (induct xs) (*  1. conc [] (conc ys zs) = conc (conc [] ys) zs\n                        2. \u22c0a xs.\n                              conc xs (conc ys zs) =\n                              conc (conc xs ys) zs \u27f9\n                              conc (a # xs) (conc ys zs) =\n                              conc (conc (a # xs) ys) zs *)\n   apply simp_all   (* No subgoals! *)\n  done  \n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\n  by (induct xs) simp_all\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\nproof (induct xs)\n  show \"conc [] (conc ys zs) = conc (conc [] ys) zs\" \n    by simp\nnext\n  fix x xs\n  assume HI: \"conc xs (conc ys zs) = conc (conc xs ys) zs\" \n  have \"conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))\" \n    by simp\n  also have \"\u2026 = x # (conc (conc xs ys) zs)\" \n    using HI by simp\n  also have \"\u2026 = conc (conc (x # xs) ys) zs\" \n    by simp\n  finally show \"conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs\" \n    by simp\nqed\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\nproof (induct xs)\n  show \"conc [] (conc ys zs) = conc (conc [] ys) zs\" \n    by (simp only: conc.simps(1))\nnext\n  fix x xs\n  assume HI: \"conc xs (conc ys zs) = conc (conc xs ys) zs\" \n  have \"conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))\" \n    by (simp only: conc.simps(2))\n  also have \"\u2026 = x # (conc (conc xs ys) zs)\" \n    using HI by (simp only:)\n  also have \"\u2026 = conc (conc (x # xs) ys) zs\" \n    by (simp only: conc.simps(2))\n  finally show \"conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs\" \n    by this\nqed\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 11. Refutar que \n     conc xs ys = conc ys xs\n  ------------------------------------------------------------------- \u203a\n\nlemma \"conc xs ys = conc ys xs\"\n  quickcheck\n  oops\n\ntext \u2039 Encuentra el contraejemplo, \n  xs = [a2]\n  ys = [a1] \u203a\n\ntext \u2039--------------------------------------------------------------- \n  Ejemplo 12. (p. 28) Demostrar que \n     conc xs [] = xs\n  ------------------------------------------------------------------- \u203a\n\n(* La demostraci\u00f3n aplicativa es *)\nlemma \"conc xs [] = xs\"\n  apply (induct xs) (* 1. conc [] [] = []\n                       2. \u22c0a xs.\n                             conc xs [] = xs \u27f9\n                             conc (a # xs) [] = a # xs *)\n   apply simp_all   (* No subgoals! *)\n  done  \n\n(* La demostraci\u00f3n autom\u00e1tica es *)\nlemma \"conc xs [] = xs\"\n  by (induct xs) simp_all\n\n(* declare [[show_types]] *)\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"conc xs [] = xs\"\nproof (induct xs)\n  show \"conc [] [] = []\" \n    by simp\nnext \n  fix x xs\n  assume HI: \"conc xs [] = xs\" \n  have \"conc (x # xs) [] = x # (conc xs [])\" \n    by simp\n  also have \"\u2026 = x # xs\" \n    using HI by simp\n  finally show \"conc (x # xs) [] = x # xs\" \n    by simp\nqed\n\n\n(* La demostraci\u00f3n declarativa es *)\nlemma \"conc xs [] = xs\"\nproof (induct xs)\n  show \"conc [] [] = []\" by simp\nnext \n  fix x :: \"'a\" and xs :: \"'a list\"\n  assume HI: \"conc xs [] = xs\" \n  have \"conc (x # xs) [] = x # (conc xs [])\" \n    by simp\n  also have \"\u2026 = x # xs\" \n    using HI by simp\n  finally show \"conc (x # xs) [] = x # xs\" \n    by simp\nqed\n\n(* La demostraci\u00f3n declarativa detallada es *)\nlemma \"conc xs [] = xs\"\nproof (induct xs)\n  show \"conc [] [] = []\" \n    by (simp only: conc.simps(1))\nnext \n  fix x :: \"'a\" and xs :: \"'a list\"\n  assume HI: \"conc xs [] = xs\" \n  have \"conc (x # xs) [] = x # (conc xs [])\" \n    by (simp only: conc.simps(2))\n  also have \"\u2026 = x # xs\" \n    using HI by (simp only:)\n  finally show \"conc (x # xs) [] = x # xs\" \n    by this\nqed\n\nend\n<\/pre>\n<p>Como tarea se ha propuesto la resoluci\u00f3n de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/LMF2020\/index.php\/R9\">9\u00aa relaci\u00f3n<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos se ha estudiado c\u00f3mo se pueden demostrar manualmente propiedades de programas Haskell y c\u00f3mo traducir dichas demostraciones a Isabelle\/HOL. Para ello, se han usado las transparencias del tema 8 del curso de Inform\u00e1tica (de 1\u00ba del Grado en Matem\u00e1tica). Como lectura complementaria se&#8230;<\/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":[334],"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\/7132"}],"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=7132"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7132\/revisions"}],"predecessor-version":[{"id":7158,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7132\/revisions\/7158"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7132"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7132"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7132"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}