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.

No additional funding sources recorded.