Automatic Structures

本项目涉及算法模型理论领域的问题。总体目标包括更好地理解有限可表示无限结构的模型理论和算法性质，发展无限结构算法处理的新方法，走向计算机科学的几个领域中的应用，以及解决这一领域的一些基本理论问题。如果一个结构的元素可以用正则语言的词来表示，使得该结构的所有关系和功能都可以被同步有限自动机识别，则该结构是自动的。由于自动机结构允许对任意一阶公式和某些更强的形式主义进行有效的(事实上甚至是自动的)求值，并且由于它们在许多基本运算下是封闭的，它们为算法模型理论的研究计划提供了一个自然而相关的框架。特别是，我们将解决当前的挑战，超越相对较好地理解的单词自动结构的情况，推进欧米伽自动和欧米伽树自动结构的理论和算法方法。此外，我们的目标是建立一个全面的自动结构框架，以便能够独立于自动陈述的具体变体解决某些基本问题。虽然最近在omega-Automatic结构和内射与非内射表示方面已经取得了相关的成果，但为了在omega-tree-Automatic结构方面取得重大进展，现有的方法还需要丰富和完善。在研究已有的自动表示类之后，我们的目标是系统地推广基于这种有限表示的算法处理无限结构的方法。该方法的另一个动机来自于目前仍然不正式的问题，即是否每个具有可判定理论的(自然)结构都可以通过有限(或者甚至在某种意义上的自动)表示来确定。在另一种形式中，这个问题已经在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.