关系不动点逻辑的描述性复杂性及其表达性的研究

RRR可在www.sciencedirect.com在线获取理论计算机科学电子笔记332（2017）113-130www.elsevier.com/locate/entcs通过具有关系不动点和捕获结果的逻辑来描述决策问题的复杂性1Marcia Farias2，安娜特蕾莎·马丁斯3法国大学计算机系P.O. Box 12166，Fortaleza，CE，巴西Francicleber Ferreira4FederalUniversityofCear'a， Campusde菜ad'a63902-580，菜ad'a，CE，Brazil摘要在这项工作中，我们推广了经典的不动点逻辑使用关系，而不是运营商，以捕捉非决定性的概念。 基本思想是我们在关系中使用循环而不是函数的固定点，也就是说，如果对（X，X）属于，则X是关系的固定点。 本文引入了不等式关系的初始不动点的概念以及相关的操作员RIFP。我们用RIFP表示一阶逻辑，其中包含推理关系定点运算符RIFP，并证明它使用到二阶逻辑的转换来捕获多项式层次。我们也考虑片段RIFP1，限制是RIFP操作符最多只能应用一次。我们证明了RIFP1捕获了NP类，并将我们的逻辑与所提出的非确定性定点逻辑进行了比较[4]阿比特布尔，维阿努和瓦尔迪。关键词：描述性复杂性，不动点逻辑，关系不动点逻辑，表达性。1介绍通过逻辑对复杂性类的刻画是描述复杂性的中心主题[17]。这样的刻画表明，某些逻辑中的句子定义了属于一个特定的有限结构上的决策问题1这项工作得到了CAPES（DS）、CNPq（305980/2013-0，474821/2012-9）、CAPES/CNPq（552578/2011-8）、CAPES（PROCAD/NF 789/2010）和FUNCAP的部分支持。2电子邮件：roberta@lia.ufc.br3电子邮件：ana@lia.ufc.br4电子邮件：fran@lia.ufc.brhttp://dx.doi.org/10.1016/j.entcs.2017.04.0081571-0661/© 2017作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。114M. Farias等人/理论计算机科学电子笔记332（2017）113复杂性类，反之亦然，也就是说，这个复杂性类中的问题可以通过语言的句子来定义。这种结果在有限模型理论[9]和复杂性理论[20]之间建立了桥梁，并开辟了使用一个领域的方法和结果来解决另一个领域的问题的可能性。它还支持逻辑资源之间的关系（例如，量化、变量数和计算资源（例如，处理器的数量、不确定性、交替、时间、空间等）。Codd[8]提出的数据库的关系模型，明确了数据库理论与有限模型理论之间的数据库可以被看作是有限的结构，查询语言可以被看作是逻辑语言[1]。对逻辑语言的兴趣迅速增长，因为这种语言及其相关的语义为数据库理论提供了强大的理论背景，特别是在查询处理方面，并且可以应用大量的模型论技术反过来，这种对数据库逻辑方法的兴趣促进了有限模型理论的深入发展。查询语言的一个明显候选者是一阶逻辑（FO）。一阶逻辑是在上个世纪发展起来的，数学的逻辑基础在这种情况下，无限结构起着重要的作用，事实上，一阶逻辑的模型论方法依赖于结构可以无限的事实[7，15]。 虽然FO非常适合数学推理，但它对有限模型的表达能力相当有限。许多问题，例如判定一个图是否连通，不能用FO来表达，即使只限于有限结构。这些限制来自于FO不能表达归纳定义的事实。这种缺乏表现力的情况通过引入固定点运算符来改善FO的表现力而得到了弥补。Aho和Ullman[2]引入了扩展关系代数的思想，关系代数基本上是代数形式的一阶逻辑，具有固定点运算符。钱德拉和哈雷尔[6]遵循了这个想法，产生了一阶逻辑的最小固定点扩展运算符，称为最小固定点逻辑LFP。算子是一个函数F：P（A）→ P（A）。当F是单调算子（即X<$Y<$F（X）<$F（Y））时，它有一个最小不动点lfp（F）。最小不动点逻辑用表达式扩展了一阶逻辑的语言，这些表达式定义了适当选择的单调算子的最小不动点（参见第2节中的精确定义）。最小固定点逻辑严格来说比FO更有表现力。例如，像连通性和可达性这样的图形属性可以用LFP语句来表达。其他固定点逻辑可以通过改变所考虑的运算符的类型和所选择的固定点的类型给定一个具有某种逻辑的句子，其有限模型的集合定义了一个决策问题。一旦我们用某种语言的句子来表达决策问题，直接的问题是：这些问题的复杂性是什么这个问题已经有几个逻辑回答了，见[17]。例如，一阶逻辑对应于时间-时间层次。第一个与逻辑表达M. Farias等人/理论计算机科学电子笔记332（2017）113115功率和计算复杂度是著名的费金根据Fagin定理，二阶逻辑的存在片段精确地定义了NP（非确定性多项式时间，见[20]）中的问题，并且它被Stockmeyer[21]用来表明二阶逻辑对应于多项式层次。由于Bu？chi[5]的一个较早的结果表明，字符串上的一元二阶逻辑精确地定义了正则语言类LFP的表达能力介于一阶逻辑和存在二阶逻辑之间。在有序结构类上，LFP对应于可以在多项式时间内解决的问题类P中的决策问题[17]。大多数固定点逻辑都是按照上面为LFP的情况所勾画的方式定义的。特别是，它们使用运算符（函数）及其固定点来定义归纳集我们有兴趣扩展这个概念，不仅考虑操作者，但关系。代替函数F：P（A）→ P（A）及其固定点，我们考虑关系R <$P（A）×P（A）及其循环，即X使得（X，X）∈ R。我们的动机是试图用关系来处理非决定论，在固定点逻辑中使用函数来形式化决定论。这种推广为关系的固定点和相应的逻辑的定义开辟了新的可能性。正如在传统的不动点逻辑中使用的算子一样，所考虑的关系和不动点的适当条件可以用来以不同的方式定义几个逻辑我们将集中讨论一种特殊类型的关系，我们称之为推理（见第3节），它可以被看作是推理定点逻辑的关系对应物[9，13]。在第2节中，我们回顾了不动点理论和逻辑的基本原理。在第3节中，我们定义了一些关于关系不动点理论的重要概念。在第4节中，我们介绍了关系型固定点逻辑RIFP及其语法和语义，我们还展示了如何在这种逻辑中表达问题的例子在第5节中，我们证明了RIFP逻辑通过将RIFP转换为二阶逻辑来捕获多项式层次复杂性类，反之亦然。在第6节中，我们定义了RIFP逻辑的一个片段，称为RIFP1，它只包含RIFP算子的一个应用，我们证明了这个逻辑捕获NP。在第7节中，我们将RIFP与NIFP进行比较，NIFP是由Abiteboul，Vianu和Vardi定义的逻辑[4]。最后，我们总结了这项工作，并在第8节中展示了未来的研究主题。2不动点逻辑与描述复杂性在本节中，我们将回顾本文中使用的一阶逻辑和描述复杂性的我们 遵循 的 注：[10，9]。一符号集是一个集合S={R1，...，R1，F1，...， f k，c1，.， c m}的关系、函数和常数符号。每个Ri是元ai的关系符号，fj是元rj的函数符号。一个S-结构是一个对A=（A，σ），其中A是一个集合，σ是一个映射，它把元数k的每个关系符号R∈S关联到一个关系σ（R）=RA<$Ak，把每个函数符号f关联到一个函数σ（f）=fA，把每个常数c∈S关联到一个元素σ（c）=cA。116M. Farias等人/理论计算机科学电子笔记332（2017）113XXXXX，xX我们将[S]定义为有限S-结构的集合。有序结构是符号集合S中的结构，该符号集合S包含被解释为线性顺序的关系符号。<一个S-解释I是由一个S-结构和一个赋值β组成的一个对（A，β），它将每个一阶变量x与一个元素β（x）∈A相关联，并将每个元数为k的关系变量X与一个关系β（X）<$Ak相关联。一阶逻辑和二阶逻辑的语言和语义都像往常一样定义。一个公式，其符号属于某个符号集S，称为S-公式。我们把具有自由关系变量但没有二阶量化的公式称为一阶公式，因为它们本质上是一阶的。 如果x是一个一阶变量且a∈A，则βa是赋值，定义为βa（y）=a，如果y= x，否则β a（y）= β（y）。类似地，如果X是元数为k的二阶变量且X<$Ak，则当Y=X时βX（Y）=X，否则βX（Y）=β（Y）。归纳集可以定义为某些算子的不动点。设A是一个集合，F：P（A）→ P（A）和A上的算子. F的阶段序列是F0（= 0），F1， . .其中Fi+1=F（Fi），Fi称为F的第i级.一个算子F被称为归纳的，如果它的阶段形成一个递增链（Fi<$Fi+1）。称F是单调的，如果对所有X∈ P（A），X<$F（X）;如果对所有X，Y∈P（A），X <$Y蕴涵F（X）<$F（Y），则F是单调的我们用F∞表示阶段Fi，如果它存在，它是F的一个不动点，否则是F的一个不动点。归纳算子（以及非归纳和单调算子，因为它们是归纳的）的阶段序列在序列的某个阶段达到一个固定点如果F是归纳的，则F的归纳不动点定义为ind（F）=F∞。如果F是非正则的，则F的非正则不动点定义为如果p（F）=F∞。一个单调算子总是有一个最小不动点（w.r.t.包容定义为lfp（F）=F∞。对于F是一个任意算子，我们称F∞为F的部分不动点，记为pfp（F）=F∞。定点逻辑是用表示语言中定义的运算符的定点的语法结构来扩展FO语言而创建的。设φ（X，x）是某种语言的公式，其中X是元数为k的关系符号，x=x1，.，x k.公式φ将解释I的域上的算子定义为：φI（X）={a ∈ A k|I X，a|= φ（X，x）}。公式在关系变量i上是正的，该变量不会出现在奇数个否定的范围内（当我们只考虑连接词时和 如果φ在X上是正的，那么φI是单调的。 如果φ的形式为φ=Xx<$φJ（X，x），则φI是正则的。最小固定点逻辑是用以下规则扩展FO语言获得的：• 如果X是k元关系变量，则x=x1，...，xk且φ（X，x）是X上的LFP公式，则[lfpX，xφ（X，x）]（t）是LFP公式，其中t=t1，.，k是 长度为k的项的元组。M. Farias等人/理论计算机科学电子笔记332（2017）1131171K1K1K给定一个解释I，新公式的满意度关系被定义为作为我|=[lfpX，x φ（X，x）]（t）i φ（tI，.，tI）∈ lfp（φI）.推理定点逻辑的定义类似于：• 如果X是k元关系变量，则x=x1，...，xk且φ（X，x）是IFP公式，则[pX，xφ（X，x）<$Xx]（t）是IFP公式，其中t=t1，.，t k是长度为k的项的元组。满意度关系定义为：我|=[ifpX，x φ（X，x）]（t）i φ（tI，.，tI）∈ ifp（φI）.另一个重要的固定点逻辑是部分固定点逻辑：• 如果X是k元关系变量，则x=x1，...，x，k且φ（X，x）是PFP公式，则[pfpX，xφ（X，x）]（t）是PFP公式，其中t=t1，.，t k是长度为k的项的元组。以及相应的满意度关系：我|=[pfpX，x φ（X，x）]（t）i φ（tI，.，tI）∈ pfp（φI）.LFP和IFP具有相同的表达能力。这一结果由Gurevich和Shelah[14]对有限结构进行了证明。后来，Kreutzer放弃了对结构基数的限制[18]。我们感兴趣的是使用逻辑来描述复杂性类。我们可以将逻辑定义为一对L =（L，|=），其中L是语言，|=满足关系。一个来自L的S-句子定义了一个关于S-结构的判定问题。设φ是一个S-句.我们将φ的有限模型类定义为S-满足φ的结构：Mod（φ）={A∈φ CT [S]|一|= φ}。根据数据库术语，由一类结构定义的决策问题称为查询有限结构可以被编码为计算模型的输入（详见[17]）。因此，我们可以问一类结构是否是可计算的，以及解决它的复杂性是什么。因此，我们可以考虑由某种逻辑定义的查询属于哪个复杂性类，如果有的话定义2.1（L捕获C）设L是一个逻辑，C是一个复杂性类。我们说L捕获C（L =C）i，• 对于每个句子φ∈ L，结构类Mod（φ）在 C（ L <$C）中，并且，• 对于C中的每一类结构Q，存在一个句子φ ∈L，使得Q=Mod（φ）（C<$L）。Fagin 证 明 了 二 阶 逻 辑 的 存 在 片 段 （ EXISTIAL FRAGMENT OF THESECURITY LOGY，简称EXISTIAL SO）捕获了可以在非确定性多项式时间（NP）内解决的一类查询118M. Farias等人/理论计算机科学电子笔记332（2017）113[11]第10段。定理2.2（NSO = NP）NSO捕获NP。受限于有序结构，LFP和等价的IFP精确地定义了PTIME（[16，22]）中的查询。定理2.3（LFP = PTIME，在有序结构上）一类有序结构可以在LFP中定义，如果该类在PTIME中。顺序的作用在这里很重要，因为LFP不能定义PTIME中对无序结构的所有查询实际上，即使是简单的多项式问题，如决定结构是否具有偶数基数的域，也不能在LFP中定义[19]。在无序结构上，我们只有包含LFP_ PTIME，而不是相反。关于PFP，我们有PFP捕获PSPACE，可以使用多项式空间解决的决策问题类，在有序结构上：定理2.4（PFP = PSPACE，关于有序结构）一类有序结构可以在PFP中定义，如果该类在PSPACE中[3，22]。许多其他的捕获结果已经证明了几个逻辑和复杂性类。详情见[17]。我们在上述逻辑之间有以下关系：LFP = IFP，其中最后一个包含仅适用于有序结构。我们希望推广传统不动点理论中考虑的不动点算子，以探索定义逻辑的新方法，旨在通过逻辑来描述描述复杂性的精神。我们将在下一节介绍关系方法3关系不动点理论正如我们已经看到的，传统的定点理论是基于算子的概念，算子本质上是一个函数。我们的建议是考虑关系而不是函数，以捕捉非决定性。给定一个有限域A，设R ∈ P（Ak）× P（Ak）是一个（二阶）关系。我们说二元关系R是全的，如果对所有X∈ P（Ak），存在一个Y∈ P（Ak），使得（X，Y）∈R. R中的链是序列X0，X1， . ，Xm满足X0=n，Xi <$Xi+1且（Xi，Xi+1）∈ R.我们可以定义关系的条件，类似于我们以前见过的用于定义不动点算子 我们说一个关系R如果对所有的（X，Y）∈ R，有X，则P（Ak）× P（Ak）是一个不等式关系很好。给定一个任意关系R <$P（Ak）× P（Ak），我们从R定义一个非对称的全关系RINF如下：RI NF={（X，X<$Y）∈ P（A k）2|（X，Y）∈ R}（一）{（X，X）∈ P（A k）2|$Y：（X，Y）∈R}。M. Farias等人/理论计算机科学电子笔记332（2017）113119KK我们说关系R<$P（Ak）× P（Ak）是归纳的，如果任意序列X0，X1，.，Xm，使得X0=n且（Xi，Xi+1）∈R，0 ≤i≤m− 1，是R中的链。引理3.1如果R是归纳的，那么它是归纳的。一个集合X∈ P（Ak）是关系R的一个不动点，如果R（X，X）。R的一个固定点X称为归纳的，如果存在一个链X0，X1，.，使得X m= X。我们用IND FP（R）表示R的归纳不动点的集合。我们说一个固定点X是R的一个初始固定点，如果存在一个链X0，X1，.，X m使得X m= X且没有X j，j< m是R的不动点。 用INI FP（R）表示R的所有初始不动点的集合。一个集合X是R的一个归纳不动点，如果X是R的一个归纳不动点。我们说X是R的初始不动点，如果X是RINF的初始不动点。我们用rifp（R）表示R的所有初始不动点的集合，即rifp（R）= INIFP（RInf）。引理3.2设A是有限集合。若关系R ∈ P（Ak）× P（Ak）是全归纳的，则任意链X0= n，X1，.，X m，其中m足够大，包含一个不动点，其中m≤|一|K.很容易看出，算子是关系的特殊情况。事实上，给定一个算子F：P（Ak）→ P（Ak），它的图是关系式：RF={（X，Y）∈ P（A）× P（A）|Y= F（X）}。因此，可以使用关系方法来表示函数方法。我们将开发一种逻辑，它能够讨论关系的初始不动点，我们将看到这种逻辑将捕获一些非确定性复杂性类。4关系定点逻辑（Relational Fixed Point Logic，RIFP）在本节中，我们将为一阶逻辑增加定义对应于已定义关系的初始不动点的并集的这种扩展将被称为关系型不动点逻辑（RIFP）。它将增加表达能力，超越传统的定点逻辑。设φ（X，Y）是一个S-公式，其自由关系变量X和Y的元数为k，I是一个S-解释.公式φ（X，Y）定义了φ，Ik kV1，V2R={（V1，V2）∈ P（A）× P（A）|IX，Y|= φ (X, Y)}.如果φ（X，Y）除了X和Y之外没有自由变量，那么给定一个结构A，关系Rφ，I对于A上的所有解释I都是相同的。因此，我们将Rφ，A改为。RIFP语言扩展了一阶逻辑的语言，其规则如下：120M. Farias等人/理论计算机科学电子笔记332（2017）113INFINFINF1KINF• 如果X和Y是元数为k的关系变量，则t=t1，.，t k是项，φ（X，Y） 是一个S-公式，则是RIFP的S-公式[rifpX，Yφ（X，Y）]（t）满意度关系是使用假设关系Rφ，Igener定义的。由Rφ表示，I.我们给出一个解释，我|= [rifpX，Yφ（X，Y）]（t）i φ（tI，.，tI）∈rifp（Rφ，I）=I NI FP（Rφ，I）.4.1示例在下面，我们将展示如何使用RIFP来表达一些查询。例4.1（偶数基数）偶数查询对应于域具有偶数基数的结构注意，集合A具有偶数Cardi-nality如果存在A的一个划分{AJ，AJJ}和一个双射f：AJ→AJJ。我们将使用rifp算子来构造这样一个双射（实际上，是一个二元关系，它是双射的图）。设Y和X是二元关系变量，并考虑以下公式：F（Y）=xyz[YxyY xz→y=z]，INJ（Y）=xyz[Y xyY zy→x=z]，TOT（Y）=xy[YxyY yx]，DIS（Y） =x<$[yYxyzY zx]，其中TOT（Y）表示每个元素在Y中出现在某对中。设φ（X，Y）为公式φ（X，Y）=（X=φ）<$F UNC（Y）<$INJ（Y）<$T OT（Y）<$DIS（Y）.设A是一个结构，Rφ，A是A上由φ（X，Y）定义的关系。一对（B，BJ）属于Rφ，Ai <$B =<$，BJ是A的整环A的一个划分上的双射的图. 这样的双射存在当且仅当A有偶基数。的在R φ中，A包含Rφ，A和对（B，B），对于所有B∈A2，使得B1=A 2。若A有奇数基数，则R φ上的任何链，A 长度为1，唯一的初始在传统的fix e d-point中，d是0。如果A具有偶常数，则任何长度为2到达一个初始的固定点，这是一个双射函数的图形，如上所述。因此，如果A具有奇数基数，则Riff（Rφ，A）为空。句子EVEN=满足A i，则rifp（Rφ，A）非空。它只发生在A有偶数基数的情况下。 ”“ “ 那 是 什 么 ？ “ 那 是 一个 询问。QM. Farias等人/理论计算机科学电子笔记332（2017）113121例4.2（可满足性）SAT问题由合取范式（CNF）的命题逻辑公式集合组成，这些公式是可满足的。CNF中的公式α具有以下形式：α = C1... Cm，其中，每个Ci是一个子句，也就是类似于C i= l1. 斯泰尔斯每个l j是一个文字，也就是说，它要么是一个命题符号p k，我们说p k在Ci中出现正值，要么是一个否定的命题符号<$p k，我们说p k在Ci中出现负值。当我们想用公式来表达决策问题时，我们常常不得不将问题输入表示为有限结构。 设Aα是符号集S={P，N}上的一个结构，其中P和N是二元关系.设r是在α中出现的比例符号的数量，A={1，.，max{m，r}}。令PA={（i，j）|pjoccurspositiveinC i}和NA={（i，j）|pjoccursn enegativeinC i}. P和N的第一个位置代表一个子句，第二个位置代表一个命题符号。在不失一般性的情况下，我们认为任何公式都至少具有与命题符号一样多的子句，这可以通过向公式添加伪子句（p0<$p0）而不改变其可满足性来实现。我们将写出一个RIFP公式，满足这些结构Aα，使得α是满意的。我们利用RIPP算子构造三元关系，三元关系的元组表示命题符号的真值，子句和公式根据命题符号的某些赋值。我们使用三元组（a，b，c），使得a可以根据它是否指代命题符号而假定值为0、1或2，分句或公式，b表示分句或命题符号的索引，c可以是0或1，分别表示真或假。这一关系将分三个阶段构建。首先，我们把代表估值的三元组。令PVAL（Y）为公式PVAL（Y）=xyz（Y xyz→x= 0）y（（Y0y0Y 0y 1）<$（Y0y0Y 0y 1）），和φ0（X，Y）是公式φ0（X，Y）=（X=φ）φPVAL（Y）.两个关系X，Y满足φ0（X，Y）i <$X =<$X，Y表示赋值，其中（0，i，1）表示命题符号i的值为真，类似于（0，i，0）。在第二步中，我们包括那些对应于子句真值的三元组。 我 们 可以认为X包含代表估值的三元组，并包含在第一步中。 考虑公式CVAL（Y）CVAL（Y）=xyz（Y xyz→x= 1）y（（Y1y 0Y 1y 1）<$（Y1y 0Y 1y 1）），和式CL（X，Y）122M. Farias等人/理论计算机科学电子笔记332（2017）113φ，Aα0R12CL（X，Y）= CVAL（Y）y（Y 1 y 1 Participantp（（P yp X 0 p 1）（Nyp X 0 p0）。设φ1（X，Y）为公式φ1（X，Y）= PVAL（X）<$CL（X，Y）。如果X和Y满足φ1（X，Y），则X对应于一个赋值，Y表示根据赋值X的子句的真值。最后一步根据公式子句的真值计算设FVAL（Y）为公式FVAL（Y）=（（Y 200 <$Y 201）<$$>（Y 200 <$Y 201））。公式FVAL（Y）意味着Y要么有元组（2，0，0），表明SAT的输入是不满意的，要么有元组（2，0，1），否则。设FOR（X，Y）为公式和FOR（X，Y）=Y201个参与者（yX 1y 1）φ2（X，Y）= FVAL（Y）FOR（X，Y）.最后，设φ（X，Y）= φ0（X，Y）<$φ1（X，Y）<$φ2（X，Y）。一对（X，Y）满足φ（X，Y）i，它满足某个φ i（X，Y），0 ≤i≤ 2。特别地，（2，0，1）∈Yi，则公式α是满足的。 因此（2，0，1）∈rifp（R）i <$α是令人满意的。 让在=[rifpX，Y φ（X，Y）]（201）处的Δ S。然后Aα|i α时的= S是令人满意的。Q我们用下面的定理来结束这一节，这个定理将RIFP和IFP的表达定理4.3（IFP <$RIFP）IFP-公式在RIFP中有一个等价公式。证据 设f为以下IFP公式：φ：= [ifpX，xφ（X，x）]（t）.设I是一个解释，φI是由φ在I上定义的算子。让φI（=φ），φI，φI， . .是φI的级数。我们将定义一个公式θ（X，Y），使得θ，I中唯一通向初始固定点的链与φI的阶段序列重合。设θ（X，Y）为公式θ（X，Y）= θx（Y x Participi φ（X，x））.关系Rθ，I正是算子φI的图。因此，φI的级数序列的任何有限初始段都是Rθ，I的链，反之亦然。此外，委员会认为，M. Farias等人/理论计算机科学电子笔记332（2017）113123INFINFINFYφ，IYINFV2由于φI是非线性的，则Rθ，I=Rθ，I。因此，Rθ，I只有一个初始它是一个固定的点，它等于φI的预定固定点。因此，公式N= [rifpX，Yθ（X，Y）]（t）相当于。Q5RIFP捕获PH在本节中，我们将展示RIFP的表达能力与SO的表达能力相当。由于SO捕获了多项式层次（PH）[21]，因此RIFP也捕获了PH。为了表明RIFP的表达能力与因此，我们将提供两种语言之间的翻译。考虑以下从SO到RIFP的翻译：Tr（t0<$t1）：=t0<$t1Tr（Rt1.（t k） ：= Rt1. tkTr（Xt1. t k）：= Xt1. t kTr（<$φ）：=<$Tr（φ）Tr（φ1<$φ2）：=Tr（φ1）<$Tr（φ2）Tr（λxφ）：=λxTr（φ）Tr（φYφ（Y）） ：=<$x[rif pX，Y<$（X，Y）]（x）<$T r（φ（φ））其中φ是公式φ（X，Y）=（X = φ Tr（φ（Y）。引理5.1设φ∈SO。然后φ<$Tr（φ）[12]。证明是通过归纳法。有趣的情况是二阶的情况存在性量化器 注意，一对（V1，V2）在Rφ中，I i V1=且IV2|=φ（Y）。我们有两种情况： |=φ（Y），在这种情况下，I|=Tr（φ（φ）），或ii）V2YY|f = φ（Y）。在这种情况下，我们有RINF中的任何链，如果有的话，大小为2，并且任何初始固定点都是满足φ（Y）的非空关系V2相反，任何这样的关系V2都在某个链中，它是一个初始固定点。因此，I V2|=<$x [rifpX，Y <$（X，Y）]（x），因为根据归纳假设，Tr（φ（Y））等价于φ（Y）。因此，等价性如下。对于相反的情况，也就是说，从RIFP到SO的翻译的定义，我们必须能够使用二阶逻辑重构产生初始不动点的链。关键的事实是，关系Rφ，I，保证任何初始固定点都可以通过长度极短的链条我124M. Farias等人/理论计算机科学电子笔记332（2017）113INFRJINFINF设φ（X，Y）是X，Y为k元关系变量的公式，I是定义域基数为n的解释.设X0，X1，.，X m是一个链在φ，IINF 而Xm是初始固定点。 作为Rφ，I是逆的，m至多是nk（引理3.2）。 设是一个关于I的2k元关系，它是关于k元组<对于1≤i≤nk，设ti是关于的第i个k元组.让X是2k元关系，定义为：XJ={（ti，a）∈A2k|a∈ X i}。我们使用元组在XJ中的前k个位置来表示关系Xi在链中的索引i，其他k个位置表示Xi中的k元组。 我们可以使用存在性量化来检查像Xj这样的关系的存在性，它证明了到达初始固定点的链的存在性。我们必须保证链中的连续关系是Rφ，I中的对。考虑以下公式：TE（φ，XJ，t）：=φ（X，Y）<$$>φ（X，X）<$a（X Jt，aParticipXa）b（X JtJ，bParticipYb<$Xb））。公式TE（φ，XJ，t）表示t和tJ关于到，XJ在t和tJ的投影在Rφ，I中形成一对，这不是一个固定的点。公式START（XJ）意味着链的关系X1是XJ在t1的投影（回想一下，在链中X 0=X 1）：S T A RT（X J）：=<$Y（φ（n， Y）<$<$a（X Jt1aParticipateYa））.最后，公式END（X J，tpf，z）：=<$X（<$a（X JtfpaParticipXa）<$φ（X，X））<$Xtfpz意味着XJ在tfp上的投影是一个固定点，z属于这个投影。设Ord（）是一个一阶公式，说明它是k-元组上的线性序XJ<$tXJ<$t

下载后可阅读完整内容，剩余1页未读，立即下载