理论计算机科学电子笔记：锐化持续时间演算的不完全性

理论计算机科学电子笔记139（2005）91-104www.elsevier.com/locate/entcs锐化持续时间演算的不完整性1迪米塔山口盖列夫伯明翰大学计算机科学学院，英国数学与信息学研究所，保加利亚科学院电子邮件：gelevdp@math.bas.bg。摘要我们证明了由BNF定义的持续时间演算的特别窄的子集：：=|）S¶|一|ϕ⇒ϕ|（n; n）不是递归可公理化的，或者换句话说，是不完全的。保留字： 持续时间演算，递归公理化，不完全性。介绍持续时间演算（DC）是在[18]中引入的，作为一种基于谓词区间的线性时间 时 态 逻 辑 ， 用 于 推 理 实 时 系 统 。 DC 可 以 被 视 为 区 间 时 序 逻 辑（IntervalTemporal Logic，ITL，[12，13，2]）的实时变体中的理论对DC的全面调查可以在[10]中找到。最近的专著[17]对DC和案例研究进行了详细的介绍DC是一阶谓词逻辑的保守扩展，因此DC的有效性是不可判定的。决策过程仅对于DC的子集是已知的，参见例如。[19 ]第10段。由于这个原因，证明系统对于DC的使用是相对重要的。DC的有限希尔伯特式证明系统，它是完整的，1 [11]后的标题1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.00492D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）91在[9]中获得了关于其相对于在ITL实时帧有效的ITL公式集的实时语义一个理论的无穷完备证明系统的存在意味着在这个理论中有效的公式的集合不会比半可判定的更差，因为在一个无穷证明系统中形式良好的证明的集合然而，在DC中的有效性不是半可判定的.因此，[9]的证明系统只是相对完整的，这并不奇怪。在逻辑学中，有效性并不比半可判定性差，因为逻辑学允许完全递归公理化，而这些公理化也不需要基于有限的公理和规则集。有效性的半可判定性所需要的是识别公理的出现和证明中规则应用的正确性的算法逻辑和理论不承认一个完整的递归公理化称为不完整的。最著名的不完全理论是皮亚诺算术。它的不完备性在著名的哥德尔定理（cf.e. G.[15]）。基于区间的时态逻辑的令人生畏的复杂性已经在早期的工作中显示出来[8]。在[19]中建立了DC的小子集的不可判定性。更多结果可参见[4]。命题ITL的复杂性很大程度上取决于局部性原理，该原理限制原子公式仅依赖于其真值的参考区间的初始点具有局部性原理的命题ITL是可判定的。在[11]中发现了命题ITL的一个非常窄的不可判定子集。在本文中，我们提出了一个特别小的DC子集，它仍然足够大，以体现DC的不完备性。 该子集包括仅以受限形式出现的持续时间项[S|，只有0元可变谓词符号，也称为命题时间字母，因此，没有正确的一阶结构。本文结构经过简短的讨论，我们介绍了子集的问题，并证明在这个子集的有效性是不半判定。1预赛1.1DC的定义DC是一个经典的一阶模态逻辑，具有一个称为chop的正常二进制模态。我们用（表示chop。;。）. DC语义中的可能世界是实数的闭有界区间因此，DC也是一种基于区间的实时时序逻辑。这里有一个正式的定义，D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）9193DC.1.1.1语言除了惯用的一阶逻辑符号，DC词汇表还包括状态变量P、Q、. 状态变量用于构建状态表达式S，其语法为：S：：= 0|P|SS状态表达式S作为持续时间项的一部分出现在公式∫S. 的DC项t和公式的语法通过持续时间项和使用模态（. ;。），分别为：∫t：：= c|X | S|f（t，.（t）：：=|R（t，.（t）|ϕ⇒ϕ|（;）|x这里，x、c、f和R分别表示单个变量、常数、函数和关系符号在DC中，常数、函数和关系符号可以是刚性的，也可以是柔性的。刚性符号的解释要求不依赖于参考区间。个体变量是刚性的。状态变量是可变的。我们用#s表示非逻辑符号s的arity。元0的柔性关系符号和柔性常数符号也分别称为时态命题字母和时态变量的刚性常数0、刚性二元函数符号+、刚性二元关系符号=和≤以及无穷多个单个变量在DC词汇表中是强制性1.1.2语义DC中的时间模型是实数的线性有序群R，0 R，+R，≤R 让我表示集合{[τ1，τ2]：τ1，τ2∈R，τ1≤τ2}.定义1.1谓词p：R→ {0， 1}具有有限可变性如果设定{τ∈σ：p（τ）= 0}要么是空的，要么是对所有σ∈I的区间的有限并。有限可变性属性如图1所示它反映了一个自然的假设，即出现在由DC建模的系统中的{0， 1}值信号在任何给定的有界时间间隔内只改变其值有限次不可能公理化DC完全由无穷手段可以归因于对状态变量的解释的要求，94D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）9110τ∈Rτ1τ2τ3Fig. 1.具有有限可变性属性的谓词的图。对于所示的区间σ，定义1.1中的集合{τ ∈ σ：p（τ）= 0}为[τ1，τ2]<$[τ3，max σ]。这个财产。这可以通过比较抽象时间ITL[3]和抽象时间DC[5]来看出，ITL中不存在有限可变性，而DC中存在有限可变性。前一个系统允许完全的无穷公理化，而后者不允许。定义1.2DC语言L的解释I是关于L的词汇表的函数。各种符号的I值的类型如下：I（x），I（c）∈R，对于单个变量x刚性常数cI（c）：I→R，对于可变常数c对于正则函数symbolsf，I（f）：R#f→R，I（R）：R#R→{0，1}和关系符号RI（f）：I×R#f→R，I（R）：I×R#R→{0，1}表示可解的f，RI（P）：对于状态变量P，R →{0， 1}I（0），I（+）和I（≤）总是R的相应分支，0R，+R，≤R<$，且I（=）在R上相等.状态变量的解释需要具有有限可变性属性。定义1.3给定解释I，状态表达式的值Iτ（S时间τ∈R处的S由以下条款定义：Iτ（0）= 0Iτ（P）=I（P）（τ）Iτ（S1<$S2）= max{ 1−Iτ（S1），Iτ（S2）}在区间σ∈I上的项t的值Iσ（t）由以下条款定义：最小σσ最大σD.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）9195Iσ（x）=I（x）Iσ（c）=I（c），对于刚性cIσ（c）=I（c）（σ），对于可伸缩的cmIσ（S）=Iτ（S）dτ最小σIσ（f（t1， . . ，t#f）） 为I（f）（Iσ（t1）， . . ，Iσ（t#f））Iσ （f（t1 ， . . ，t#f））为I （f）（σ，Iσ （ t1 ）， . . ，Iσ（t#f）），其中f是可伸缩的给定同一语言L的解释I和J以及来自其词汇表的符号s，J称为I的s-变体，如果J（sJ）=I（sJ），对于所有来自L的sJ，可能除了s。建模关系|=定义在L的解释I上，区间σ∈I和公式从L通过以下条款：I，σ|=I，σ|=R（t1， . . ，t#R） i∈I（R）（Iσ（t1）， . . ，Iσ（t#R））=1，对于刚性RI，σ|=R（t1， . . ，t#R） i∈I（R）（σ，Iσ（t1）， . . ，Iσ（t#R））=1，对于可伸缩的RI，σ|= i I，σ| =或I，σ|=I，σ| =（;）i I，σ1|=和I，σ2|对于某些σ1，σ2∈ I，使得σ=σ1<$σ2且最大σ1=最小σ2I，σ| = xi J，σ|对于某个J，它是I的x-变量，1.1.3运算符的缩写和优先顺序在公式中，符号T、<$、惠、和/在任何出现+、=和≤的地方都使用fix表示法。连接词<$、、和惠也在状态表达中用作缩略语。以下缩写是DC专用的：Q（（T;）; T），Q哦，（第1页;第2页;.）;n）（注1;. ;（<$n−1;<$n）.. . ）的情况下，10-0，L2001年，[S|l/= 0 S = l.通常的优先约定被假定为关于命题连接词，和。使用chop模态时，我们总是写括号（。;。），从而为其分配最低优先级。例如，（AB;C惠D）与（（AB）;（C惠D））相同，而AB;C惠D不是格式良好的。96D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）911.2波斯特我们的证明依赖于Emil Post关于可判定性的著名定理我们以如下形式使用该定理定理1.4设X是某个有限字母表中的一个可判定词集。 设Y<$X，且Y和X\Y都是半可判定的。 则Y和X\Y都可判定。可以找到一个更一般的公式和波斯特定理的证明例如，在[15]中。2不完全子集我们在本文中关注的DC子集由BNF（一）：：=|[S||一|ϕ⇒ϕ|（;）S：：=0|P|S其中P代表状态变量，A代表命题时态字母。在下一节中，我们证明了在这个子集中有效性不是半可判定的.3不完全性证明许多文献中的不可判定性证明都是基于将图灵机的停机问题简化为所考虑的逻辑或理论的有效性问题这样就可以证明，在所考虑的系统中，有效公式的集合并不比半可判定简单。在下面的证明中，我们将停机问题简化为所考虑的DC子集中的可满足性问题。这种方法可以被视为类似于[8]中所采用的方法，其中图灵机的非停机问题被简化为有效性问题。约简表明，来自公式X的某个可判定集合的可满足公式形成仅半可判定的集合Y的具有来自X的有效否定的公式形成不可判定集合Y相对于可判定集合X的补集X\Y。波斯特因此，我们的约简表明，在所考虑的公式集合X中的有效性不能公理化。证明由两部分组成在第一部分中，我们将已知的R上谓词的有限可变性（定义1.1）推广到I上的谓词。时间命题字母的解释是I上的谓词。我们证明了D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）9197最小σ τ最大σ图二.对于具有定义3.1所述的有限可变性性质的a：I → { 0，1 }，为了使单例{τ}成为Va，σ的合适候选者，用相同图案的线标记的σ的子区间处的a的值必须相同。在不同标记的子间隔处的a的值可以是不同的。请注意，其中两个区间被分组在一起，因为它们都以τ为起点。时间命题字母的解释的有限可变性在某种意义上可以用DC子集（1）中的公式来表示。证明的第二部分使用的公式，表达了有限可变性的一般形式，在适当选择图灵机的停机问题的简化中，如上所述。3.1区间谓词的有限变异性定义3.1I上的谓词a具有有限可变性，如果对于每个σ∈I，存在有限个Va，σ<$σ使得如果σ1，σ2∈I，σ1，σ2<$σ且a（σ1）/=a（σ2），则存在Va，σ的成员，它要么是σ1和σ2的端点之一，要么在minσ1和minσ2之间，要么在maxσ1和maxσ2之间。图2说明了这个定义。I上谓词的有限可变性是[ 6 ]中提出的有限可变性从DC状态到DC可变符号给定一个命题时态字母A和一个状态变量P，我们写：⎛ ⎞fv（A，P）Q1，Q2∈{P，<$P}B∈{A，<$A}Q <$（[Q1|; B（[Q1|; T;[Q2|）;[Q2|）（[第一季|;<$B（[Q1|; T;[Q2|）;[Q2|）命题3.2设I表示某个包含A和P的DC语言的解释。设σ∈ I. 然后又道：(i) 如果I（A）具有有限可变性，则I（P）可以定义为：（二）I，σ| = fv（A，P）.(ii) 相反，如果（2）对某个解释I成立，则限制I（A）|I（A）的{σJ∈I：σJ<$σ}对σ在I中的替换可扩展为I上的一个谓词，具有有限可变性.98D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）91证据 （i）设VI（A），σ满足定义3.1的要求。让{τ0，. ，τn}= VI（A），σn {min σ，max σ}和τ0<... <τn.LetI，[τ2i−1，τ2i]|=[<$P|对于i，suchthat0<2i≤n且I，[τ2i，τ2i+1]|=[P|对于i，使得0 2i +1≤n。<则（2）对于任意两个i，j∈ {1，.， n}，τJ，τJJ∈（τi−1，τi）和τJ，τJJ∈（τj−1，τj）使得τJ≤τJ和τJJ≤τJJ，我们有1 1 2 2 1 2 1 2(3) I（A）（[τ J，τ J]）= I（A）（[τ JJ，τ JJ]）。1 2 1 2因此，I（A）的有限可变性意味着（2）。(ii)让（2）保持。我们说I（P）在τ∈R处改变其值，如果存在τJ∈（−∞，τ）和τJJ∈（τ，∞）使得I，[τ J，τ]|=[Q|而我，[τ，τ JJ]|=[<$Q|其中Q是P或-P。设集合V由minσ、maxσ和σ中I（P）改变其值的时间点I（P）的有限可变性意味着V是有限的。让{000，.，m}= V和0<. < 好吧如果τJ，τJJ∈（i−1，i）和τJ，τJJ∈（j−1，j），对于某些i，j∈ {1，.，m}，1 1 2 2且τJ≤τJ且τJJ≤τJJ，则（2）蕴涵（3）.故V是满足要求的。1 2 1 2定义3.1中关于VI（A），σ的项。设a：I→{0， 1}，a（σJ）=I（A）（σJ），对σJ∈I，a（σJ）=0.则对于所有σJ∈I，V满足定义3.1中关于Va，σJ的方程。Q第3.2节结论是，I（A）|{σJ∈I：σJ<$σ}可以扩展为I上具有有限可变性的谓词当且仅当I，σ|=Pfv（A，P），其中，PARP具有通常的含义。这个量化器在[14]中被添加到DC中，并在[7，16]中进一步研究以用于实际目的。fv（A，P）显然不在DC的子集（1）之内，而且确实不在1.1小节中介绍的DC系统之内，但fv（A，P）在子集（1）之内。然而，如果P不出现在公式η中，则Pfv（A，P）η的有效性等价于不包含P的fv（A，P）η的有效性。这让我们避免使用在续集中的Pills3.2用可满足的DC公式编码图灵机的终止计算设T是一个确定性图灵机，其字母表为，控制状态集为Q。令来自于C的字母和来自于Q的状态是语言L的词汇表中用于DC的时间命题字母。 我们假设Q= 0。设L有两个以上的命题时态字母b，r/∈QD.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）9199以及状态变量P。 然后T的构形可以被编码为L中的公式，只用集合Q的命题时态字母来写。;。）如下。 设磁带上的字在某种构形中位于T的头部的左边，它是α= A1. 分枝让头部右侧的字为β= B1. Bn.设头部观察到的字母为C，T的当前控制状态为q。则T的构形α、q、C、β可由下式α，q，C，β（b）A1;. Am; q; C; B1;. ;Bn;b）b在α、q、C、β中的出现用来标记到目前为止在T的计算过程中观察到并可能被重写的（潜在无限）磁带部分的结束使用这种约定，T的转换规则也可以被编码为L的子集（1）中的公式。下面我们提出一种方法来做到这一点。它涉及辅助命题时间字母r。考虑L的解释I，其中关于r的下列公式是有效的：（四）（五）€ [1|布雷尔（D;r）D∈Q{b}在这样的解释下，如果τ0，.，τn∈R，τ0<. < τn，并且对于每个i=1， . . ， n存在一个D∈Q <$$><${ b}满足chthatI，[τi−1，τi]|=D，thenI，[τ0，τn]|=r.在Words中，r完全满足于I的值，I可以被分割成有限多个子区间，每个子区间满足D∈Q的某个时间命题字母。对于一个解释I来验证公式（4）和（5），只在可以这样划分或长度为0的区间上满足r注意，（4）和（5）是在L的子集（1）中的公式。我们用Axr表示公式（4）和（5）的合取。T的转换规则规定T覆盖其头部观察到的字母，并向左或向右移动，这取决于观察到的字母。考虑T的转换规则，该规则声明在控制处观察C状态qJ应该使T用D代替C，将其控制状态改变为qJJ并向左移动。设Z表示来自T的字母，它占据了T的磁带上没有其他字母被写入的所有位置这样的规则可以由一组含义描述（r;A;qJ;C;r）<$（r;qJJ;A;D;r）对于每个A∈<$，（6）（r;b;qJ;C;r）（r;b;qJJ;Z;D;r）100D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）91第一组含义描述了当T的头部正确地位于在计算的早期步骤中已经写入的磁带部分内时，规则所规定的转换最后一个含义适用于向左移动将T的头部带到迄今为止尚未使用的磁带位置的情况，因此T在那里发现了Z导致T的头部向右移动的规则可以用类似的公式来描述：（r;qJ;C;A;r）<$（r;D;qJJ;A;r）对于每个A∈<$，（七）（r;qJ;C;b;r）（r;D;qJJ;Z;b;r）如果γ<$δ是（6）和（7）中的一个蕴涵，并且γ描述了在构形αJ，qJ，CJ，βJ处T的头部周围的情况，那么T可以从αJ，qJ，CJ，βJ移动到构形αJJ，qJJ，CJJ，βJJ，其中头部的邻域由δ描述。这从公式的有效性中反映出来(8)αjJ，qJJ，CJJ，βJJ由于我们只考虑确定性T，对于每个配置αJ，qJ，CJ，βJ，最多有一个蕴涵γ<$δ来自（6）和（7），使得（8）描述T的下一个移动。显然，固定机T的转移规则可以用形式（6）和（7）的有限蕴涵集来描述设AxT表示所有这些蕴涵的合取.显然，如果从由<$α，q，C，β描述的配置开始，机器T可以达到由<$αJ，qJ，CJ，βJ，then描述的配置(9)<$α，q，C，β<$QAxr<$AxT<$<$αJ，qJ，CJ，βJ这是一个有效的公式。如果初始配置α，q，C，β使T生成一个无限配置集，(10) I，σ |=<$α，q，C，β<$Q Ax r<$AxT<$Q一个人（[1|;<$A[1|;[1|）的情况下，A∈Q{b}“我的天，Q则谓词I（A）对所有A∈不能具有有限可变性- 是的 为了实现这一点，请注意，如果（10）成立，则（9）的有效性意味着I，σ |=J J J J对于由y生成的所有无穷多个配置α， q， C， Β，T从α，q，C，β开始，其中有αJ和βJ的任意大的l∞的构形。 此外，（10）中的公式<$Q<${b}只在σ的非零长度的子区间上满足在<$αJ，qJ，CJ，βJ中发生的前序项口头字母，而这些子区间又假定为D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）91101以包含不满足相应命题时间字母的非零长度的子区间 让我们把右边的公式表示为|=（10）中的ηα，q，C，β。则命题3.2意味着，对于使T生成无限个构形集的α，q，C，β(11)fv（A，P）α，q，C，βA∈Q{b}这是一个有效的公式。另一方面，如果α，q，C，β使T在有限步中终止，则I和σ可以被选择以满足（10），使得I（A）对所有A∈φ具有有限变分性质，因此（11）对这样的α，q，C，β无效。我们在下面的命题3.3中证明了这一点。这意味着（11）是有效的当且仅当α，q，C，β使T生成无穷多个构形。注意，（11）在L的子集（1）中。 我们使用相同的状态变量P来证明（11）中所有命题时间字母A∈Q{b}我们能够做到这一点，因为这些字母是无限多的，因此可以选择P的解释，以便经常改变所有字母的可以选择图灵机T，使得对于每个初始配置，它要么终止，要么生成无限多个不同的配置。因此，可以选择T，使得使它最终终止的初始配置的集合是半可判定的，但不是可判定的，并且根据定理1.4，使它不终止地运行并生成无限多个配置的初始配置的集合不是半可判定的。如果T是这样选择的，那么形式（11）的有效公式的集合不是半可判定的。由于所有这些公式都在L的子集（1）中，并且子集（1）中的公式是否具有形式（11）是可判定的，所以在L的整个子集（1）中的有效性不是半可判定的，这意味着子集（11）是不完整的。这是本文的主要结果。为了完成它的证明，我们只需要证明命题3.3，就像上面承诺的那样。命题3.3令某个确定性图灵机T的初始配置α，q，C，β使它在有限步内终止。则（10）中的公式ηα，q，C，β可满足一个解释I，使得谓词I（A）对所有A ∈ φ具有有限可变性。证据设α，q，C，β使T通过构形序列αk，qk，Ck，βk，k = 0，.，N，其中，α0，q0，C0，β0是α，q，C，β，qN是T的终止控制状态。为了简化我们的概念，假设Dk，1， . . ，Dk，nkst和forsometemporal102D.P. Guelev/Electronic Notes in Theoretical Computer Science 139（2005）91从Q_k_b{b}中得到的比例方程，其中αk，qk，Ck，βk是（Dk，1;. . ;Dk，nk），k = 0，…，N.Wecoseσtobe[0，1].我们的目标是.. . . ，τk，nk ∈[0，1]，k=0，.，N，这样，(12) 0=τk，0<.. . <对于k=0， .. . ，N，和（13）{τkJ，1， . . ，τkJ，nkJ−1}<${τkJJ，1， . . ，τkJJ，nkJJ−1}=k，如果0≤k

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