{"id":6827,"date":"2019-11-07T17:38:16","date_gmt":"2019-11-07T16:38:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6827"},"modified":"2019-11-09T17:43:25","modified_gmt":"2019-11-09T16:43:25","slug":"ra2019-razonamiento-sobre-programas-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2019-razonamiento-sobre-programas-con-isabelle-hol\/","title":{"rendered":"RA2019: Razonamiento sobre programas 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-19\">Razonamiento autom\u00e1tico<\/a> se han comentado las soluciones de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/RA2019\/index.php\/R1\">1\u00aa relaci\u00f3n<\/a>.<\/p>\n<p>En la segunda parte, se ha estudiado c\u00f3mo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-19\/temas\/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>A continuaci\u00f3n se ha explicado c\u00f3mo demostrar autom\u00e1ticamente las propiedades anteriores con Isabelle\/HOL.<\/p>\n<p>El 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>La demostraci\u00f3n es la palabra <strong>by<\/strong> seguida por el m\u00e9todo de demostraci\u00f3n. Los m\u00e9todos que hemos usado son<\/p>\n<ul>\n<li><strong>by simp<\/strong>: que es el m\u00e9todo de simplificaci\u00f3n por reescritura,<\/li>\n<li><strong>by (induct x) auto<\/strong>: que es por inducci\u00f3n en x (donde x es un n\u00famero natural o una lista) y simplificaci\u00f3n autom\u00e1tica de ambos casos,<\/li>\n<li><strong>by (induct rule: fn.induct) auto<\/strong>: que es por inducci\u00f3n seg\u00fan la definici\u00f3n de la funci\u00f3n fn y simplificaci\u00f3n autom\u00e1tica de todos los casos, <\/li>\n<li><strong>by (simp add: lema_auxiliar)<\/strong>: que es el m\u00e9todo de simplificaci\u00f3n por reescritura a\u00f1adi\u00e9ndole a las reglas de reescritura la correspondiente al lema_auxiliar,<\/li>\n<\/ul>\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 2: Razonamiento sobre programas\u203a\n\ntheory T2_Razonamiento_sobre_programas\nimports Main \nbegin\n\ntext \u2039En este tema se demuestra con Isabelle las propiedades de los\n  programas funcionales como se expone en el tema 8 del curso\n  \"Inform\u00e1tica\" que puede leerse en\n  https:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/temas\/tema-8.pdf \u203a \n\ndeclare [[names_short]]\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 (x#xs) = 1 + longitud xs\"\n   \nvalue \"longitud [a,c,d] = 3\"\n\ntext \u2039La definici\u00f3n de la funci\u00f3n longitud genera dos regla de\n  simplificaci\u00f3n\n  \u00b7 longitud.simps(1): longitud [] = 0\n  \u00b7 longitud.simps(2): longitud (?x # ?xs) = 1 + longitud ?xs\n  \n  Se pueden ver con \n  \u00b7 thm longitud.simps(1)\n  \u00b7 thm longitud.simps(2)\n\u203a\n\nthm longitud.simps(1)\n(* da longitud [] = 0 *)\n\nthm longitud.simps(2)\n(* da longitud (?x # ?xs) = 1 + longitud ?xs *)\n\ntext \u2039 ---------------------------------------------------------------\n  Ejemplo 2. Demostrar que \n     longitud [a,c,d] = 3\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n detallada *)\nlemma \"longitud [a,c,d] = 3\"\n  apply (simp only: longitud.simps(2))\n  apply (simp only: longitud.simps(1))\n  done\n\n(* Demostraci\u00f3n aplicativa no detallada  *)\nlemma \"longitud [a,c,d] = 3\"\n  apply simp\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\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) = (v,u)\"\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\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 aplicativa detallada *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  apply (simp only: intercambia.simps)\n  done\n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  apply simp\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"intercambia (intercambia (x,y)) = (x,y)\"\n  by simp \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(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"inversa [x] = [x]\"\n  apply (simp only: inversa.simps(2)) \n  apply (simp only: inversa.simps(1)) \n  apply (simp only: append_Nil)       \n  done\n\n(* Nota: El nombre del \u00faltimo simplificador se busca con *)\nfind_theorems \"[] @ _ = _\"\n\n(* Tambi\u00e9n se puede buscar con la pesta\u00f1a Query *)\n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"inversa [x] = [x]\"\n  apply simp\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"inversa [x] = [x]\"\n  by simp\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\n\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(* Demostraci\u00f3n aplicativa *)\nlemma \"longitud (repite n x) = n\"\n  apply (induct n) \n   apply (simp only: repite.simps(1))\n   apply (simp only: longitud.simps(1))\n  apply (simp only: repite.simps(2))\n  apply (simp only: longitud.simps(2))\n  done\n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"longitud (repite n x) = n\"\n  apply (induct n) \n   apply simp      \n  apply simp       \n  done\n\n(* Demostraci\u00f3n aplicativa con simp_all *)\nlemma \"longitud (repite n x) = n\"\n  apply (induct n) \n   apply simp_all  \n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"longitud (repite n x) = n\"\n  by (induct n) simp_all\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(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\n  apply (induct xs) \n   apply (simp only: conc.simps(1))  \n  apply (simp only: conc.simps(2))   \n  done  \n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\n  apply (induct xs) \n   apply simp_all   \n  done  \n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"conc xs (conc ys zs) = conc (conc xs ys) zs\"\n  by (induct xs) simp_all\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 \u2039Encuentra 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(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"conc xs [] = xs\"\n  apply (induct xs) \n   apply (simp only: conc.simps(1))\n  apply (simp only: conc.simps(2))\n  done  \n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"conc xs [] = xs\"\n  apply (induct xs) \n   apply simp_all   \n  done  \n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"conc xs [] = xs\"\n  by (induct xs) simp_all\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 13. (p. 30) Demostrar que \n     longitud (conc xs ys) = longitud xs + longitud ys\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  apply (induct xs)  \n   apply (simp only: conc.simps(1))\n   apply (simp only: longitud.simps(1))\n  apply (simp only: conc.simps(2)) \n  apply (simp only: longitud.simps(2))\n  done  \n\n(* Demostraci\u00f3n aplicativa *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  apply (induct xs)  \n   apply simp_all   \n  done  \n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"longitud (conc xs ys) = longitud xs + longitud ys\"\n  by (induct xs) simp_all\n\nsection \u2039Inducci\u00f3n correspondiente a la definici\u00f3n recursiva\u203a\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 14. 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  Ejemplo 15. 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  La definici\u00f3n coge genera el esquema de inducci\u00f3n coge.induct:\n     \u27e6\u22c0n. P n []; \n      \u22c0x xs. P 0 (x#xs); \n      \u22c0n x xs. P n xs \u27f9 P (Suc n) (x#xs)\u27e7\n     \u27f9 P n x\n\n  Puede verse usando \"thm coge.induct\". \u203a\n\nthm coge.induct\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 16. (p. 35) Demostrar que \n     conc (coge n xs) (elimina n xs) = xs\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\n  apply (induct rule: coge.induct) \n    apply (simp only: coge.simps(1))\n    apply (simp only: elimina.simps(1))\n    apply (simp only: conc.simps(1))\n   apply (simp only: coge.simps(2))\n   apply (simp only: elimina.simps(2))\n   apply (simp only: conc.simps(1))\n   apply (simp only: coge.simps(3))\n   apply (simp only: elimina.simps(3))\n  apply (simp only: conc.simps(2))\n  done\n\n(* Demostraci\u00f3n aplicativa no detallada *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\n  apply (induct rule: coge.induct) \n    apply simp_all\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"conc (coge n xs) (elimina n xs) = xs\"\n  by (induct rule: coge.induct) simp_all\n\nsection \u2039Razonamiento por casos\u203a\n\ntext \u2039 --------------------------------------------------------------- \n  Ejemplo 17. 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  ------------------------------------------------------------------ \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  Ejemplo 18 (p. 39) . Demostrar que \n     esVacia xs = esVacia (conc xs xs)\n  ------------------------------------------------------------------- \u203a\n\n(* Demostraci\u00f3n aplicativa detallada *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\n  apply (cases xs) \n   apply (simp only: esVacia.simps(1))\n   apply (simp only: conc.simps(1))\n   apply (simp only: esVacia.simps(1))\n  apply (simp only: esVacia.simps(2))\n  apply (simp only: conc.simps(2))\n  apply (simp only: esVacia.simps(2))\n  done\n\n(* Demostraci\u00f3n aplicativa *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\n  apply (cases xs) \n   apply simp_all\n  done\n\n(* Demostraci\u00f3n autom\u00e1tica *)\nlemma \"esVacia xs = esVacia (conc xs xs)\"\n  by (cases xs) simp_all\n\nsection \u2039 Referencias \u203a\n\ntext \u2039\n  \u00b7 J.A. Alonso. \"Razonamiento sobre programas\" http:\/\/goo.gl\/R06O3\n  \u00b7 G. Hutton. \"Programming in Haskell\". Cap. 13 \"Reasoning about\n    programms\". \n  \u00b7 S. Thompson. \"Haskell: the Craft of Functional Programming, 3rd\n    Edition. Cap. 8 \"Reasoning about programms\". \n  \u00b7 L. Paulson. \"ML for the Working Programmer, 2nd Edition\". Cap. 6. \n    \"Reasoning about functional programs\". \n\u203a\n\nend\n<\/pre>\n<p>Como tarea se propuso la resoluci\u00f3n de los ejercicios de la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/RA2019\/index.php\/R2\">2\u00aa relaci\u00f3n<\/a>.<\/p>\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 los ejercicios de la 1\u00aa relaci\u00f3n. En la segunda parte, se ha estudiado c\u00f3mo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las transparencias del tema 8 del curso de&#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":[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\/6827"}],"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=6827"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6827\/revisions"}],"predecessor-version":[{"id":6830,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6827\/revisions\/6830"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6827"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6827"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6827"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}