Foundations of the Finite Model Theory of Concatenation

本提案的主题是有限模型连接理论（FC），这是一种新的逻辑，结合了理论计算机科学的两个不同子领域的方法，在信息提取和数据库理论中有直接应用，并最终应用于处理文本数据搜索或过滤的所有领域。文本数据在现代生活中无处不在：无论我们是在处理书籍、报告、电子邮件、社交媒体、电子表格，甚至是HTML文档或日志文件，大量的信息都是以字母序列的形式表示的。信息提取（Information extraction， IE）处理的是从这些数据中提取相关信息的问题。其中一个模型是文档生成器，这是一种用于IE的关系框架，可以理解为像查询数据库一样查询文本。由于与关系查询相似，文档生成器最近成为数据库理论中的一个热门话题。数据库理论使用有限模型理论（FMT）的方法，这是计算机科学中逻辑的一个分支学科。FMT为关系数据库提供了灵感，在过去的50年里，这两个领域一直保持着密切的联系。特别重要的是对查询进行有效评估的方法，以及对某些类型的查询能表达什么和不能表达什么的深刻见解。FMT中的每个结果也是数据库上的结果，因为逻辑公式和数据库查询之间存在直接的一对一对应关系：每个数据库查询对应一个逻辑公式，每个逻辑公式对应一个数据库查询。这对于关系数据库来说是很容易理解的，但是它确实直接转换为文档生成器的文本设置：对于文档生成器建模，规范的fmt文本方法显然太弱了。但是为了能够评估、优化和比较文本上的查询，为文档生成器提供这个功能将非常有用。作为朝这个方向迈出的第一步，之前的研究使用了“连接理论”，这是一种不同于理论计算机科学的另一个分支学科——词组合学（CoW）的逻辑，研究文本中的模式。但这种逻辑对应的是无限模型理论，而不是有限模型理论，这使得FMT中的许多有用技术无法使用。为了解决这一问题，提出了新的逻辑FC，将CoW的串联理论与FMT的有限模型方法相结合。如预备研究所示，FC具有文档扳手所需的表达能力，同时仍然允许使用许多经典的FMT技术。除了与文档生成器的连接之外，FC可以看作是以前使用过的逻辑的自然变体：从fmt的角度来看，FC可以看作是使用字符串相等运算符扩展字符串上的规范一阶逻辑。从cow的观点来看，FC是连接理论的有限模型版本。因此，FC是在文本数据上使用逻辑的基本框架，它可以直接扩展到涵盖其他操作，比如字符串验证中使用的长度约束。预备研究介绍了FC，证明了它具有所需的文档生成器的一对一对应，并表明许多fmt技术可以适应。但是仍然存在许多悬而未决的问题，特别是关于两个最重要的方面：查询的有效评估，以及框架的基本限制——或者，不那么正式地说，哪些查询可以快速评估，应该使用哪些算法，以及这个查询模型中有什么可能？本项目将通过为FC创建坚实的理论基础来缩小这一差距。这将需要新的证明技术，至少要合并来自CoW和FMT的证明技术，或者甚至远远超过它们。最终的目标是FC可以像FMT查询数据库那样查询文本。

The topic of this proposal is the finite model theory of concatenation (FC), a new logic that combines approaches from two different subfields of theoretical computer science and that has direct applications in information extraction and database theory, and eventual applications in all areas that deal with searching in or filtering of textual data.Textual data is everywhere in modern life: No matter whether we are dealing with books, report, emails, social media, spreadsheets, or even HTML documents or log files, a huge amount of information is represented as a sequence of letters.Information extraction (IE) deals with the problem of extracting relevant information from such data. One model for this are document spanners, a relational framework for IE that can be understood as querying text like one would query a database. Due to their similarity to relational queries, document spanners have recently become a trending topic in database theory. Database theory uses methods from finite model theory (FMT), a sub-discipline of logic in computer science. FMT provided the inspiration for relational database, and both fields have maintained a close connection over these last fifty years. Of particular importance are methods for efficient evaluation of queries and deep insights of what can and cannot be expressed with certain types of queries. Every result in FMT is also a result on databases, as there is an immediate one-to-one correspondence between logical formulas and database queries: Every database query corresponds to a logical formula, and every logical formula corresponds to a database query.This is well-understood for relational databases, but it does directly translate to the textual setting of document spanners: The canonical FMT-approaches to text are provably too weak to model document spanners. But to be able to evaluate, optimize, and compare queries on texts, having this for document spanners would be tremendously useful.As first steps in this direction, previous research used "the theory of concatenation", a different logic from combinatorics on words (CoW), another sub-discipline of theoretical computer science, that studies patterns in texts. But this logic corresponds to infinite model theory, not finite model theory, which makes many useful techniques from FMT unavailable.To address this problem, the proposed new logic FC combines the theory of concatenation from CoW with the finite model approach from FMT. As shown in the preparatory research, FC has exactly the required expressive power of document spanners while still allowing the use of many classical FMT techniques. Apart from the connection to document spanners, FC can be seen as a natural variant of the logics that have previously been used: From an FMT-point of view, FC can be seen as extending the canonical first-order logic on strings with a string equality operator. From a CoW-point of view, FC is the finite model version of the theory of concatenation. As such, FC is a fundamental framework for using logic on textual data, and it can directly be extended to cover other operations, like length constraints as they are used in string verification.The preparatory research introduces FC, proves it has the desired one-to-one corresponds to document spanners, and shows that many FMT-techniques can be adapted. But many open questions remain, in particular regarding two of the most important aspects: The efficient evaluation of queries, and the fundamental limitations of the framework -- or, less formally, which queries can be evaluated quickly, which algorithms should be used for this, and what is possible in this querying model?This project will close this gap by creating a solid theoretical foundation for FC. This will require new proof techniques that at the very least merge those from CoW and FMT, or even go far beyond them. The ultimate goal is that FC will do for querying text what FMT did for databases.