软件学报  2018, Vol. 29 Issue (10): 3009-3020   PDF    
良结构下推系统的可覆盖性问题的下界
李春淼, 蔡小娟, 李国强     
上海交通大学 软件学院, 上海 200240
摘要: 良结构下推系统是下推系统和良结构迁移系统的结合,该系统允许状态和栈字符是向量的形式,因而它们是无限的.状态迁移的同时允许栈进行入栈出栈的操作.它"非常接近不可判定的边缘".利用重置0操作,提出了一种模型可覆盖性问题复杂度下界的一般性证明方法,并且证明了状态是三维向量的子集和一般性的良结构下推系统的可覆盖性问题分别是Tower难和Hyper-Ackermann难的.
关键词: 良结构下推系统     可覆盖性     下界     重置0     Hyper-Ackermann难    
Lower Bound for Coverability Problem of Well-Structured Pushdown Systems
LI Chun-Miao, CAI Xiao-Juan, LI Guo-Qiang     
School of Software, Shanghai Jiaotong University, Shanghai 200240, China
Foundation item: National Natural Science Foundation of China (61472238, 61672340, 61472240, 61872232)
Abstract: Well-Structured pushdown systems (WSPDSs) combine pushdown systems and well-structured transition systems to allow locations and stack alphabets to be vectors, and thus they are unbounded. States change with the push and pop operations on the stack. The model has been said to be "very close to the border of undecidability". This paper proposes a general framework to get the lower bounds for coverability complexity of a model by adopting the reset-zero method. The paper proves that the complexity is Tower-hard when a WSPDS is restricted with three dimensional state vectors, and Hyper-Ackermann hard for the general WSPDSs.
Key words: well-structured pushdown system     coverability     lower bound     reset-zero     Hyper-Ackermann hard    
1 引言

程序分析是软件工程和形式化方法重要的研究领域之一, 人们在最初的程序分析中使用有限系统[1]作为程序模型, 它是由有限的状态集和在状态上有限的迁移规则组成.其表达能力十分有限, 无法对递归、并发等程序特征进行分析.对其扩展后可分别形成下推系统[2]和良结构迁移系统[3].前者给有限系统配备一个栈, 状态迁移的同时进行入栈、出栈操作, 方便建模单线程递归程序; 后者将状态集拓展到无限的良拟序集, 并保证迁移规则具有单调性.为了更好地描述和分析并发程序, Cai和Ogawa将二者结合, 提出良结构下推系统[4], 可以很方便地建模并发递归程序, 其具有强大的表达能力[5], 已经“很接近不可判定的边缘”[6].

我们通过一个自然数程序例子来说明这个模型:只用一个局部变量计算Ackermann函数A(2, n)的程序如图 1所示.并发程序对应多栈, 因此图灵等价, 是不可判定的.很多研究都对并发程序进行了限制, 比如在文献[7]中, 要求程序在函数调用时不能进行进程切换, 直到建模其行为的多重集下推系统栈空才行, 该模型就可被编码为良结构下推系统; 在文献[8]中, 针对用于建模程序的模型, 允许多栈但限制栈高, 也允许栈元素是多重集, 该模型也可以被编码成良结构下推系统.因此尽管并发后的程序相比单进程的程序, 相对应的良结构下推系统的可覆盖性问题的难度可能会上升, 但依旧满足我们提到的下界难度结论.由于我们后面证明的下界结论主要是针对单进程程序的执行, 所以这里不考虑并发性对结果的影响.Ackermann函数A(m, n)是著名的非原始递归函数, 其定义如下所示:

