Frontiers of recognizability – FREC

One of the challenges of computer science is to manipulate objects from an infinite set using finitary means. The central concept that
has emerged in response to this challenge is an algebraic concept of recognizability. It offers unparalleled closure and algorithmic properties, matched with useful expressiveness. The combination of this theory with logic and automata has proved incredibly fruitful.

The goal of this project is to be a driving force behind the extension of the algebraic approach made possible by recent advances. In our
opinion, a new frontier is opening for the study of recognizability. In order to have a concrete work plan in this vast
area, we propose to concentrate on the development on four particular fronts. One of these fronts (Task 2) concerns tree languages: trees
have become a major model in computer science, because of the emergence of XML, by now a standard format of data exchange on the web
but also an underlying structure in databases, and because of their role in verification. The second front (Task 3) concerns languages of
lambda-terms. While they may be represented by trees, lambda-terms are much more than that. They are essential tools in computational linguistics and in semantics, but are not usually studied from the point of view of recognizability. The third front (Task 4), is the study of automata
with limited counters for word or tree languages. There are surprising connections of these kinds of models with classical questions. The
last front that we want to develop (Task 5), which could well be termed foundational, aims at developing algebraic and topological
tools for the other tasks based on the emergence of the new concepts and completely new results which have thoroughly revolutionized the algebraic theory of recognizable languages of finite words.

The project will drive its impetus from recent important developments on all four fronts. On the most historically established of them, Task
5, such a development is the discovery of the role of the Stone duality and of the power of profinite equations. Research on Task 2
has also a relatively long history, but recent algebraic approaches have contributed to a new development of the field. The remaining
Tasks 3 and 4 offer a very novel, promising and largely unexplored potential. First results in these two new subjects justify in our
opinion their prominent place in this project. We believe that the interaction of tasks at different levels of maturity, can offer enormous benefits to all of them.

In the domain of trees, we expect to get new insights into expressive power of tree formalisms. For example, one of the main open problems
in the field is to find a decidable characterization of first-order logic over trees. Another challenge is to understand the power of
having an ad-hoc ordering of trees: an order that is a natural consequence of the way the trees are stored or streamed.

In the domain of lambda-terms, we will study the notion of recognizability, recently introduced. The algebraic and topological tools we will
develop will allow us to connect to the studies in semantics of programming languages and linguistics. This approach has already given
very interesting insights, like for example, an easy proof of decidability of fourth-order matching. We also want to make a step to infinitary
lambda-terms, and look at the theory of recursive programme schemes from a new perspective.

In the domain of cost functions we plan to study their algorithmic theory, giving optimal constructions for key operations of the theory.
One of our main aims is to extend this theory to cost functions over trees. Recent results have shown that over words this theory allows to
easily derive some classical results, such as decidability of the star-height problem. An extension of this theory to infinite trees would solve, among others, a major long standing problem in automata theory: the Mostowski hierarchy problem.