Automatic Structures

这个项目解决了算法模型理论领域的问题。总体目标包括更好地理解有限可呈现的无限结构的模型理论和算法特性，开发无限结构的算法处理新方法，在计算机科学的几个领域中的应用，以及解决该领域的一些基本理论问题。更具体地说，这个项目关注的是自动结构。一个结构是自动的，如果它的元素可以用规则语言的单词表示，并且结构的所有关系和功能都可以被同步有限自动机识别。由于自动结构允许对任意一阶公式和某些更强的形式进行有效的（实际上甚至是自动的）评估，并且由于它们在许多基本操作下是封闭的，因此它们为算法模型理论的研究计划提供了一个自然和相关的框架。特别地，我们将解决当前的挑战，超越相对容易理解的单词自动结构的情况，推进-自动和-树自动结构的理论和算法方法。此外，我们的目标是为自动结构建立一个一般和全面的框架，它应该允许解决某些独立于自动表示的特定变体的基本问题。尽管最近在欧米茄-自动结构和注入与非注入表示方面取得了相关成就，但为了在欧米茄-树-自动结构方面取得重大进展，目前的方法需要得到丰富和完善。除了研究已建立的自动表示类之外，我们的目标是系统地推广基于这种有限表示的算法处理无限结构的方法。这种方法的进一步动机来自于一个目前仍不正式的问题，即是否每个具有可决定理论的（自然）结构都可以通过有限的（甚至在某种意义上自动的）表示来决定。在Rabin 1969年关于无限二叉树一元理论的经典论文中，这个问题已经以不同的形式被提出。通过这种方式，我们也希望能够更好地理解可决定理论的算法复杂性。

This project adresses questions from the field of algorithmic model theory. The overall goals include a better understanding of the model-theoretic and algorithmic properties of finitely presentable infinite structures, the development of new methods for the algorithmic treatment of infinite structures, towards applications in several areas of computer science, and the solution of some fundamental theoretic problems in this area.More specifically, this project is concerned with automatic structures. A structure is automatic if its elements can be represented by words of a regular language in such a way that all relations and functions of the structure can be recognized by synchronous finite automata. Since automatic structures admit the effective (in fact even automatic) evaluation of arbitrary first-order formulae, and certain stronger formalisms, and since theyare closed under many fundamental operations, they provide a natural and relevant framework for the research programme of algorithmic model theory.In particular we will address the current challenge to advance, beyond the relatively well-understood case of word-automatic structures, the theory and algorithmic methods for omega-automatic and omega-tree-automatic structures. In addition we aim at a general and comprehensive framework for automatic structures that should permit to solve certain fundamental questions independent of a specific variant of automatic presentations. Although relevant achievements have recently been obtained on omega-automatic structures and on injective versus non-injective presentations, the current methodology needs to be enriched and refined for making significant progress for omega-tree-automatic structures.Beyond the study of the established classes of automatic presentations we aim at a systematic generalization of the approach to handle infinite structures algorithmically on the basis of such finite presentations.A further motivation for this approach comes from the, at present still informal, question of whether every (natural) structure with a decidable theory can be decided by means of a finite (or even in some sense automatic) presentation. In a differern form this question has already been raised in Rabin's classical paper from 1969 on the monadic theory of the infinite binary tree. In this way, we also hope to provide a better understanding of the algorithmic complexity of decidable theories.