Foundations of the Finite Model Theory of Concatenation

本提案的主题是连接的有限模型理论（FC），这是一种新的逻辑，它结合了理论计算机科学两个不同子领域的方法，并直接应用于信息提取和数据库理论，最终应用于处理文本数据搜索或过滤的所有领域。文本数据在现代生活中无处不在：无论我们处理的是书籍、报告、电子邮件、社交媒体、电子表格，还是HTML文档或日志文件，大量的信息都表示为一系列字母。信息提取（IE）处理的是从这些数据中提取相关信息的问题。其中一个模型是文档生成器，这是IE的一个关系框架，可以理解为像查询数据库一样查询文本。由于它们与关系查询的相似性，文档空间查询最近成为数据库理论中的一个热门话题。数据库理论使用有限模型理论（FMT）的方法，这是计算机科学中逻辑的一个子学科。FMT为关系数据库提供了灵感，这两个领域在过去的50年里保持着密切的联系。特别重要的是有效评估查询的方法，以及对某些类型的查询可以表达什么和不可以表达什么的深刻见解。FMT中的每个结果也是数据库上的结果，因为逻辑公式和数据库查询之间存在直接的一一对应关系：每个数据库查询对应于一个逻辑公式，每个逻辑公式对应于一个数据库查询。这对于关系数据库来说是很好理解的，但它确实直接转换为文档空间的文本设置：规范的FMT方法文本是证明太弱，模型的文档空间。但是，为了能够评估、优化和比较文本查询，将其用于文档空间将是非常有用的。作为这个方向的第一步，以前的研究使用了“连接理论”，这是一种与词组合学（CoW）不同的逻辑，CoW是理论计算机科学的另一个子学科，研究文本中的模式。但这种逻辑对应的是无限模型理论，而不是有限模型理论，这使得FMT中的许多有用技术无法使用。正如在预备研究中所示，FC完全具有所需的文档空间的表达能力，同时仍然允许使用许多经典的FMT技术。除了与文档空间的连接之外，FC可以被看作是以前使用的逻辑的自然变体：从FMT的角度来看，FC可以被看作是用字符串相等运算符扩展了字符串上的规范一阶逻辑。从牛的观点来看，FC是连接理论的有限模型版本。因此，FC是一个基本的框架，用于使用逻辑的文本数据，它可以直接扩展到涵盖其他操作，如长度约束，因为它们被用于字符串verifiation.The预备研究介绍FC，证明它有所需的一对一对应的文档spatial，并表明，许多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.