{"id":6408,"date":"2018-12-20T19:00:56","date_gmt":"2018-12-20T18:00:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6408"},"modified":"2018-12-22T08:01:59","modified_gmt":"2018-12-22T07:01:59","slug":"ra2018-verificacion-de-algoritmos-de-ordenacion-con-isabelle-hol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2018-verificacion-de-algoritmos-de-ordenacion-con-isabelle-hol\/","title":{"rendered":"RA2018: Verificaci\u00f3n de algoritmos de ordenaci\u00f3n con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-18\">Razonamiento autom\u00e1tico<\/a> se ha estudiado c\u00f3mo verificar con Isabelle\/HOL la correcci\u00f3n de distintos algoritmos de ordenaci\u00f3n.<\/p>\n<p>El primero de los algoritmos verificados ha sido el de ordenaci\u00f3n por inserci\u00f3n. La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nchapter {* T6a: Verificaci\u00f3n de la ordenaci\u00f3n por inserci\u00f3n *}\n\ntheory T6a_Verificacion_de_la_ordenacion_por_insercion\nimports Main\nbegin\n\ntext {*\n  En este de tema se define el algoritmo de ordenaci\u00f3n de listas \n  por inserci\u00f3n y se demuestra que es correcto. *}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir la funci\u00f3n\n     inserta :: int \u21d2 int list \u21d2 int list\n  tal que (inserta a xs) es la lista obtenida insertando a delante del\n  primer elemento de xs que es mayor o igual que a. Por ejemplo,\n     inserta 3 [2,5,1,7] = [2,3,5,1,7]\n  ------------------------------------------------------------------ *}\n\nfun inserta :: \"int \u21d2 int list \u21d2 int list\" where\n  \"inserta a []     = [a]\"\n| \"inserta a (x#xs) = (if a \u2264 x \n                       then a # x # xs \n                       else x # inserta a xs)\"\n\nvalue \"inserta 3 [2,5,1,7] = [2,3,5,1,7]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n\n     ordena :: int list \u21d2 int list\n  tal que (ordena xs) es la lista obtenida ordenando xs por inserci\u00f3n. \n  Por ejemplo, \n     ordena [3,2,5,3] = [2,3,3,5]\n  ------------------------------------------------------------------ *}\n\nfun ordena :: \"int list \u21d2 int list\" where\n  \"ordena []     = []\"\n| \"ordena (x#xs) = inserta x (ordena xs)\"\n\nvalue \"ordena [3,2,5,3] = [2,3,3,5]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 3. Definir la funci\u00f3n\n     menor :: int \u21d2 int list \u21d2 bool\n  tal que (menor a xs) se verifica si a es menor o igual que todos los\n  elementos de xs.Por ejemplo,  \n     menor 2 [3,2,5] = True\n     menor 2 [3,0,5] = False\n  ------------------------------------------------------------------ *}\n\nfun menor :: \"int \u21d2 int list \u21d2 bool\" where\n  \"menor a []     = True\"\n| \"menor a (x#xs) = (a \u2264 x \u2227 menor a xs)\"\n\nvalue \"menor 2 [3,2,5] = True\"\nvalue \"menor 2 [3,0,5] = False\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n\n     ordenada :: int list \u21d2 bool\n  tal que (ordenada xs) se verifica si xs es una lista ordenada de\n  manera creciente. Por ejemplo,  \n     ordenada [2,3,3,5] = True \n     ordenada [2,4,3,5] = False \n  ------------------------------------------------------------------ *}\n\nfun ordenada :: \"int list \u21d2 bool\" where\n  \"ordenada []     = True\"\n| \"ordenada (x#xs) = (menor x xs & ordenada xs)\"\n\nvalue \"ordenada [2,3,3,5] = True\" \nvalue \"ordenada [2,4,3,5] = False\" \n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 5. Demostrar que si y es una cota inferior de zs y x \u2264 y,\n  entonces x es una cota inferior de zs.\n  ------------------------------------------------------------------ *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma menor_menor: \n  assumes \"x \u2264 y\"  \n  shows   \"menor y zs \u27f6 menor x zs\"\nusing assms\nby (induct zs) auto\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma menor_menor_2: \n  assumes \"x \u2264 y\"  \n  shows   \"menor y zs \u27f6 menor x zs\"\nproof (induct zs)\n  show \"menor y [] \u27f6 menor x []\" by simp\nnext\n  fix z zs\n  assume HI: \"menor y zs \u27f6 menor x zs\"  \n  show \"menor y (z # zs) \u27f6 menor x (z # zs)\"\n  proof\n    assume sup: \"menor y (z # zs)\"\n    show \"menor x (z # zs)\"\n    proof (simp only: menor.simps(2))\n      show \"x \u2264 z \u2227 menor x zs\"\n      proof\n          have \"x \u2264 y\" using assms .\n          also have \"y \u2264 z\" using sup by simp\n          finally show \"x \u2264 z\" .\n      next\n        have \"menor y zs\" using sup by simp\n        with HI show \"menor x zs\" by simp\n      qed\n    qed\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Demostrar el siguiente teorema de correcci\u00f3n: x es una\n  cota inferior de la lista obtenida insertando y en zs syss x \u2264 y y x\n  es una cota inferior de zs.\n  ------------------------------------------------------------------ *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma menor_inserta:\n  \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\nby (induct zs) auto\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma menor_inserta_2: \n  \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\nproof (induct zs)\n  show \"menor x (inserta y []) = (x \u2264 y \u2227 menor x [])\" by simp\nnext \n  fix z zs\n  assume HI: \"menor x (inserta y zs) = (x \u2264 y \u2227 menor x zs)\"\n  show \"menor x (inserta y (z#zs)) = (x \u2264 y \u2227 menor x (z#zs))\" \n  proof (cases \"y \u2264 z\")\n    assume \"y \u2264 z\"\n    hence \"menor x (inserta y (z#zs)) = menor x (y#z#zs)\" by simp\n    also have \"\u2026 = (x \u2264 y \u2227 menor x (z#zs))\" by simp\n    finally show ?thesis by simp\n  next\n    assume \"\u00ac(y \u2264 z)\"\n    hence \"menor x (inserta y (z#zs)) = \n           menor x (z # inserta y zs)\" by simp\n    also have \"\u2026 = (x \u2264 z \u2227 menor x (inserta y zs))\" by simp\n    also have \"\u2026 = (x \u2264 z \u2227 x \u2264 y \u2227 menor x zs)\" using HI by simp\n    also have \"\u2026 = (x \u2264 y \u2227 menor x (z#zs))\" by auto\n    finally show ?thesis by simp\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Demostrar que al insertar un elemento la lista obtenida\n  est\u00e1 ordenada syss lo estaba la original.\n  ------------------------------------------------------------------ *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma ordenada_inserta:\n  \"ordenada (inserta a xs) = ordenada xs\"\nby (induct xs) (auto simp add: menor_menor menor_inserta)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\nlemma ordenada_inserta_2:\n  \"ordenada (inserta a xs) = ordenada xs\"\nproof (induct xs)\n  show \"ordenada (inserta a []) = ordenada []\" by simp\nnext\n  fix x xs\n  assume HI: \"ordenada (inserta a xs) = ordenada xs\" \n  show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n  proof (cases \"a \u2264 x\")\n    assume \"a \u2264 x\"\n    hence \"ordenada (inserta a (x # xs)) = \n           ordenada (a # x # xs)\" by simp\n    also have \"\u2026 = (menor a (x#xs) \u2227 ordenada (x # xs))\" by simp\n    also have \"\u2026 = ordenada (x # xs)\"  \n      using `a \u2264 x`  by (auto simp add: menor_menor)\n    finally show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n      by simp\n  next\n    assume \"\u00ac(a \u2264 x)\"\n    hence \"ordenada (inserta a (x # xs)) = \n           ordenada (x # inserta a xs)\" by simp\n    also have \"\u2026 = (menor x (inserta a xs) \u2227 ordenada (inserta a xs))\" \n      by simp\n    also have \"\u2026 = (menor x (inserta a xs) \u2227 ordenada xs)\" \n      using HI by simp\n    also have \"\u2026 = (menor x xs \u2227 ordenada xs)\" \n      using `\u00ac(a \u2264 x)` by (simp add: menor_inserta)\n    also have \"\u2026 = ordenada (x # xs)\" by simp\n    finally show \"ordenada (inserta a (x # xs)) = ordenada (x # xs)\" \n      by simp\n  qed\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 7. Demostrar que, para toda lista xs, (ordena xs) est\u00e1\n  ordenada. \n  ------------------------------------------------------------------ *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\ntheorem ordenada_ordena:\n  \"ordenada (ordena xs)\"\nby (induct xs) (auto simp add: ordenada_inserta)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\ntheorem ordenada_ordena_2:\n  \"ordenada (ordena xs)\"\nproof (induct xs) \n  show \"ordenada (ordena [])\" by simp\nnext\n  fix x xs\n  assume \"ordenada (ordena xs)\" \n  then have \"ordenada (inserta x (ordena xs))\" \n    by (simp add: ordenada_inserta)  \n  then show \"ordenada (ordena (x # xs))\" by simp\nqed\n\ntext {*  \n  --------------------------------------------------------------------- \n  Nota. El teorema anterior no garantiza que ordena sea correcta, ya que\n  puede que (ordena xs) no tenga los mismos elementos que xs. Por\n  ejemplo, si se define (ordena xs) como [] se tiene que (ordena xs)\n  est\u00e1 ordenada pero no es una ordenaci\u00f3n de xs. \n\n  Para garantizarlo, definimos la funci\u00f3n cuenta.\n  ------------------------------------------------------------------ *}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 8. Definir la funci\u00f3n\n     cuenta :: int list \u21d2 int \u21d2 nat\n  tal que (cuenta xs y) es el n\u00famero de veces que aparece el elemento y\n  en la lista xs. Por ejemplo, \n     cuenta [1,3,4,3,5] 3 = 2\n  ------------------------------------------------------------------ *}\n\nfun cuenta :: \"int list \u21d2 int \u21d2 nat\" where\n  \"cuenta []     y = 0\"\n| \"cuenta (x#xs) y = (if x=y \n                      then Suc (cuenta xs y) \n                      else cuenta xs y)\"\n\nvalue \"cuenta [1,3,4,3,5] 3 = 2\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 9. Demostrar que el n\u00famero de veces que aparece y en \n  (inserta x xs) es \n  * uno m\u00e1s el n\u00famero de veces que aparece en xs, si y = x; \n  * el n\u00famero de veces que aparece en xs, si y \u2260 x; \n  ------------------------------------------------------------------ *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\nlemma cuenta_inserta:\n  \"cuenta (inserta x xs) y =\n   (if x=y then Suc (cuenta xs y) else cuenta xs y)\"\nby (induct xs) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 10. Demostrar que el n\u00famero de veces que aparece y en \n  (ordena xs) es el n\u00famero de veces que aparece en xs.\n  ------------------------------------------------------------------ *}\n\n\u2015 \u2039La demostraci\u00f3n autom\u00e1tica es\u203a\ntheorem cuenta_ordena:\n  \"cuenta (ordena xs) y = cuenta xs y\"\nby (induct xs) (auto simp add: cuenta_inserta)\n\n\u2015 \u2039La demostraci\u00f3n estructurada es\u203a\ntheorem cuenta_ordena_2:\n  \"cuenta (ordena xs) y = cuenta xs y\"\nproof (induct xs)\n  show \"cuenta (ordena []) y = cuenta [] y\" by simp\nnext\n  fix x xs\n  assume HI: \"cuenta (ordena xs) y = cuenta xs y\"\n  show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" \n  proof (cases \"x = y\")\n    assume \"x = y\"\n    have \"cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y\" \n      by simp\n    also have \"\u2026 = Suc (cuenta (ordena xs) y)\" using `x = y` \n      by (simp add: cuenta_inserta) \n    also have \"\u2026 = Suc (cuenta xs y)\" using HI by simp\n    also have \"\u2026 = cuenta (x # xs) y\" using `x = y` by simp\n    finally show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" by simp\n  next\n    assume \"x \u2260 y\"\n    have \"cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y\" \n      by simp\n    also have \"\u2026 = cuenta (ordena xs) y\" using `x \u2260 y` \n      by (simp add: cuenta_inserta) \n    also have \"\u2026 = cuenta xs y\" using HI by simp\n    also have \"\u2026 = cuenta (x # xs) y\" using `x \u2260 y` by simp\n    finally show \"cuenta (ordena (x # xs)) y = cuenta (x # xs) y\" \n      by simp\n  qed\nqed\n\ntext {*\n    Para exportar el c\u00f3digo Haskell de la funci\u00f3n snoc se usa\n*}\n\nexport_code ordena in Haskell \n  module_name OrdInsercion \n  file \"CodigoGenerado\/\"\nend\n<\/pre>\n<p>El segundo de los algoritmos verificados ha sido el de ordenaci\u00f3n por mezcla. La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<\/p>\n<pre lang=\"isar\">\nchapter {* T6b: Verificaci\u00f3n de la ordenaci\u00f3n por mezcla *}\n\ntheory T6b_Verificacion_de_la_ordenacion_por_mezcla\nimports Main\nbegin\n\ntext {*\n  En esta relaci\u00f3n de ejercicios se define el algoritmo de ordenaci\u00f3n de\n  listas por mezcla y se demuestra que es correcto.\n*}\n\nsection {* Ordenaci\u00f3n de listas *}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 1. Definir la funci\u00f3n\n     menor :: int \u21d2 int list \u21d2 bool\n  tal que (menor a xs) se verifica si a es menor o igual que todos los\n  elementos de xs.Por ejemplo,  \n     menor 2 [3,2,5] = True\n     menor 2 [3,0,5] = False\n  ------------------------------------------------------------------ *}\n\nfun menor :: \"int \u21d2 int list \u21d2 bool\" where\n  \"menor a []     = True\"\n| \"menor a (x#xs) = (a \u2264 x \u2227 menor a xs)\"\n\nvalue \"menor 2 [3,2,5] = True\"\nvalue \"menor 2 [3,0,5] = False\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 2. Definir la funci\u00f3n\n     ordenada :: int list \u21d2 bool\n  tal que (ordenada xs) se verifica si xs es una lista ordenada de\n  manera creciente. Por ejemplo,  \n     ordenada [2,3,3,5] = True \n     ordenada [2,4,3,5] = False \n  ------------------------------------------------------------------ *}\n\nfun ordenada :: \"int list \u21d2 bool\" where\n  \"ordenada []     = True\"\n| \"ordenada (x#xs) = (menor x xs & ordenada xs)\"\n\nvalue \"ordenada [2,3,3,5] = True\" \nvalue \"ordenada [2,4,3,5] = False\" \n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 3. Definir la funci\u00f3n\n     cuenta :: int list => int => nat\n  tal que (cuenta xs y) es el n\u00famero de veces que aparece el elemento y\n  en la lista xs. Por ejemplo, \n     cuenta [1,3,4,3,5] 3 = 2\n  ------------------------------------------------------------------ *}\n\nfun cuenta :: \"int list => int => nat\" where\n  \"cuenta []     y = 0\"\n| \"cuenta (x#xs) y = (if x=y \n                      then Suc(cuenta xs y) \n                      else cuenta xs y)\"\n\nvalue \"cuenta [1,3,4,3,5] 3 = 2\"\n\nsection {* Ordenaci\u00f3n por mezcla *}\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 4. Definir la funci\u00f3n\n     mezcla :: int list \u21d2 int list \u21d2 int list\n  tal que (mezcla xs ys) es la lista obtenida mezclando las listas\n  ordenadas xs e ys. Por ejemplo, \n     mezcla [1,2,5] [3,5,7] = [1,2,3,5,5,7]\n  ------------------------------------------------------------------ *}\n\nfun mezcla :: \"int list \u21d2 int list \u21d2 int list\" where\n  \"mezcla [] ys = ys\" \n| \"mezcla xs [] = xs\" \n| \"mezcla (x # xs) (y # ys) = (if x \u2264 y\n                               then x # mezcla xs (y # ys)\n                               else y # mezcla (x # xs) ys)\"\n\nvalue \"mezcla [1,2,5] [3,5,7] = [1,2,3,5,5,7]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 5. Definir la funci\u00f3n\n     ordenaM :: int list \u21d2 int list\n  tal que (ordenaM xs) es la lista obtenida ordenando la lista xs\n  mediante mezclas; es decir, la divide en dos mitades, las ordena y las\n  mezcla. Por ejemplo, \n     ordenaM [3,2,5,2] = [2,2,3,5]\n  ------------------------------------------------------------------ *}\n\nfun ordenaM :: \"int list \u21d2 int list\" where\n  \"ordenaM []  = []\" \n| \"ordenaM [x] = [x]\" \n| \"ordenaM xs = \n     (let mitad = length xs div 2 in\n      mezcla (ordenaM (take mitad xs)) \n             (ordenaM (drop mitad xs)))\"\n\nvalue \"ordenaM [3,2,5,2] = [2,2,3,5]\"\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 6. Sea x \u2264 y. Si y es menor o igual que todos los elementos\n  de xs, entonces x es menor o igual que todos los elementos de xs\n  ------------------------------------------------------------------ *}\n\nlemma menor_menor: \n  \"x \u2264 y \u27f9 menor y xs \u27f6 menor x xs\"\nby (induct xs) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 7. Demostrar que el n\u00famero de veces que aparece n en la\n  mezcla de dos listas es igual a la suma del n\u00famero de apariciones en\n  cada una de las listas\n  ------------------------------------------------------------------ *}\n\nlemma cuenta_mezcla: \n  \"cuenta (mezcla xs ys) n = cuenta xs n + cuenta ys n\"\nby (induct xs ys rule: mezcla.induct) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 8. Demostrar que si x es menor que todos los elementos de\n  ys y de zs, entonces tambi\u00e9n lo es de su mezcla.\n  ------------------------------------------------------------------ *}\n\nlemma menor_mezcla:\n  assumes \"menor x ys\" \n          \"menor x zs\" \n  shows   \"menor x (mezcla ys zs)\"\nusing assms \nby (induct ys zs rule: mezcla.induct) simp_all\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 9. Demostrar que la mezcla de dos listas ordenadas es una\n  lista ordenada. \n  Indicaci\u00f3n: Usar los siguientes lemas\n  \u00b7 linorder_not_le: (\u00ac x \u2264 y) = (y < x)\n  \u00b7 order_less_le:   (x < y) = (x \u2264 y \u2227 x \u2260 y)\n  ------------------------------------------------------------------ *}\n\nlemma ordenada_mezcla:\n  assumes \"ordenada xs\" \n          \"ordenada ys\" \n  shows   \"ordenada (mezcla xs ys)\"\nusing assms \nby (induct xs ys rule: mezcla.induct) \n   (auto simp add: menor_mezcla\n                   menor_menor\n                   linorder_not_le \n                   order_less_le)\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 10. Demostrar que si x es mayor que 1, entonces el m\u00ednimo de\n  x y su mitad es menor que x.\n  ------------------------------------------------------------------ *}\n\nlemma min_mitad: \n  \"1 < x \u27f9 min x (x div 2::int) < x\"\nby simp\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 11. Demostrar que si x es mayor que 1, entonces x menos su\n  mitad es menor que x. \n  ------------------------------------------------------------------ *}\n\nlemma menos_mitad: \n  \"1 < x \u27f9 x - x div (2::int) < x\"\nby arith\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 11. Demostrar que (ordenaM xs) est\u00e1 ordenada.\n  ------------------------------------------------------------------ *}\n\ntheorem ordenada_ordenaM:\n  \"ordenada (ordenaM xs)\"\nby (induct xs rule: ordenaM.induct) \n   (auto simp add: ordenada_mezcla)\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 12. Demostrar que el n\u00famero de apariciones de un elemento en\n  la concatenaci\u00f3n de dos listas es la suma del n\u00famero de apariciones en\n  cada una.\n  ------------------------------------------------------------------ *}\n\nlemma cuenta_conc: \n  \"cuenta (xs @ ys) x = cuenta xs x + cuenta ys x\"\nby (induct xs) auto\n\ntext {*  \n  --------------------------------------------------------------------- \n  Ejercicio 13. Demostrar que las listas xs y (ordenaM xs) tienen los\n  mismos elementos.\n  ------------------------------------------------------------------ *}\n\ntheorem cuenta_ordenaM: \n  \"cuenta (ordenaM xs) x = cuenta xs x\"\nby (induct xs rule: ordenaM.induct) \n   (auto simp add: cuenta_mezcla \n                   cuenta_conc [symmetric])\nend\n<\/pre>\n<p>Finalmente, se ha dejado conmo tarea el estudio del algoritmo eficiente de ordenaci\u00f3n por mezcla de GHC que se describe en el art\u00edculo <a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-012-9260-7\">Proof pearl: A mechanized proof of GHC\u2019s mergesort<\/a> y cuya correspondiente teor\u00eda es <a href=\"https:\/\/www.isa-afp.org\/entries\/Efficient-Mergesort.html\">Efficient mergesort<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de Razonamiento autom\u00e1tico se ha estudiado c\u00f3mo verificar con Isabelle\/HOL la correcci\u00f3n de distintos algoritmos de ordenaci\u00f3n. El primero de los algoritmos verificados ha sido el de ordenaci\u00f3n por inserci\u00f3n. La correspondiente teor\u00eda Isabelle\/HOL se muestra a continuaci\u00f3n<\/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":[322],"tags":[144,323],"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\/6408"}],"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=6408"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6408\/revisions"}],"predecessor-version":[{"id":6409,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6408\/revisions\/6409"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6408"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6408"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6408"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}