树自动机与拟阵的鸽洞类:I

Hlineny 定理表明,当输入限于具有有界分支宽度的 F-可表示拟阵类(其中 F 为有限域)时,拟阵一元二阶逻辑中的任何句子都可在多项式时间内被检验。若一个类中的每个拟阵都能被一棵次立方树分解,使得跨所展示分离集流动的信息量有界,则该类具有有界分解宽度。我们引入拟阵类的鸽洞性质:若一个类的每个具有有界分支宽度的子类也具有有界分解宽度,则该类是鸽洞的。高效鸽洞类具有更强的性质,涉及基集子集上可有效计算的等价关系。我们证明 Hlineny 定理可推广至任意高效鸽洞类。在后续论文中,我们利用这些思想将 Hlineny 定理推广至基本横截拟阵、格路拟阵、双圆拟阵以及 H-增益图拟阵类,其中 H 为任意有限群。我们还给出了可由树自动机描述的超图族的刻画:一个族由树自动机定义当且仅当它具有有界分解宽度。此外,我们证明若一个拟阵类具有鸽洞性质且可用一元二阶逻辑定义,则其任何具有有界分支宽度的子类都具有可判定的一元二阶理论。