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

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - DuaLL (Duality in Formal Languages and Logic - a unifying approach to complexity and semantics)

Teaser

Summary

Dualities between algebraic and topological structure are pervasive in mathematics, and toggling back and forth between them has often been associated with important breakthroughs. The main objective of this project is to bring this important tool to bear on a number of subjects in theoretical computer science thereby advancing, systematising, and unifying them.

One subject of focus is the search for robust extensions of the theory of regular languages. A powerful technical tool for classifying regular languages and proving decidability results is Eilenberg-Reiterman theory, which assigns classes of finite monoids or single profinite algebras to classes of languages. The goals of this project in this direction are to:
- (Objective 1) Develop an Eilenberg-Reiterman theory beyond regular languages with the goal of obtaining new tools and separation results for Boolean circuit classes, an active area in the search for lower bounds in complexity theory.
- (Objective 2) Systematise and advance the search for robust generalisations of regularity to other structures such as infinite words, finite and infinite trees, cost functions, and words with data.

The second subject of focus is the development of duality theoretic methods for logics with categorical semantics. We want to approach the problem incrementally:
- (Objective 3) View duality for categorical semantics through a spectrum of intermediate cases going from regular languages over varying alphabets, Ghilardi-Zawadowski duality for finitely presented
Heyting algebras, and the Bodirsky-Pinsker topological Birkhoff theorem to Makkaiâ€™s, Awodey and Forssellâ€™s, and Coumansâ€™ first-order logic duality, thus unifying topics in semantics and formal languages.

This project may provide new tools in the search for lower bounds in complexity theory, which is an important issue in that it informs us of the limits and nature of computational processes. It may also provide tools for semantic modeling of computational processes with binding of variables in a modular setting, which is important for the development of flexible and sophisticated modern computer programs. Finally, since the mathematical tools behind these two developments are one and the same, it may contribute to the unification of the semantic and the algorithmic study of the foundations of computer science.

Work performed

Several papers have been written which provide foundations for the project. These provide, among other, a full account of the duality theoretic underpinnings of syntactic recognizers and the ensuing Eilenberg-Reiterman theory for regular languages and of the theory of completions in the abstract setting of Pervin spaces and its application to obtaining characterizations by inequalities for lattices of languages (regular or not).
Specific progress on the individual objectives have also been achieved. In particular, under Objective 1, a proof of concept, establishing the feasibility of equational characterizations, has been obtained. And, in a series of papers, accepted at ICALP 2016, LICS 2017, and CSL 2017, significant progress on Objective 1 has been made in the form of constructions of topo-algebraic recognizers which mirror the action of quantifiers, such as classical first-order quantifiers and modular quantifiers. In addition, new connections with finite model theory have been identified and are being investigated. This includes new collaborations with NeÅ¡etÅ™il and Ossona de Mendez as well as with a project under construction by Abramsky and Dawar.
Under Objective 2, contributions include the definition of new categorical constructions that are suitable for the description of minimizable classes of recognizers, and, as a central application, a class of automata that can be named â€œhybrid-set-vector automataâ€, that generalizes both the class of finite deterministic automata and the class of automata weighted over a field while possessing minimal recognizers for languages. This class of automata is an important contribution to automata theory in itself, and has been obtained by design thanks to a cross fertilisation between category theory and automata theory. In addition this work has led to refinements of known results concerning minimisation of automata thanks to the deeper categorical understanding.
Under Objective 3, several of the intermediate cases in our bottom-up approach to duality methods for logics with binders have been tackled. In particular, the work on topo-algebraic recognizers which mirror the action of quantifiers in logic on words mentioned under Objective 1, work by associated PhD student Luca Reggio and Sam van Gool on the Ghilardi-Zawadowski duality for finitely presented Heyting algebras, and work by Gehrke and Pinsker on a common generalization of the Bodirsky-Pinsker topological Birkhoff theorem and the Reiterman Theorem for finite algebras complete all the intermediate goals of Objective 3 of the proposed project. Contributions to full semantics for logics with binders include a general form of the Isbell duality for a certain type of refinement systems, an embedding of the classical categorical semantics structures known as hyperdoctrines in a larger bifibration with the bicategory of distributors (or profunctors) as basis. In addition, a new notion of higher-order parity automaton which is designed to recognize languages of infinitary simply-typed Î»-terms has been introduced. Finally, to make the move into the full categorical setting of semantics for quantifier logics, new team members from higher category theory have been recruited and a workshop on topos theory has been held.

Apart from the standard dissemination of research results, additional effort has been made to disseminate the results and the nature of the project to as wide an audience as possible. Thus, the project quicked off with a workshop on Duality Theory at the Dagstuhl center. Also, an invited tutorial at the Logic in Computer Science (LICS) conference in July 2016 provided an introduction and overview of the duality theoretic components of the project and how they connect with other topics in semantics. Further, two papers, that provide an invitation and introduction to Objective 1 and Objective 2, respectively, have appeared as invited columns (on complexity and semantics, respectively) of the ACM SIGLOG News of Ap

Final results

The majority of the results described above move significantly beyond the state of the art, however, it is too early to assess the impact of these results in a larger sense.