{"id":4613,"date":"2014-11-20T19:44:21","date_gmt":"2014-11-20T18:44:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4613"},"modified":"2014-11-22T06:45:17","modified_gmt":"2014-11-22T05:45:17","slug":"ra2014-razonamiento-sobre-tipos-recursivos-en-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2014-razonamiento-sobre-tipos-recursivos-en-isabellehol\/","title":{"rendered":"RA2014: Razonamiento sobre tipos recursivos en Isabelle\/HOL"},"content":{"rendered":"<p>En la tercera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-14\">Razonamiento autom\u00e1tico<\/a> se ha estudiado<\/p>\n<ul>\n<li>c\u00f3mo definir \u00e1rboles binarios en Isabelle\/HOL y c\u00f3mo demostrar sus propiedades,<\/li>\n<li>c\u00f3mo definir y razonar con funciones recursivas que no son primitivas recursivas y<\/li>\n<li>c\u00f3mo definir y razonar con tipos de datos mutuamente recursivos.<\/li>\n<\/ul>\n<p>La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\ntheory T4b\nimports Main\nbegin\n\ntext {* \n  Ejemplo de definici\u00f3n de tipos recursivos:\n  Definir un tipo de dato para los \u00e1rboles binarios.\n*}\n\ndatatype 'a arbolB = Hoja \"'a\" \n                   | Nodo \"'a\" \"'a arbolB\" \"'a arbolB\"\n\ntext {* \n  Ejemplo de definici\u00f3n sobre \u00e1rboles binarios:\n  Definir la funci\u00f3n \"espejo\" que aplicada a un \u00e1rbol devuelve su imagen\n  especular.  \n*}\n\nfun espejo :: \"'a arbolB \u21d2 'a arbolB\" where\n  \"espejo (Hoja x) = (Hoja x)\"\n| \"espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))\"\n\nvalue \"espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))\"\n-- \"= Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))\"\n\ntext {* \n  Ejemplo de demostraci\u00f3n sobre \u00e1rboles binarios:\n  Demostrar que la funci\u00f3n \"espejo\" es involutiva; es decir, para\n  cualquier \u00e1rbol a, se tiene que \n     espejo(espejo(a)) = a.\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma espejo_involutiva:\n  fixes a :: \"'b arbolB\" \n  shows \"espejo (espejo a) = a\" (is \"?P a\")\nproof (induct a)\n  fix x \n  show \"?P (Hoja x)\" by simp \nnext\n  fix x\n  fix i assume h1: \"?P i\"\n  fix d assume h2: \"?P d\"\n  show \"?P (Nodo x i d)\" \n  proof -\n    have \"espejo(espejo(Nodo x i d)) = espejo(Nodo x (espejo d) (espejo i))\"\n      by simp\n    also have \"\u2026 = Nodo x (espejo (espejo i)) (espejo (espejo d))\" by simp\n    also have \"\u2026 = Nodo x i d\" using h1 h2 by simp \n    finally show ?thesis .\n qed\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (fixes a :: \"'b arbolB\") es una abreviatura de \"sea a1 un \u00e1rbol binario\n    cuyos elementos son de tipo b\". \n  \u00b7 (induct a) indica que el m\u00e9todo de demostraci\u00f3n es por inducci\u00f3n\n    en el \u00e1rbol binario a.\n  \u00b7 Se generan dos casos:\n    1. \u22c0a. espejo (espejo (Hoja a)) = Hoja a\n    2. \u22c0a1 a2 a3. \u27e6espejo (espejo a2) = a2; \n                   espejo (espejo a3) = a3\u27e7\n                  \u27f9 espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma espejo_involutiva_1: \n  \"espejo (espejo a ) = a\"\nby (induct a) auto\n\ntext {* \n  Ejemplo. [Aplanamiento de \u00e1rboles]\n  Definir la funci\u00f3n \"aplana\" que aplane los \u00e1rboles recorri\u00e9ndolos en\n  orden infijo.  \n*}\n\nfun aplana :: \"'a arbolB \u21d2 'a list\" where\n  \"aplana (Hoja x)     = [x]\"\n| \"aplana (Nodo x i d) = (aplana i) @ [x] @ (aplana d)\"\n\nvalue \"aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))\"\n-- \"= [c, b, d, a, e]\"\n\ntext {* \n  Ejemplo. [Aplanamiento de la imagen especular] Demostrar que\n     aplana (espejo a) = rev (aplana a)\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma \n  fixes a :: \"'b arbolB\"\n  shows \"aplana (espejo a) = rev (aplana a)\" (is \"?P a\")\nproof (induct a)\n  fix x\n  show \"?P (Hoja x)\" by simp \nnext\n  fix x \n  fix i assume h1: \"?P i\"\n  fix d assume h2: \"?P d\"\n  show \"?P (Nodo x i d)\" \n  proof -\n    have \"aplana (espejo (Nodo x i d)) = \n          aplana (Nodo x (espejo d) (espejo i))\" by simp\n    also have \"\u2026 = (aplana(espejo d))@[x]@(aplana(espejo i))\" by simp\n    also have \"\u2026 = (rev(aplana d))@[x]@(rev(aplana i))\" using h1 h2 by simp\n    also have \"\u2026 = rev((aplana i)@[x]@(aplana d))\" by simp\n    also have \"\u2026 = rev(aplana (Nodo x i d))\" by simp\n    finally show ?thesis .\n qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"aplana (espejo a) = rev (aplana a)\"\nby (induct a) auto\n\nsection {* Heur\u00edsticas para la inducci\u00f3n *}\n\ntext {*\n  Definici\u00f3n. [Definici\u00f3n recursiva de inversa]\n  (inversa xs) la inversa de la lista xs. Por ejemplo,\n     inversa [a,b,c] = [c,b,a] \n*}\n\nfun inversa :: \"'a list \u21d2 'a list\" where\n  \"inversa [] = []\" \n| \"inversa (x#xs) = (inversa xs) @ [x]\"\n\nvalue \"inversa [a,b,c]\"\n\ntext {* \n  Definici\u00f3n. [Definici\u00f3n de inversa con acumuladores]\n  (inversaAc xs) es la inversa de la lista xs calculada con\n  acumuladores. Por ejemplo,\n     inversaAc [a,b,c]       = [c,b,a] \n     inversaAcAux [a,b,c] [] = [c,b,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\ndefinition inversaAc :: \"'a list \u21d2 'a list\" where\n  \"inversaAc xs \u2261 inversaAcAux xs []\"\n\nvalue \"inversaAcAux [a,b,c] []\"\nvalue \"inversaAc [a,b,c]\"\n\ntext {* \n  Lema. [Ejemplo de equivalencia entre las definiciones]\n  La inversa de [a,b,c] es lo mismo calculada con la primera definici\u00f3n\n  que con la segunda.\n*}\n\nlemma \"inversaAc [a,b,c] = inversa [a,b,c]\"\nby (simp add: inversaAc_def)\n\ntext {*\n  Nota. [Ejemplo fallido de demostraci\u00f3n por inducci\u00f3n]\n  El siguiente intento de demostrar que para cualquier lista xs, se\n  tiene que  \"inversaAc xs = inversa xs\" falla.\n*}\n\nlemma \"inversaAc xs = inversa xs\"\nproof (induct xs)\n  show \"inversaAc [] = inversa []\" by (simp add: inversaAc_def)\nnext\n  fix a xs assume HI: \"inversaAc xs = inversa xs\"\n  have \"inversaAc (a#xs) = inversaAcAux (a#xs) []\" by (simp add: inversaAc_def)\n  also have \"\u2026 = inversaAcAux xs [a]\" by simp\n  also have \"\u2026 = inversa (a#xs)\"\n  -- \"Problema: la hip\u00f3tesis de inducci\u00f3n no es aplicable.\"\noops\n\ntext {* \n  Nota. [Heur\u00edstica de generalizaci\u00f3n]\n  Cuando se use demostraci\u00f3n estructural, cuantificar universalmente las \n  variables libres (o, equivalentemente, considerar las variables libres\n  como variables arbitrarias).\n\n  Lema. [Lema con generalizaci\u00f3n]\n  Para toda lista ys se tiene \n     inversaAcAux xs ys = (inversa xs) @ ys\n*}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma inversaAcAux_es_inversa:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\nproof (induct xs arbitrary: ys)\n  show \"\u22c0ys. inversaAcAux [] ys = (inversa [])@ys\" by simp\nnext\n  fix a xs \n  assume HI: \"\u22c0ys. inversaAcAux xs ys = inversa xs@ys\"\n  show \"\u22c0ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys\"\n  proof -\n    fix ys\n    have \"inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)\" by simp\n    also have \"\u2026 = inversa xs@(a#ys)\" using HI by simp\n    also have \"\u2026 = inversa (a#xs)@ys\" using [[simp_trace]] by simp \n    finally show \"inversaAcAux (a#xs) ys = inversa (a#xs)@ys\" by simp\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma inversaAcAux_es_inversa_1:\n  \"inversaAcAux xs ys = (inversa xs)@ys\"\nby (induct xs arbitrary: ys) auto\n\ntext {*\n  Corolario.  Para cualquier lista xs, se tiene que\n     inversaAc xs = inversa xs\n*}\n\ncorollary \"inversaAc xs = inversa xs\"\nby (simp add: inversaAcAux_es_inversa inversaAc_def)\n\ntext {*\n  Nota. En el paso \"inversa xs@(a#ys) = inversa (a#xs)@ys\" se usan\n  lemas de la teor\u00eda List. Se puede observar, insertano \n     using [[simp_trace]]\n  entre la igualdad y by simp, que los lemas usados son \n  \u00b7 List.append_simps_1: []@ys = ys\n  \u00b7 List.append_simps_2: (x#xs)@ys = x#(xs@ys)\n  \u00b7 List.append_assoc:   (xs @ ys) @ zs = xs @ (ys @ zs)\n  Las dos primeras son las ecuaciones de la definici\u00f3n de append.\n\n  En la siguiente demostraci\u00f3n se detallan los lemas utilizados.\n*}\n\nlemma \"(inversa xs)@(a#ys) = (inversa (a#xs))@ys\"\nproof -\n  have \"(inversa xs)@(a#ys) = (inversa xs)@(a#([]@ys))\" \n    by (simp only: append.simps(1))\n  also have \"\u2026 = (inversa xs)@([a]@ys)\" by (simp only: append.simps(2))\n  also have \"\u2026 = ((inversa xs)@[a])@ys\" by (simp only: append_assoc)\n  also have \"\u2026 = (inversa (a#xs))@ys\" by (simp only: inversa.simps(2))\n  finally show ?thesis .\nqed\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\nsection {* Recursi\u00f3n mutua e inducci\u00f3n *}\n\ntext {*\n  Nota. [Ejemplo de definici\u00f3n de tipos mediante recursi\u00f3n cruzada]\n  \u00b7 Un \u00e1rbol de tipo a es una hoja o un nodo de tipo a junto con un\n    bosque de tipo a.\n  \u00b7 Un bosque de tipo a es el boque vac\u00edo o un bosque contruido a\u00f1adiendo\n    un \u00e1rbol de tipo a a un bosque de tipo a.\n*}\n\ndatatype 'a arbol = Hoja | Nodo \"'a\" \"'a bosque\"\n     and 'a bosque = Vacio | ConsB \"'a arbol\" \"'a bosque\"\n\ntext {*\n  Regla de inducci\u00f3n correspondiente a la recursi\u00f3n cruzada:\n  La regla de inducci\u00f3n sobre \u00e1rboles y bosques es arbol_bosque.induct:\n     \u27e6P1 Hoja; \n      \u22c0x b. P2 b \u27f9 P1 (Nodo x b); \n      P2 Vacio;\n      \u22c0a b. \u27e6P1 a; P2 b\u27e7 \u27f9 P2 (ConsB a b)\u27e7 \n     \u27f9 P1 a \u2227 P2 b\n*}\n\ntext {* \n  Ejemplos de definici\u00f3n por recursi\u00f3n cruzada:\n  \u00b7 aplana_arbol a) es la lista obtenida aplanando el \u00e1rbol a.   \n  \u00b7 (aplana_bosque b) es la lista obtenida aplanando el bosque b.   \n  \u00b7 (map_arbol a h) es el \u00e1rbol obtenido aplicando la funci\u00f3n h a\n    todos los nodos del \u00e1rbol a.   \n  \u00b7 (map_bosque b h) es el bosque obtenido aplicando la funci\u00f3n h a\n    todos los nodos del bosque b. \n*}\n\nfun aplana_arbol :: \"'a arbol \u21d2 'a list\" and \n    aplana_bosque :: \"'a bosque \u21d2 'a list\" where\n  \"aplana_arbol Hoja = []\"\n| \"aplana_arbol (Nodo x b) = x#(aplana_bosque b)\"\n| \"aplana_bosque Vacio = []\"\n| \"aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)\"\n\nfun map_arbol :: \"('a \u21d2 'b) \u21d2 'a arbol \u21d2 'b arbol\" and\n    map_bosque :: \"('a \u21d2 'b) \u21d2 'a bosque \u21d2 'b bosque\" where\n  \"map_arbol  f Hoja        = Hoja\"\n| \"map_arbol  f (Nodo x b)  = Nodo (f x) (map_bosque f b)\"\n| \"map_bosque f Vacio       = Vacio\"\n| \"map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)\"\n\ntext {*\n  Ejemplo de demostraci\u00f3n por inducci\u00f3n cruzada:\n  Demostrar que:\n  \u00b7 aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)\n  \u00b7 aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\n*}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma \"aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)\n     \u2227 aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\nproof (induct_tac a and b)\n  show \"aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)\" \n    by simp\nnext\n  fix x b\n  assume HI: \"aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\n  have \"aplana_arbol (map_arbol f (Nodo x b)) = \n        aplana_arbol (Nodo (f x) (map_bosque f b))\" by simp\n  also have \"\u2026 = (f x)#(aplana_bosque (map_bosque f b))\" by simp\n  also have \"\u2026 = (f x)#(map f (aplana_bosque b))\" using HI by simp\n  also have \"\u2026 = map f (aplana_arbol (Nodo x b))\" by simp\n  finally show \"aplana_arbol (map_arbol f (Nodo x b))\n                = map f (aplana_arbol (Nodo x b))\" .\nnext\n  show \"aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)\" \n    by simp\nnext\n  fix a b\n  assume HI1: \"aplana_arbol (map_arbol f a) = map f (aplana_arbol a)\"\n     and HI2: \"aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\n  have \"aplana_bosque (map_bosque f (ConsB a b)) = \n        aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))\" by simp\n  also have \"\u2026 = aplana_arbol(map_arbol f a)@aplana_bosque(map_bosque f b)\" \n    by simp\n  also have \"\u2026 = (map f (aplana_arbol a))@(map f (aplana_bosque b))\" \n    using HI1 HI2 by simp\n  also have \"\u2026 = map f (aplana_bosque (ConsB a b))\" by simp\n  finally show \"aplana_bosque (map_bosque f (ConsB a b)) \n                = map f (aplana_bosque (ConsB a b))\" by simp\nqed\n\ntext {*\n  Comentarios sobre la demostraci\u00f3n anterior:\n  \u00b7 (induct_tac a and b) indica que el m\u00e9todo de demostraci\u00f3n es por\n    inducci\u00f3n cruzada sobre a y b.\n  \u00b7 Se generan 4 casos:\n    1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)\n    2. \u22c0a bosque.\n          aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) \u27f9\n          aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =\n          map h (aplana_arbol (arbol.Nodo a bosque))\n    3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)\n    4. \u22c0arbol bosque.\n          \u27e6aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);\n           aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)\u27e7\n          \u27f9 aplana_bosque (map_bosque (ConsB arbol bosque) h) =\n             map h (aplana_bosque (ConsB arbol bosque))\n*}\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma \"aplana_arbol  (map_arbol  f a) = map f (aplana_arbol a)\n     \u2227 aplana_bosque (map_bosque f b) = map f (aplana_bosque b)\"\nby (induct_tac a and b) auto\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la tercera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo definir \u00e1rboles binarios en Isabelle\/HOL y c\u00f3mo demostrar sus propiedades, c\u00f3mo definir y razonar con funciones recursivas que no son primitivas recursivas y c\u00f3mo definir y razonar con tipos de datos mutuamente recursivos. La correspondiente teor\u00eda Isabelle\/HOL&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[240],"tags":[144,307],"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\/4613"}],"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=4613"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4613\/revisions"}],"predecessor-version":[{"id":4614,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4613\/revisions\/4614"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4613"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4613"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4613"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}