Higher-Order Logics and Structures

From specifying programs to querying databases, computer science is rife with phenomena whose understanding requires close attention to the interaction between formal languages and structures. Fundamentally important questions to this regard are: a) Is the language at hand expressive enough as to allow us to specify the required queries? b) Can we get an answer to our queries in a reasonable amount of time? For instance, if we want to know whether there is a flight between two cities with at most one stopover and our language is first-order logic, then the answer to (a) and (b) is yes in both cases. Now if we want to know whether there is a flight with any number of stopovers, then the answer to (a) is negative already since first-order logic is not expressive enough as to specify this latter query. Fortunately, there are many extensions of fist-order logic which can express this last query and whose formulae can be evaluated in a reasonable amount of time. But for many fundamentally important queries this is not the case. This has been the source of intensive studies in finite model theory and descriptive complexity, which can be defined as the study of the interaction between logics (formal languages), finite structures (databases) and its complexity. In the last thirty years, this area of research has produced several of the most striking, fundamental and deepest results in computer science. However, there are still many fundamental questions which are open. One of those questions is whether there are ways of taking advantage of highly expressive languages such as higher-order logics without paying the high cost that they have in terms of time of evaluation of expressions. This question is of utmost importance not only from a theoretical, but also from a practical perspective. Even for the type of queries common in the industry, which in general do not strictly require the high expressive power of higher-order logics, these logics have the potential of greatly simplifying the task of writing queries by allowing more natural and higher- level descriptions of the problems at hand. In this proposal, we aim to investigate this problem and propose three concrete lines of research that can open the door for the use of highly expressive languages in the industry. The first line aims at using an engineering approach to identifying and classifying concrete, tractable cases that enable the use of rich and expressive higher-order language constructs to simplify the expression of queries. The second line of work aims at developing tractable higher-order languages to model and query semantic Web data. Nested collections are naturally modelled in logic as higher order structures. This makes higher-order languages a natural choice to manipulate such collections. The third and final line of the research proposed aims at gaining a better understanding of which features of higher-order logics have a real impact on their expressive power and complexity. This line focuses on fundamental theoretical questions regarding logics over finite structures.

From specifying programs to querying databases, computer science is rife with phenomena whose understanding requires close attention to the interaction between formal languages and structures. This has been the source of intensive research in finite model theory and descriptive complexity, which can be defined as the study of the interaction between logics (formal languages), finite structures (databases) and its complexity. In the last forty years, this area of research has produced several of the most striking, fundamental and deepest results in computer science. Nevertheless, many open questions remain. Within this general framework the focus of this project is on higher-order logics. These highly expressive languages are rightfully gaining relevance in diverse areas of computer sciences, including, among others, databases, knowledge representation in AI, rigorous methods for software specification, and automated theorem provers. A key research problem on this regard is to find ways of exploiting in practice the natural high-levels of expressibility of these languages. The main challenge lies in the high intractability associated to standard higher-order logics. It is then important to deeply understand the impact of different features of higher-order logics on their descriptive complexity, identifying good compromises between expressive power and tractability. The main results of this project concern this problem. The first key result consists in the definition of novel and natural fragments of higher-order logics, showing interesting collapsing theorems, sometimes unexpected, on their expressive power. Among other things, it is constructively shown that the increase in the expressive power of the higher-order logics is determined by the extra space provided by the higher-order relations, not by their level of nesting. From a practical perspective these fragments enable clear and concise definitions of problems that, when expressed in lower-order logics, result in extremely complicated sentences which require intricate encodings. The second key result introduces restricted second-order and fixed-point logics which give elegant and precise descriptive characterization of sub1linear complexity classes, most prominently of non-deterministic and deterministic polylogarithmic time. The relevance of these logics and complexity classes is demonstrated by several problems in database theory, proving lower bounds for their expressibility and complexity. Sublinear query languages are of course extremely relevant when dealing with big data. Additionally, this project contributes to the development of higher-order languages to Model and query semantic Web data, systematically refine high-level systems design and analysis tasks, characterize and verify properties of abstract state machines, and define complex algorithms in terms of declaratively specified computations at a high level of abstraction.