{"id":4865,"date":"2015-04-22T07:43:17","date_gmt":"2015-04-22T05:43:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4865"},"modified":"2015-04-22T07:43:17","modified_gmt":"2015-04-22T05:43:17","slug":"resena-higmans-lemma-and-its-computational-content","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-higmans-lemma-and-its-computational-content\/","title":{"rendered":"Rese\u00f1a: Higman\u2019s lemma and its computational content"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.mathematik.uni-muenchen.de\/~logik\/minlog\/index.php\">Minlog<\/a> sobre combinatoria titulado <a href=\"http:\/\/www.mathematik.uni-muenchen.de\/~schwicht\/papers\/jaeger14\/higman.pdf\">Higman\u2019s lemma and its computational content<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www.mathematik.uni-muenchen.de\/~schwicht\/\">Helmut Schwichtenberg<\/a> (de la Univ. de Munich en Alemania),<\/li>\n<li><a href=\"http:\/\/cs.swan.ac.uk\/~csmona\/\">Monika Seisenberger<\/a> (de la Univ. de Swansea en el Reino Unido) y<\/li>\n<li>Franziskus Wiesnet.<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  Higman\u2019s Lemma is a fascinating result in infinite combinatorics, with manyfold applications in logic and computer science. It has been proven several times using different formulations and methods. The aim of this paper is to look at Higman\u2019s Lemma from a computational and comparative point of view. We give a proof of Higman\u2019s Lemma that uses the same combinatorial idea as Nash-Williams\u2019 indirect proof using the so-called minimal bad sequence argument, but which is constructive. For the case of a two letter alphabet such a proof was given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary well-quasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of G\u00f6del\u2019s system T) expressing its computational content.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Minlog sobre combinatoria titulado Higman\u2019s lemma and its computational content. Sus autores son Helmut Schwichtenberg (de la Univ. de Munich en Alemania), Monika Seisenberger (de la Univ. de Swansea en el Reino Unido) y Franziskus Wiesnet. Su resumen es Higman\u2019s Lemma is a fascinating result in&#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":[100],"tags":[245,285],"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\/4865"}],"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=4865"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4865\/revisions"}],"predecessor-version":[{"id":4866,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4865\/revisions\/4866"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4865"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4865"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4865"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}