#	Pagina
attuale pagina	/open-h2020/projects/203249/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - LIPA (A unified theory of finite-state recognisability)

Teaser

Summary

The main goal of the project is to produce a unified theory of finite state devices which recognise properties of words, trees, graphs, etc. The literature contains a wide array of results on this topic, but a unifying framework is lacking. The project proposes such a framework, using monads and Eilenberg-Moore algebras, which are concepts known from category theory. The main goal of the project is to use monads and their algebras to understand finite state devices in contexts where they are not properly understood, and to place this understanding inside a uniform framework. Two specific areas of focus for the project are: (a) finite state devices which process graphs and trees; and (b) transductions, i.e. devices which produce outputs, like words or trees, as opposed to just yes/no answers.

Work performed

\"The main achievements of the project have been, so far:
(1) A proof of Courcelle\'s conjecture, which shows that for graph languages of bounded treewidth, recognisability by algebras conicides with definability in logic. This extends to graphs a correspondence which was already known for words and trees (finite and infinite), following the pioneering work of Buchi and Rabin in the 1960s. Courcelle\'s conjecture was a major open problem in algebraic language theory.
(2) The introduction of a new class of string-to-string transducers, called the polyregular function. This class admits multiple equivalent descriptions, including automata, functional programs, imperative programs and logic, and has many closure properties. Polyregular functions are a natural candiate for the \"\"regular\"\" functions of polynomial size increase.
(3) The analysis of a probabilistic extension of monadic second-order logic over infinite trees, which contains a quantifier that says \"\"a property Ï† of branches in the infinite tree is satisfied almost surely, in the sense of probability\"\". The analysis explains the border of decidability: when only weak sets can be quantified, the logic is decidable, but when infinite sets can be quantified, the logic becomes undecidable.\"

Final results

\"The two main contributions of the project so far are:
(1) A proof of Courcelle\'s conjecture, which shows that for graph languages of bounded treewidth, recognisability by algebras conicides with definability in logic. This extends to graphs a correspondence which was already known for words and trees (finite and infinite). Courcelle\'s conjecture was a major open problem in algebraic language theory.
(2) The introduction of a new class of string-to-string transducers, called the polyregular function. This class admits multiple equivalent descriptions, including automata, functional programs, imperative programs and logic, and has many closure properties. It seems that the polyregular functions are the \"\"regular\"\" functions of polynomial size increase.\"