{"id":5010,"date":"2015-09-10T09:00:00","date_gmt":"2015-09-10T07:00:00","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5010"},"modified":"2015-09-10T09:00:00","modified_gmt":"2015-09-10T07:00:00","slug":"resena-decreasing-diagrams-for-church-rosser-modulo","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-decreasing-diagrams-for-church-rosser-modulo\/","title":{"rendered":"Rese\u00f1a: Decreasing diagrams for Church-Rosser modulo"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre reescritura titulado <a href=\"http:\/\/afp.sourceforge.net\/entries\/Decreasing-Diagrams-II.shtml\">Decreasing diagrams for Church-Rosser modulo<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/bf3\/index.php\">Bertram Felgenhauer<\/a> (del <a href=\"http:\/\/cl-informatik.uibk.ac.at\/\">Computational Logic Research Group<\/a> en la <a href=\"http:\/\/bit.ly\/1ELGKOo\">Universidad de Innsbruck<\/a>, Austria).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/bf3\/publications\/2013-BFVvO-RTA.pdf\">Felgenhauer and van Oostrom (RTA 2013)<\/a>. The theory also provides important specializations, in particular <a href=\"http:\/\/www.phil.uu.nl\/~oostrom\/publication\/talk\/rta170708.pdf\">van Oostrom\u2019s conversion version (TCS 2008)<\/a> of decreasing diagrams.<\/p>\n<p>  We follow the development described in <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/bf3\/publications\/2013-BFVvO-RTA.pdf\">1<\/a>: Conversions are mapped to Greek strings, and we prove that whenever a local peak (or cliff) is replaced by a joining sequence from a locally decreasing diagram, then the corresponding Greek strings become smaller in a specially crafted well-founded order on Greek strings. Once there are no more local peaks or cliffs are left, the result is a valley that establishes the Church-Rosser modulo property.<\/p>\n<p>  As special cases we provide non-commutation versions and the conversion version of decreasing diagrams by van Oostrom <a href=\"http:\/\/www.phil.uu.nl\/~oostrom\/publication\/talk\/rta170708.pdf\">3<\/a>. We also formalize extended decreasingness <a href=\"http:\/\/www.jaist.ac.jp\/~hirokawa\/publications\/10ijcar.pdf\">2<\/a>.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <a href=\"http:\/\/afp.sourceforge.net\/index.shtml\">The Archive of Formal Proofs<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/afp.sourceforge.net\/browser_info\/current\/AFP\/Decreasing-Diagrams-II\/index.html\">aqu\u00ed<\/a>.<\/p>\n<p>Este art\u00edculo puede servir de lectura complementaria en los cursos de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a>, <a href=\"http:\/\/www.cs.us.es\/cursos\/rac\/\">Razonamiento asistido por ordenador<\/a> y <a href=\"http:\/\/www.cs.us.es\/~mjoseh\/LCyTM-15\">L\u00f3gica computacional y teor\u00eda de modelos<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre reescritura titulado Decreasing diagrams for Church-Rosser modulo. Su autor es Bertram Felgenhauer (del Computational Logic Research Group en la Universidad de Innsbruck, Austria). Su resumen es This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van&#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":[144,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\/5010"}],"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=5010"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5010\/revisions"}],"predecessor-version":[{"id":5011,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5010\/revisions\/5011"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5010"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5010"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5010"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}