$ A(m, n) = \left\{ {\begin{array}{*{20}{l}} {n + 1, }&{{\mathop{\rm if}\nolimits} \;m = 0}\\ {A(m - 1, 1), }&{{\mathop{\rm if}\nolimits} \;n = 0}\\ {A(m - 1mA(m, n - 1)), }&{{\rm{otherwise}}} \end{array}} \right.. $
Fig. 1 Computing Ackermann function A(2, n) with only one local variable 图 1 只用1个局部变量计算Ackermann函数A(2, n)

Ackermann函数是严格单调的.

图 1左侧为计算A(2, n)的程序, *是布尔表达式, 不确定地计算出true或false, 与WSPDS中不允许0测试(测试一个值是否为0)相一致.这段程序只要求第1个参数为固定参数, 主要是为了表明程序的局部变量可以被编码到相对应的良结构下推系统的栈字符集中, 为第4节栈字符为向量集的良结构下推系统可用于建模的相关程序提供一个直觉上的例子.该程序不能精确地计算出A(2, n), 但可以保证计算出的最大值是A(2, n).右侧为与程序对应的WSPDS, 状态对应于左侧程序的行号, 栈字符是函数名x∈{B0, B1, B2}和局部变量自然数x组成的序对.状态间的迁移描述了栈上的操作, 例如在状态3时的迁移(B2, x)→(B2, x-1)(B1, x)表示x≥1时, 将原栈顶(B2, x)替换成(B1, x)后压入(B2, x-1), 这种规则称为入栈规则.状态15到状态8的迁移依次弹出两个元素(B0, x)(B1, x′)后压入新栈顶(B1, x), 这种称为非标准的出栈规则.

递归的自然数程序可以被建模成良结构下推系统, 可将局部的自然数变量编码到栈向量, 可将全局的自然数变量编码到状态向量.用良结构下推系统的栈字符向量编码并发的递归程序的活动的进程数[9].因此, 递归程序的某一点是否可达可以转换成良结构下推系统的可覆盖性问题.

本文展示了基于重置0的证明模型的可覆盖性问题难度下界的通用方法, 所谓重置0是指直接对变量赋值为0.我们证明了一旦一个模型可以正向弱计算和反向弱计算一个函数f, 则其可覆盖性问题的难度的下界就是f难的.另外, 还证明了具有栈字符集为n维向量集的良结构下推系统的可覆盖性问题的下界是Hyper- Ackermann难的.并且利用本文提出的方法重新证明了具有状态集为三维自然数向量集的良结构下推系统的可覆盖性问题的下界是TOWER难的.

对于可覆盖性和可达性的复杂性证明有如下一些工作:Lipton给出最有名的向量加法系统的下界[10].证明了其可覆盖性问题和可达性问题是EXPSPACE的, 主要思想是用并行程序设置固定上界的计数器设置“精确地”0测试.Lazic[11]使用与Lipton相同的方法, 证明了状态为向量集的下推系统的可覆盖性问题的下界是TOWER难的, Schnoebelen等人的工作[12, 13]使用重置0的技巧, 证明了重置Petri网的可覆盖性问题是Ackermann难的, 也是本文借鉴使用的方法.在Schnoebelen等人的证明中, 重置Petri网的维度必须与要得到的其可覆盖性问题的难度Ackermann(m, n)中的参数m相关, 因此整个规约过程相对输入大小不是多项式的.但在良结构下推系统中, 因为有栈的存在, 保证了其可覆盖性问题下界的证明是多项式的, 且独立于参数的大小.Demri等人[14]证明了分支向量加法系统的可覆盖性问题是2EXPTIME完备的.Lazic[15]证明了分支向量加法系统的可达性问题是2EXPSPACE难的.Bonnet[16]证明了允许一个计数器用于0测试的向量加法系统的可达性问题是可判定的.不对称的带状态的向量加法系统的可达性问题是不可判定的[17-19], 但其自底向上的可覆盖性问题是Ackermann完备的[20].

本文第2节介绍后文将用到的一些基础符号和良结构下推系统、Hyper-Ackermann函数和2-计数机器的定义.第3节介绍证明可覆盖性问题的难度的一般性方法.第4节给出证明, 得出栈字符集为n维向量集的良结构下推系统的可覆盖性问题的下界是Hyper-Ackermann的.第5节采用本文提出的方法重新证明状态为向量集的下推系统的可覆盖性问题的下界是TOWER难的, 与Lazic[11]的结果一致.第6节总结全文, 并展望未来工作.

2 预备知识

$\mathbb{N}$为自然数集, $\mathbb{Z}$为整数集, ${{\mathbb{Z}}^{k}}$(或$\mathbb{Z}$k)表示k维的自然数(或整数)向量集.n, m表示k维的自然数向量, a, a′表示k维的整数向量, nk表示向量n的第k维分量.令p, q等表示状态, α, β等表示栈字符, w, v表示栈上的字, 其长度分别为|w|和|v|.用c, d表示格局.|Γ| < ∞表示Γ是有限集.

在迁移规则中使用→表示迁移关系.用$ \mapsto $表示格局之间的单步迁移, $ \mapsto ^*$表示格局之间的多步迁移.

2.1 良结构下推系统

定义2.1. 一个良结构下推系统是一个三元组, 其中,

● P是有限的状态集, 或者给定一个具体的维度k, P=${{\mathbb{Z}}^{k}}$;

● Γ是有限的栈字符集, 或者给定一个具体的维度d, Γ=${{\mathbb{N}}^{d}}$;

● Δ是有限的单调偏函数的集合:P×Γ≤2P×Γ≤2.

单调性是指对p, qP, w, v∈Γ≤2, 若(p, wq, v)∈Δ, 则对任意p′≥p, w′≫w, 有(p′, w′→q′, v′)∈Δ且q′≥q, v′v.这里,≫是≥在Γ*上的按位扩展, 即:a1a2...amb1b2bn, 当且仅当对任意的i, aibim=n.如果移除了单调性, 良结构下推系统就会变得图灵完备.

下推向量加法系统是栈字符集有限且状态集为k维自然数向量集的良结构下推系统, 即P=${{\mathbb{N}}^{k}}$, |Γ| < ∞.

良结构下推系统的格局$ \langle p, w\rangle $是由状态p和栈上的字w组成的序对.格局间的单步迁移$ \mapsto $是格局的重写, $ \mapsto ^*$$ \mapsto $的自反传递闭包.

$ \frac{{(p, w \to q, v) \in \Delta }}{{\langle p, ww'\rangle \mapsto \langle q, vw'\rangle }}.$

给定初始格局c0=〈p, w〉和目标格局cf=〈q, v〉, 良结构下推系统的可达性问题是判断${c_0}{ \mapsto ^ * }{c_f}$是否成立, 可覆盖性问题是对任意cg=〈q′, v′〉且q′≥q, v′v, 判断${c_0}{ \mapsto ^ * }{c_g}$是否成立.

例2.1:一个良结构下推系统$ M=\langle (\mathbb{N}, \le ), (\mathbb{N}, \le ), \Delta \rangle $, 迁移规则Δ如下:

$ \Delta = \left\{ \begin{array}{l} {r_1}:p, \alpha \to p + 6, (\alpha - 6)(\alpha - 6), ~{\rm{ if }}~\alpha \ge 6\\ {r_{2}}:p, \varepsilon \to p - 6, 6, ~~~~~~~~~~~~~~~~~~~~~~{\rm{ if }}~p \ge 6 \end{array} \right..$

给定初始格局c0=〈6, 0〉, 则存在一个如下的格局迁移序列:

$ \langle 6, 0\rangle \mapsto \langle 0, 60\rangle \mapsto \langle 6, 000\rangle \mapsto \langle 0, 6000\rangle \mapsto \langle 6, 00000\rangle \mapsto ... $

可见, 格局〈6, 000〉是从初始格局可达的, 而格局〈0, 5000〉虽然不可达, 但可被覆盖.

2.2 Hyper-Ackermann函数

康托尔在1883年提出了序数的概念[21], 引入了无限的序列.ω是最小的无限序数.按照康托尔正规式的表示方法, 每一个limit序数λ都可以被唯一地分解成$ {\omega ^{{d_{^{_1}}}}}.{c_1} + {\omega ^{{d_{^2}}}}.{c_2} + ... + {\omega ^{{d_{^k}}}}.{c_k}$, 其中, k是自然数, c1, c2, …, ck是正整数, d1 > d2 > … > dk≥0是序数.每一个limit序数λ都有一个唯一的基础序列(λn)n$\mathbb{N}$.对小于ωω的limit序数, 其基础序列为

$ {\left( {{\omega ^{{d_1}}}.{c_1} + {\omega ^{{d_2}}}.{c_2} + ... + {\omega ^{{d_k}}}.{c_k}} \right)_n} = {\omega ^{{d_1}}}.{c_1} + ... + {\omega ^{{d_{k - 1}}}}.{c_{k - 1}} +\\ {\omega ^{{d_k}}}.\left( {{c_k} - 1} \right) + {\omega ^{{d_{k + 1}}}}.\left( {n + } \right.\left. 1 \right). $

定义2.2. Fast-Growing函数族按下标序数为aωω索引定义如下[6]:

$ \begin{array}{l} {F_0}(n) = n + 1, \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;{F_{\alpha + 1}}(n) = F_\alpha ^{n + 1}(n) = \overbrace {{F_\alpha }({F_\alpha }(...{F_\alpha }(n)...))}^{n + 1}, \\ {F_\lambda }(n) = {F_{{\lambda _n}}}(n), \lambda < {\omega ^\omega }, \;\;\;\;\;{F_{{\omega ^\omega }}}(n) = {F_{{\omega ^{n + 1}}}}(n). \end{array}$

F1(n)是n的线性函数, F2(n)是n的指数函数, $ {F_{{\omega ^\omega }}}(n)$是Hyper-Ackermann函数.

例2.2:

$ \begin{array}{l} {F_{{\omega ^\omega }}}(3) &= {F_{{\omega ^4}}}(3)\\ ~~~~~~~~~~~~~{\rm{ }} &= {F_{{\omega ^3}.4}}(3)\\ ~~~~~~~~~~~~~{\rm{ }}& = {F_{({\omega ^3}.3 + {\omega ^2}.\left. 4 \right)}}(3) = {F_{({\omega ^3}.3 + {\omega ^2}.\left. {3 + \omega .4} \right)}}(3) = {F_{({\omega ^3}.3 + {\omega ^2}.\left. {3 + \omega .3 + 4} \right)}}(3)\\ ~~~~~~~~~~~~~{\rm{ }} &= {F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\left( {{F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\left( {{F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\\\left( {{F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\left( 3 \right)} \right)} \right)} \right)\\ ~~~~~~~~~~~~~{\rm{ }}& = ... \end{array}$

引理2.2. Hyper-Ackermann函数是严格单调的, 即对任何n′ > n, $ {F_{{\omega ^\omega }}}(n') > {F_{{\omega ^\omega }}}(n).$

2.3 2-计数机器

定义2.3. 一个计数机器是一个三元组M=〈P, C, Δ〉, 其中, P是有限的状态集, C是有限的计数器的集合, Δ$\subseteq $P× op(CP是有限的迁移规则.指令集op(C)是按如下方式定义的规则集(CiM的第i个计数器):

$ op:: = {C_i} = 0?{\rm{ | }}{C_i} + + {\rm{ | }}{C_i} > 0?{C_i} - - $

计数机器的格局是一个序对〈p, n〉, 其中, pP表示当前的状态, n$\mathbb{N}$|C|表示每个计数器当前的内容.格局之间的迁移$\langle p, {\bf{n}}\rangle \mapsto \langle q, {\bf{m}}\rangle $成立当且仅当如下情况之一成立.

● 若(p, Ci=0?, q)∈Δ且ni=0, 则m=n;

● 若(p, Ci++, q)∈Δ, 则mi=ni+1且对jimj=nj;

● 若(p, Ci > 0?Ci- -, q)∈Δ且ni > 0, 则mi=ni-1且对jimj=nj.

给定初始格局〈p0, 0〉和目标格局〈pf, 0〉, 计数机器的可达性问题是判断格局的执行序列$ \langle {p_0}, 0\rangle { \mapsto ^ * }\langle {p_f}, 0\rangle $是否成立.

2-计数机器(只有2个计数器)是图灵完备的[22], 其可达性问题是不可判定的.然而, 如果给每个计数器设定一个上界, 即每个计数器的值不超过这个上界值, 则2-计数机器的计算能力就得到了限制, 其可达性问题就是可判定的.例如, 输入的大小为n, 上界值是$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$, 可达性问题是TOWER难的; 上界值为Hyper-Ackermann函数$ {F_{{\omega ^\omega }}}(n), $可达性问题是Hyper-Ackermann难的[23].

这里给定2-计数机器设定一个上界B, 使得在格局迁移的过程中所有的计数器的值的总和不超过上界, 记为$ \langle p, {\bf{n}}\rangle { \mapsto ^B}\langle q, {\bf{m}}\rangle $.$ { \mapsto ^{{B^ * }}}$$ { \mapsto ^B}$的自反传递闭包.

3 可覆盖性问题的下界

我们的证明技巧基于Schnoebelen等人在文献[12, 13]中提出的将Ackermann-bound的2-计数机器的可达性问题规约到重置Petri网的可覆盖性问题.本节不针对任何具体的模型, 只是给出具体的规约的思路:将以f(x)为界的2-计数机器的可达性问题规约到某个特定模型M的可覆盖性问题, 注意, 这里的f(x)应该是严格单调的函数.

简单来说, 规约由3部分构成.

● 输入为n, MH计算f(n)的值;

● Mb模拟以f(x)为界的2-计数机器;

● $ M_H^{ - 1}$逆向计算f(n).

MH根据输入向量n计算一个上界值B, 最大为f(n), 将这个值传递给Mb, 触发Mb的执行.Mb执行后, B的值可能会变小(错误的模拟)或保持不变(正确的模拟).然后将值传递给第3部分$ M_H^{ - 1}$进行逆向计算, 即根据B的值求对应的向量n′.函数f(n)严格的单调性, 保证如果B < f(n), n′≯n, 即n′不能覆盖n.只有正确的模拟才能保证最后的可覆盖性成立.当可覆盖性成立时, Mb精确地模拟了以f(x)为界的2-计数机器的执行, 所以M的可覆盖性问题的下界为f-难的.相关思想如图 2所示($ M_{CM}^b$是以f(x)为界的2-计数机器, 下文将具体介绍其构造).

Fig. 2 Reduction from the reachability problem of 2-counter machine with f(x) bounds to the coverability problem of M 图 2 从以f(x)为界的2-计数机器的可达性问题到M的可覆盖性问题的规约

3.1 有界的2-计数机器的模拟

给定2-计数机器M=〈P, C, Δ〉, 有界的2-计数机器$ M_{CM}^b{\rm{ = }}\langle P', C \cup \left\{ b \right\}, \Delta '\rangle , $初始化P′=P, Δ′=Ø, 根据Δ中的每一条规则(p, op(C), q)按如下方式构造$ M_{CM}^b.$

● 若op(C)=Ci++, 则对新状态s$\notin $P′, P′=P$ \cup ${s},

$ \Delta ' = \Delta ' \cup \left\{ {\left( {p, b > 0?b - - , s} \right), \left( {s, {C_i} + + , q} \right)} \right\}$

● 若op(C)=Ci=0?, 则Δ′=Δ′$\cup ${p, Ci=0?q};

● 若op(C)=Ci > 0?Ci- -, 则对新状态s$\notin $P′, P′=P$ \cup ${s},

$ \Delta ' = \Delta ' \cup \left\{ {\left( p \right., {C_i} > 0?{C_i} - - , \left. s \right), \left( s \right., b + + , \left. q \right)} \right\}.$

$ M_{CM}^b$的构造具体如图 3所示.

Fig. 3 Construct bounded 2-counter machine from 2-counter machine 图 3 从2-计数机器构造相应的有界的2-计数机器

$ M_{CM}^b$M添加了一个上界计数器, 记为b, 保证在对应的2-计数机器的格局迁移的过程中所有计数器的和不发生改变(在添加的新状态上可能总和会暂时地变大或变小, 但在原始对应的2-计数机器中状态上的计数器的和是固定的).根据i1+i2+b的大小, $ M_{CM}^b$的可达性问题具有相应的难度.

但是由于很多模型都没有测0能力, 因此本文使用重置0操作代替测0, 即将图 3中的i1=0?用i1=0来代替, 构造相应的模型Mb.Mb的构造如图 4所示.

Fig. 4 Mb simulate bounded 2-counter machine 图 4 Mb模拟有界的2-计数机器

注意, 在Mb中, i1+i2+b的和可能会变小, 虽然一旦对一个非0的计数器置0, 但却并未对有界计数器增加相应的数量.在Mb的格局迁移过程中, 如果i1=0从未执行或者仅仅执行在对一个值已经为0的变量上, 则所有计数器的和保持不变, Mb精确地模仿了$ M_{CM}^b$的格局迁移; 如果对一个非0的计数器执行了重置0操作, 所有计数器的和就会变小, 这种情况下, Mb$ M_{CM}^b$会产生不同的格局序列, 即Mb并未精确地模仿$ M_{CM}^b$反之, 如果在Mb的格局迁移中, 所有计数器的和始终保持不变(注意, 这里的始终也是对应于原始的2-计数机器的状态上), 则每一次可能存在的重置0操作都精确地模仿了有界的2-计数机器上的测0操作.

引理3.1. $ M_{CM}^b$是如图 3构造的有界的2-计数机器, Mb是如图 4构造的模型(以下的状态p, q均对应于图 3中原始的2-计数机器M中的状态).

● 如果$ M_{CM}^b$中存在$ \langle p, ({i_1}, {i_2}, b)\rangle { \mapsto ^ * }\langle q, ({i'_1}, {i'_2}, b')\rangle $的格局迁移序列, 则Mb中也存在相同的格局迁移序列, 且$ {i_1} + {i_2} + b = {i'_1} + {i'_2} + b'.$

● 如果Mb中存在$\langle p, ({i_1}, {i_2}, b)\rangle { \mapsto ^ * }\langle q, ({i'_1}, {i'_2}, b')\rangle $的格局迁移序列, 则$ {i_1} + {i_2} + b \ge {i'_1} + {i'_2} + b'.$但是, 如果${i_1} + {i_2} + b = {i'_1} + {i'_2} + b', $$ M_{CM}^b$中必然存在$ \langle p, ({i_1}, {i_2}, b)\rangle { \mapsto ^ * }\langle q, ({i'_1}, {i'_2}, b')\rangle $的格局迁移序列.

3.2 函数f(n)的正向计算和逆向计算

函数f(n)的定义域为k维的自然数向量n, 且严格单调, 即对任意i∈[1...k], 若${n'_i} > {n_i}, $则有

$ f\left( {{n_1}, ..., {{n'}_i}, ..., {n_k}} \right) > f\left( {{n_1}, ..., {n_i}, ..., {n_k}} \right).$

因为我们要研究的模型不是图灵完备的, f(n)的正向和逆向计算可能不精确, 但这并不影响我们的结论, 因为Mb的格局迁移中不会增大f(n)的值.因此, 如果MH计算出的上界值B不大于f(n), 则经过Mb后, B依旧不大于f(n), $ M_H^{ - 1}$逆向计算后得到的n′≯n.

定义3.2. 给定输入n, 如果MH计算出的最大的值为f(n), 则称MH弱计算函数f(n).

给定输入B′, 设$ M_H^{ - 1}$逆向计算出来的值的集合为S, 满足:

● 若f(n)=B′, 则nS;

● 若nS, 则f(n)≤B′,

则称$ M_H^{ - 1}$逆向弱计算函数f(n).

图 2所示, 模型M的格局的迁移由MHMb$ M_H^{ - 1}$组成.MH完成计算后, 触发Mb中的p0, 并把计算得到的B传递给Mb.Mb中格局迁移到状态为pf的格局时触发$ M_H^{ - 1}$执行.3部分共享相同的计数器.MH的最终状态连接Mb中的p0, pf连接到$ M_H^{ - 1}$的初始状态.

定理3. f是严格单调的k元函数.MH弱计算函数f(n)$ M_H^{ - 1}$逆向弱计算函数f(n).$ M_{CM}^b$是如图 3构造的有界的2-计数机器, Mb图 4构造的模拟有界的2-计数机器的模型.MH的输入是k维向量n.

● 若在$ M_{CM}^b$中存在$ \langle {p_0}, (0, 0, b)\rangle { \mapsto ^*}\langle {p_f}, (0, 0, b')\rangle $的格局迁移序列, 则$ M_H^{ - 1}$逆向计算得到的最大值是n;

● 若$ M_H^{ - 1}$逆向计算得到的n′≥n, 则在$ M_{CM}^b$中必然存在$ \langle {p_0}, (0, 0, b)\rangle { \mapsto ^*}\langle {p_f}, (0, 0, b)\rangle $的格局迁移序列.

证明:

● 在$ M_{CM}^b$中存在$ \langle {p_0}, (0, 0, b)\rangle { \mapsto ^*}\langle {p_f}, (0, 0, b')\rangle $的格局迁移序列, 由引理3.1可知, Mb中也存在相同的格局迁移序列$ \langle {p_0}, (0, 0, b)\rangle { \mapsto ^*}\langle {p_f}, (0, 0, b')\rangle , $$ b = b' \le f({\bf n}).$又因为$ M_H^{ - 1}$逆向弱计算f(n), 所以$ M_H^{ - 1}$输出的最大值是n;

● 若$ M_H^{ - 1}$弱逆向计算得到的n′≥n, 则传递给$ M_H^{ - 1}$$ b' \ge f(n).$又由图 2中3部分的连接情况可得, Mb中存在格局迁移序列$ \langle {p_0}, (0, 0, b)\rangle { \mapsto ^*}\langle {p_f}, ({i'_1}, {i'_2}, b')\rangle , $又有MH弱计算函数f(n), 则$ f({\bf{n}}) \ge b \ge b' + {i'_1} + {i'_2} \ge f({\bf{n}}), $所以, b= b'=f(n), 即Mb中存在格局迁移序列$ \langle {p_0}, (0, 0, b)\rangle { \mapsto ^*}\langle {p_f}, (0, 0, b)\rangle $(Mb的格局迁移中所有计数器s的和保持不变, 表明Mb中的每次重置0操作都精确地模拟了测0), 由引理3.1可得, $ M_{CM}^b$中必然存在$ \langle {p_0}, (0, 0, b)\rangle { \mapsto ^*}$$ \langle {p_f}, $ $ (0, 0, b)\rangle $的格局迁移序列.证毕.

4 良结构下推系统的可覆盖性问题下界

本节考虑良结构下推系统的子模型:状态为有限集而栈字符为向量, 即$ M = \langle |P| < \infty , \Gamma = {{\rm{N}}^{n + 3}}, \Delta \rangle $(其中, n为要计算的函数给定的参数值).该模型可正向和逆向弱计算Hyper-Ackermann函数的值.由定理3可得, 其可覆盖性问题是Hyper-Ackermann难的.

4.1 (正向)弱计算Hyper-Ackermann函数

给定一个良结构下推系统Mr=〈{● }, $\mathbb{N}$n+3, Δ〉, 其中, 状态集为单字符集, 栈字符集为n+3维自然数向量的集合(因为只有一个状态, 所以迁移规则中省去了状态, 仅描述栈上的迁移), 迁移规则为

$ \Delta = \left\{ \begin{array}{l} {r_1}:\left( {{k_n}, {k_{n - 1}}, ..., {k_0}, t, x} \right) \to\\ \left( {{k_n}, {k_{n - 1}}, ..., {k_0} - 1, x, x} \right)\\ {r_2}:\left( {{k_n}, {k_{n - 1}}, ..., {k_0}, t, x} \right) \to\\ \left( {{k_n}, {k_{n - 1}}, ..., {k_0}, 0, x} \right)\left( {{k_n}, {k_{n - 1}}, ..., {k_0}, t - 1, x} \right)\\ {r_3}:\left( {\underbrace {{k_n}, {k_{n - 1}}, ..., {k_i}, ..., 0}_{n + 1}, 0, x} \right) \to \\\left( {\underbrace {{k_n}, {k_{n - 1}}, ..., {k_i} - 1, x + 1, ..., 0}_{n + 1}, 0, x} \right), i \in \left[ {1, n} \right]\\ {r_4}:\left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x} \right)\left( {{{k'}_n}, {{k'}_{n - 1}}, ..., {{k'}_0}, t', x'} \right) \to \\\left( {k', {{k'}_{n - 1}}, ..., k', t', x + 1} \right) \end{array} \right.. $

按照迁移规则中所示, 栈向量的前n+1个分量都标记了下标, 例如k0就表示该向量的从左向右第n+1个分量.以下描述都直接使用这一表示方法.规则r1对栈顶元素进行在某些分量上值的修改; r2将栈顶元素的第n+1个分量进行修改并压入新向量(kn, kn-1, …, 0, x); r3表示当i在[1, n]区间内(含两端)时, 都可执行r3的迁移; r4表示当栈顶的前n+2个分量都是0时, 可执行出栈操作, 并将最后一个分量值传递给栈顶的下一个元素, 形成新的栈顶.注意, 每条迁移规则都代表单调函数, 例如对r4, 任何向量只要其所有分量值均不小于0, 都有此迁移, 即

$ \left( {{p_n}, {p_{n - 1}}, ..., {p_0}, te, xp} \right)\left( {{{k'}_n}, {{k'}_{n - 1}}, ..., {{k'}_0}, t', x'} \right) \to \left( {{{k'}_n}, {{k'}_{n - 1}}, ..., {{k'}_0}, t', xp + 1} \right). $

这里写r4只是方便理解.

引理4.1. Mr可弱计算Hyper-Ackermann函数, 且

$ hyper(n) = \max \left\{ {x + 1{\rm{ }}|{\rm{ }}\left\langle { \bullet , {\rm{ }}\left( {\underbrace {n + 1, 0, ..., 0}_{n + 1}, 0, n} \right) \bot } \right\rangle {\rm{ }}{ \mapsto ^ * }\\{\rm{ }}\left\langle { \bullet {\rm{, }}\left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x} \right) \bot } \right\rangle {\rm{ }}} \right\}, $

其中, $\bot $为栈底元素.

证明:首先, 因为如定义2.2所示, 给定参数n后, Hyper-Ackermann函数没有升幂操作(除了一开始的$ {F_{{\omega ^\omega }}}(n) = {F_{{\omega ^{n + 1}}}}(n), $$ {F_{{\omega ^\omega }}}(n) = {F_{{\omega ^{n + 1}}}}(n), $可直接应用$ {F_\lambda }(n) = {F_{{\lambda _n}}}(n), \lambda < {\omega ^\omega }$降幂), ωn.kn+ωn-1.kn-1+…+ω0.k0的形式固定, 即最高幂次是n, 栈向量的前n+1个分量(kn, kn-1, …, k0)对应于ωn.kn+ωn-1.kn-1+…+ω0.k0n+1个系数.简单来说, 迁移规则r1r2描述$ {F_{\alpha + 1}}(n) = F_\alpha ^{n + 1}(n) = \overbrace {{F_\alpha }\left( {{F_\alpha }\left( {...{F_\alpha }(n)...} \right)} \right)}^{n + 1}, $求出内层函数值(栈顶向量的前n+1个分量都是0, 对应F0(n)=n+1)之后应用r4出栈, 并将内层结果值保存在最后一个分量上传递给下一个向量, 构成新栈顶进行计算.迁移规则r3对应Hyper-Ackermann函数计算规则$ {F_\lambda }(n) = {F_{{\lambda _n}}}(n), \lambda < {\omega ^\omega }.$

其次, 栈顶元素可分为以下3类.

(1) 栈顶为(kn, kn-1, …, k0, t, x)形式, 对应接下来需要计算的Hyper-Ackermann函数为$F_{{\omega ^n}.{k_n} + {\omega ^{n - 1}}.{k_{n - 1}}... + {\omega ^0}.{k_0}}^t(x), $首先计算内层函数, 直接应用r2入栈新元素(kn, kn-1, …, k0, 0, x)表明接下来要计算$F_{{\omega ^n}.{k_n} + {\omega ^{n - 1}}.{k_{n - 1}}... + {\omega ^0}.{k_0}}^{}(x), $并将(kn, kn-1, …, k0, t-1, x)(对应$F_{{\omega ^n}.{k_n} + {\omega ^{n - 1}}.{k_{n - 1}} + ... + {\omega ^0}.{k_0}}^{t - 1}(x))$变为栈顶的下一个元素.根据归纳假设, 栈顶会变为$\left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x} \right), $对应F0(x), 即$F_{{\omega ^n}.{k_n} + {\omega ^{n - 1}}.{k_{n - 1}} + ... + {\omega ^0}.{k_0}}^{}(x)$的结果为x+1.再应用r4将结果作为下一个函数的参数进行后续计算.

(2) 栈顶为$\left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x} \right)$形式, 已在(1)中说明.

(3) 栈顶为$\left( {\underbrace {{k_n}, {k_{n - 1}}, ..., {k_i}, ..., 0}_{n + 1}, 0, x} \right)$形式, 接下来需要计算的Hyper-Ackermann函数为$F_{{\omega ^n}.{k_n} + {\omega ^{n - 1}}.{k_{n - 1}} + ... + {\omega ^i}.{k_i}}^{}(x)$i≠0.应用r3生成新栈顶$\left( {\underbrace {{k_n}, {k_{n - 1}}, ..., {k_i} - 1, x + 1, ..., 0}_{n + 1}, 0, x} \right), $$F_{{\omega ^n}.{k_n} + {\omega ^{n - 1}}.{k_{n - 1}} + ... + {\omega ^i}.({k_i} - 1) + {\omega ^{i - 1}}.(x + 1)}^{}(x), $与Hyper函数计算规则$ {F_\lambda }(n) = {F_{{\lambda _n}}}(n), \lambda < {\omega ^\omega }$保持一致.

但是, 因为Mr的迁移规则具有单调性, 相比正确的格局迁移, 可能存在错误的格局迁移, 如应使用r3却使用了r4, 表明$F_{{\omega ^n}.{k_n} + {\omega ^{n - 1}}.{k_{n - 1}} + ... + {\omega ^i}.{k_i}}^{}(x)$i≠0的值直接被看作x进行后续计算, 造成数据丢失.如果在格局迁移过程中没有任何数据丢失, 则当格局处于$\left\langle { \bullet {\rm{, }}\left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x} \right) \bot } \right\rangle $x+1就是正确的结果.证毕.

例4.1:利用引理4.1计算$ hyper(1) = {F_{{\omega ^\omega }}}(1) = {F_{{\omega ^2}}}(1), $以验证其正确性.相关的格局迁移序列如下(这里, 仅列出栈上的迁移, 因只有一个状态):

$ \begin{array}{l} \left( {2, 0, 0, 1} \right) \bot \mathop \mapsto \limits^{{r_3}} \left( {1, 2, 0, 1} \right) \bot \mathop \mapsto \limits^{{r_1}} \left( {1, 1, 1, 1} \right) \bot \mathop \mapsto \limits^{{r_2}} \left( {1, 1, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_1}} \left( {1, 0, 1, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {1, 0, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_3}} \left( {0, 2, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_1}} \left( {0, 1, 1, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 1, 0, 1} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{\rm{ }}{r_1}} \left( {0, 0, 1, 1} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot\\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 0, 0, 1} \right)\left( {0, 0, 0, 1} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 0, 2} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_4}} \left( {0, 1, 0, 3} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_1}} \left( {0, 0, 3, 3} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 0, 0, 3} \right)\left( {0, 0, 2, 3} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 2, 4} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 0, 0, 4} \right)\left( {0, 0, 1, 4} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 1, 5} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{\rm{ }}{r_2}} \left( {0, 0, 0, 5} \right)\left( {0, 0, 0, 5} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 0, 6} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_4}} \left( {1, 0, 0, 7} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{\rm{ }}{r_3}} \left( {0, 8, 0, 7} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_1}} \left( {0, 7, 7, 7} \right)\left( {1, 1, 0, 1} \right) \bot \mathop \mapsto \limits^{{r_2}} ... \end{array} $

最后的(0, 7, 7, 7)(1, 1, 0, 1)表示${F_{\omega + 1}}(F_7^8(7)), $之后继续利用迁移规则计算, 直至计算至栈中为(0, 0, 0, x)$\bot $时, x+1为hyper(1)的值.

4.2 逆向弱计算Hyper-Ackermann函数

如果仅仅把Mr的迁移规则逆过来, 就构造了逆向弱计算Hyper-Ackermann值对应参数的良结构下推系统$ {M_{{r^{ - 1}}}}.$给定一个Hyper-Ackermann的值, 初始格局是$\left\langle { \bullet , \left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x - 1} \right) \bot } \right\rangle $(这里的n可任意, 但是一旦给定一个n, 之后的栈上的元素都是固定维度的), 只要可到达$ \left\langle { \bullet , \left( {\underbrace {n + 1, 0, ..., 0}_{n + 1}, 0, n} \right) \bot } \right\rangle , $最后的n就是对应hyper(n)=x的参数n.虽然$ {M_{{r^{ - 1}}}}$的规则是单调的, 但每次错误的计算都会造成最后得到比正确的参数n还要小的参数值.

引理4.2. $ {M_{{r^{ - 1}}}}$可逆向弱计算Hyper-Ackermann函数.

定理4. 给定特定的良结构下推系统, 其状态集有限, 栈字符集为n+3维的良拟序集, 则其可覆盖性问题的下界是Hyper-Ackerman难的.

证明:因为重置0操作是单调的, n+3维的良结构下推系统可以作为Mb.Mb, Mr$ {M_{{r^{ - 1}}}}$共同构成良结构下推系统.由定理3可得, 当其可覆盖性问题得到解决时, $ M_{CM}^b$中必然存在$ \langle {p_0}, (0, 0, hyper(n)\rangle { \mapsto ^*}\langle {p_f}, (0, 0, hyper(n))\rangle $的格局迁移序列.因后者是Hyper-Ackermann难的, 所以该良结构下推系统的可覆盖性问题的下界是Hyper- Ackermann难的.证毕.

5 下推向量加法系统的可覆盖性问题的下界的重新证明

本节考虑良结构下推系统的子模型:状态为向量而栈字符为有限集, 即$ M=\langle P={{\mathbb{N}}^{3}}, |\Gamma | < \infty , \Delta \rangle , $即下推向量加法系统.该模型可正向和逆向弱计算$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$的值.由定理3可得, 其可覆盖性问题是TOWER难的.

5.1 (正向)弱计算$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$函数

给定一个良结构下推系统${{M}_{p}}=\langle {{\mathbb{N}}^{3}}, \left( \left\{ a \right., \left. \bot \right\}, \ll \right), \Delta \rangle , $其中, 状态集为3维自然数向量的集合, 栈字符集为单字符集, 迁移规则$\Delta = \left\{ \begin{array}{l} {r_1}:\left( {\left( {n, 0, x} \right), \varepsilon } \right) \to \left( {\left( {n - 1, x, x} \right), \varepsilon } \right)\\ {r_2}:\left( {\left( {n, t, x} \right), \varepsilon } \right) \to \left( {\left( {n, t - 1, x + 1} \right), \varepsilon } \right).\\ {r_3}:\left( {\left( {0, 0, x} \right), a} \right) \to \left( {\left( {x - 1, 0, 2} \right), \varepsilon } \right){\rm{ }} \end{array} \right.$

引理5.1. Mp可弱计算$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$函数, 且

$ \underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n = \left\{ \begin{array}{l} \max \left\{ {x\left| {\left\langle {\left( {1, 0, 2} \right), \underbrace {aa...a}_{n - 2} \bot } \right\rangle { \mapsto ^ * }\left\langle {\left( {0, 0, x} \right), \bot } \right\rangle } \right.} \right\}{\rm{, }}~n \ge {\rm{2}}\\ 2, ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~n = 1 \end{array} \right., $

其中, $\bot $为栈底元素.

证明:对格局〈(n, t, x), ω$\bot $〉有:t=0时表示需要对x进行n次翻倍操作, 即求x×2n, 需使用规则r1; t≠0时表示需要把t的值加到x上, 需连续使用r2.以下运用数学归纳法证明.

● 当n=1时显然成立;

● 当n=2时, tower(2)=22=4.对Mp有如下格局迁移序列:$\langle (1, 0, 2), \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle (0, 2, 2), \bot \rangle \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle (0, 0, 4), \bot \rangle .$

● 假设n=k时题设成立, 则有$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_k = \max \left\{ {x\left| {\left\langle {\left( {1, 0, 2} \right), \underbrace {aa...a}_{k - 2} \bot } \right\rangle { \mapsto ^ * }\left\langle {\left( {0, 0, x} \right), \bot } \right\rangle } \right.} \right\}$成立, 则当n=k+1时, 起始格局为$\left\langle {\left( {1, 0, 2} \right), \underbrace {aa...a}_{k - 1} \bot } \right\rangle , $由3条迁移规则可得, 在格局迁移的过程中, 会迁移到格局为$\langle (0, 0, x), a \bot \rangle $$x = \underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_k.$那么, 之后的格局迁移为

$ \begin{array}{l} \langle \left( {0, 0, x} \right), a \bot \rangle \mathop \mapsto \limits^{{r_3}} \langle \left( {x - 1, 0, 2} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {x - 2, 2, 2} \right), \bot \rangle \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {x - 2, 0, 4} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \\\mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {x - 3, 0, 8} \right), \bot \rangle \\ \mathop \mapsto \limits^{{r_1}} \underbrace {\mathop { \mapsto ...}\limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} }_8\langle \left( {x - 4, 0, 16} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \underbrace {\mathop { \mapsto ...}\limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} }_{16}...\mathop \mapsto \limits^{{r_1}} \\\underbrace {\mathop { \mapsto ...}\limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} }_{{2^{\left( {x - 1} \right)}}}\langle \left( {0, 0, 2 \times {2^{\left( {x - 1} \right)}}} \right), \bot \rangle = \langle \left( {0, 0, {2^x}} \right), \bot \rangle , \end{array} $

对应的tower(k+1)的值是$ {2^x} = {2^{\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_k}} = \underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_{k + 1}, $n=k+1时成立.

但是, 因为Mp的迁移规则具有单调性, 相比正确的格局迁移, 可能存在如下情况的错误的格局迁移, 造成数据丢失.

● 当n > 0, t > 0时, 用了r1而不是r2, 即x+t被认为是x进行后续计算.

● 当n > 0, t > 0时, 用了r3而不是r2, 即(x+t)×2n被认为是x进行后续计算.

● 当n=0, t > 0时, 用了r3而不是r2, 即x+t被认为是x进行后续计算.

● 当n > 0, t=0时, 用了r3而不是r1, 即x×2n被认为是x进行后续计算.

如果在格局迁移过程中没有任何的数据丢失, 则当格局处于〈(0, 0, x), $\bot $〉时x就是正确的结果.证毕.

例5.1:利用引理5.1计算$ {2^{{2^2}}}, $以验证其正确性.相关的格局迁移序列如下:

$ \begin{array}{l} \langle \left( {1, 0, 2} \right), a \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {0, 2, 2} \right), a \bot \rangle \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {0, 0, 4} \right), a \bot \rangle \mathop \mapsto \limits^{{r_3}} \langle \left( {3, 0, 2} \right), \bot \rangle \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_1}} \langle \left( {2, 2, 2} \right), \bot \rangle \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {2, 0, 4} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {1, 4, 4} \right), \bot \rangle \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {1, 0, 8} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {0, 8, 8} \right), \bot \rangle \underbrace {\mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} ...\mathop \mapsto \limits^{{r_2}} }_8\langle \left( {0, 0, 16} \right), \bot \rangle . \end{array} $

