{"id":1469,"date":"2018-01-17T12:47:03","date_gmt":"2018-01-17T11:47:03","guid":{"rendered":"https:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=1469"},"modified":"2018-07-06T08:58:38","modified_gmt":"2018-07-06T06:58:38","slug":"msol-and-higher-order-computation","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/lipa\/lipa-summer-school-2018-june-25-29\/msol-and-higher-order-computation","title":{"rendered":"MSOL and higher-order computation"},"content":{"rendered":"<p>This one of the courses at the\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/lipa\/lipa-summer-school-2018-june-25-29\">Lipa Summer School<\/a>.<\/p>\n<h4><a href=\"http:\/\/www.labri.fr\/perso\/igw\/\">Igor Walukiewicz<\/a><\/h4>\n<h4>MSOL and higher-order computation<\/h4>\n<p>Slides:\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/upload\/pdf-lipa18-intro.pdf\">intro<\/a>\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/upload\/pdf-lipa18-finite-mc.pdf\">finite-mc<\/a>\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/upload\/pdf-lipa18-lambda.pdf\">lambda<\/a>\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/upload\/pdf-lipa18-pushdowns-mc-1.pdf\">pushdowns-mc<\/a>\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/upload\/pdf-lipa18-gfp-model.pdf\">gfp-model<\/a>\u00a0<a href=\"https:\/\/www.mimuw.edu.pl\/~bojan\/upload\/lipa18-ranked-lambda.key.pdf\">ranked-lambda<\/a><\/p>\n<p>A tree can represent all possible computations of a machine. For example, all computations of a finite automaton form a regular tree whose branching depends on the input letters. Rabin&#8217;s theorem implies that monadic second-order theory of a regular tree is decidable. What about trees generated by other devices?<\/p>\n<p>In this series of lectures, we will present results and techniques for proving decidability of monadic second-order theories of trees generated by pushdown automata, lambda terms, and tree rewriting. These investigations bring intriguing questions about semantics, recognisability, and efficient algorithms for fixpoint<br \/>\ncomputation.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>This one of the courses at the\u00a0Lipa Summer School. Igor Walukiewicz MSOL and higher-order computation Slides:\u00a0intro\u00a0finite-mc\u00a0lambda\u00a0pushdowns-mc\u00a0gfp-model\u00a0ranked-lambda A tree can represent all possible computations of a machine. For example, all computations of a finite automaton form a regular tree whose branching depends on the input letters. Rabin&#8217;s theorem implies that monadic second-order theory of a regular [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":1441,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-1469","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1469"}],"collection":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/comments?post=1469"}],"version-history":[{"count":4,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1469\/revisions"}],"predecessor-version":[{"id":1550,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1469\/revisions\/1550"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/1441"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=1469"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}