因此, $ {2^{{2^2}}} = 16.$

5.2 逆向弱计算$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$函数

如果仅仅把Mp的迁移规则逆过来, 就构造了逆向弱计算$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$值对应参数的良结构下推系统$ {M_{{p^{ - 1}}}}.$给定一个$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$x, 初始格局是〈(0, 0, x), $\bot $〉, 只要可到达$\left\langle {\left( {1, 0, 2} \right), \underbrace {aa...a}_n \bot } \right\rangle , $最后得到的最大的n(即栈中除去栈底元素外元素的个数)就是对应x的参数n(每次错误的计算都会造成最后得到比正确的参数n还要小的参数值).

引理5.2. $ {M_{{p^{ - 1}}}}$可逆向弱计算$\underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n$函数.

定理5.  给定特定的良结构下推系统, 其状态集为三维的良拟序集, 栈字符集有限, 即三维的下推向量加法系统, 其可覆盖性问题的下界是TOWER难的.

证明:类似定理4的证明.因三维下推向量加法系统可以模拟Mb.所以, 由定理3可得, 其可覆盖性问题的下界是TOWER难的.证毕.

6 总结以及未来的工作

本文基于良结构下推系统, 采用重置0操作, 提出了一种证明模型的下界的通用方法, 证明了n维的良结构下推系统的可覆盖性问题的下界是Hyper-Ackermann难的, 还将其与程序中的全局变量或局部变量的个数相对应, 表明了有n个局部变量的程序的可达性分析问题是很难的, 为分析含无限定义域的变量(如整数域)的程序时采取重置0操作持否定态度, 鼓励将无限定义域限制在有限定义域处理.本文还重新证明了下推向量加法系统在三维情况下其可覆盖性问题就可达到TOWER难.

未来希望能够推广这种证明模型可覆盖性难度下界的方法, 探索更多向量加法系统的拓展模型的下界或比已知下界更高的下界.同时, 寻求证明良结构下推系统的可覆盖性问题难度的上界, 形成证明上界的一般性方法并进行对其他模型的应用推广.再进一步探究良结构下推系统的可覆盖性问题的判定性.

参考文献
[1]
Derick WD. Theory of Computation:A Primer. Boston: Addison-Wesley Longman Publishing Co, 1987.
[2]
Autebert JM, Berstel J, Boasson L. Context-Free languages and pushdown automata. Handbook of Formal Languages, 1997, 6(3): 111–174. [doi:10.1007/978-3-642-59136-5_3]
[3]
Abdulla PA, Čerāns K, Jonsson B, Tsay YK. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 2000, 160(1-2): 109–127. [doi:10.1006/inco.1999.2843]
[4]
Cai X, Ogawa M. Well-Structured pushdown systems. In: D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin: Springer-Verlag, 2013. 121-136.[doi: 10.1007/978-3-642-40184-8_10]
[5]
Jin Y, Cai XJ, Li GQ. Expressiveness of well-structured pushdown systems. Journal of Shanghai Jiaotong University, 2015, 49(8): 1084–1089. [doi:10.16183/j.cnki.jsjtu.2015.08.002]
[6]
Leroux J, Praveen M, Sutre G. Hyper-Ackermannian bounds for pushdown vector addition systems. In: Henzinger T, Miller D, eds. Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS). New York: ACM, 2014. Article 63.[doi: 10.1145/2603088.2603146]
[7]
Sen K, Viswanathan M. Model checking multithreaded programs with asynchronous atomic methods. In: Ball T, Jones RB, eds. Proc. of the Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2006. 300-314.[doi: 10.1007/11817963_29]
[8]
Kochems J, Luke Ong CH. Safety verification of asynchronous pushdown systems with shaped stacks. In: D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin: Springer-Verlag, 2013. 288-302.[doi: 10.1007/978-3-642-40184-8_21]
[9]
Bouajjani A, Emmi M. Analysis of recursively parallel programs. In: Field J, ed. Proc. of the 39th Annual ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. New York: ACM, 2012. 203-214.[doi: 10.1145/2103621.2103681]
[10]
Lipton RJ. The reachability problem requires exponential space[Ph.D. Thesis]. Department of Computer Science, Yale University, 1976.
[11]
Lazic R. The reachability problem for vector addition systems with a stack is not elementary. Computer Science, 2013. https://www.researchgate.net/publication/257410098_The_reachability_problem_for_vector_addition_systems_with_a_stack_is_not_elementary
[12]
Schnoebelen P. Revisiting Ackermann-Hardness for lossy counter machines and reset Petri nets. Lecture Notes in Computer Science, 2010, 6281: 616–628. [doi:10.1007/978-3-642-15155-2_54]
[13]
Haddad S, Schmitz S, Schnoebelen P. The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In: Logic in Computer Science. IEEE, 2012. 355-364.[doi: 10.1109/LICS.2012.46]
[14]
Demri S, Jurdziński M, Lachish O, Lazić R. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 2013, 79(1): 23–38. [doi:10.1016/j.jcss.2012.04.002]
[15]
Lazić R. The reachability problem for branching vector addition systems requires doubly-exponential space. Information Processing Letters, 2010, 110(17): 740–745. [doi:10.1016/j.ipl.2010.06.008]
[16]
Bonnet R. The reachability problem for vector addition system with one zero-test. In: Murlak F, Sankowski P, eds. Mathematical Foundations of Computer Science. Berlin: Springer-Verlag, 2011. 145-157.[doi: 10.1007/978-3-642-22993-0_16]
[17]
Lincoln P, Mitchell J, Scedrov A, Shankar N. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 1992, 56(1-3): 239–311. [doi:10.1016/0168-0072(92)90075-B]
[18]
Kanovich MI. Petri nets, Horn programs, linear logic, and vector games. Annals of Pure and Applied Logic, 1995, 75(1-2): 107–135. [doi:10.1016/0168-0072(94)00060-G]
[19]
Raskin JF, Samuelides M, Begin LV. Games for counting abstractions. Electronic Notes in Theoretical Computer Science, 2005, 128(6): 69–85. [doi:10.1016/j.entcs.2005.04.005]
[20]
Urquhart A. The complexity of decision procedures in relevance logic Ⅱ. The Journal of Symbolic Logic, 1999, 64(4): 1774–1802. [doi:10.2307/2586811]
[21]
Cantor G. Ueber unendliche, lineare Punktmannichfaltigkeiten. Mathematische Annalen, 1883, 21(4): 545–591. [doi:10.1007/BF01446819]
[22]
Minsky ML. Computation:Finite and Infinite Machines. Prentice-Hall, Inc., 1967.
[23]
Schmitz S, Schnoebelen P. The power of well-structured systems. In: D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin: Springer-Verlag, 2013. 5-24.[doi: 10.1007/978-3-642-40184-8_2]