Page 26 - 《软件学报》2026年第1期
P. 26
陈蔚骏 等: 向量加法系统可达性问题复杂性下界研究综述 23
eval d = do eval d,1 or eval d,2 or...or eval d,d ;
即可. 当然这里要求每次从 α 出发执行 eval d 都能选择到对应的 eval d,index(λ) , 这需要由 {eval d,i } i∈[d] 这一族程序模块的
性质来保证. 回顾公式 (15) 和 (16) 可知, 在 index(λ) = 1 和 index(λ) > 1 两种情况下, β(B 0 ) 分别为 α(B 0 ) 和 1+
2α(B 0 ), 因此构造 eval d,i 时我们将这两种情况区分开来. 注意, i = 1 时有 β(B 0 ) = 1+2α(B 0 ) 而非保持不变, 因此文
献 [15] 中对此情况的构造是错误的. 幸运的是, 我们可以通过重新设计程序弥补这一缺陷. 最终完整程序如
图 14 所示. 这里因为需要两重嵌套同时实现 loop at most (1+ B 0 ) times, 因此额外引入了计数器 b、b, 使得 b+b =
B = B 0 , 另一层使用 loop at most (1+ B) times 替代. 但每次对 B 0 进行增减操作时, 都需要对 B 同步.
...
0 , ,
reset ( A A )
reset ( A A ) 1 loop i
0 ,
loop 0 a -=1, a +=1,
0
0 a -=2, a +=1, loop at most (1 B+
0
loop at most (1 B+ 0 ) times 0 ) times
0 ,
1 a -=2, a +=2, dec ( a ... ,a ), rdec d , 1i+ ,
i
1 ,
1
rdec ,2 , rdec ,2 ; inc ( a ... ,a ) i
loop at most (1 B+
d d ) times
dec ( B ) 1
1 ,
loop at most (1 B+ ) times dec ( a ... ,a ), rdec d , 1i+ , i a +=1;
i
dec ( B ) i
0 b +=1, b +=1; loop at most (1 B+ ) times b − +=1;
1
i
i=1 i≥2
eval d,i 的两种不同情形
图 14
β, 令
若 eval d,i 0 的某次执行从对应非平凡 λ 的好格局 α 出发且每次循环都执行到了允许的最大次数后得到
i 0 = index(λ). 当 i 0 ⩾ 2 时, 若 2+α(B 0 ) 整除 α(A 0 ), 则有如下结论.
α(A 0 ) α(A 0 )
● 最外层循环每次将 a 0 减少 2+α(B 0 ), 将 a 0 加 1, 最多执行 次, 且最终 β(A 0 ) = .
2+α(B 0 ) 2+α(B 0 )
α(A 1 ) ( )
● 第 2 重循环最多执行 次, 每次执行 2+α(B 0 ) 次 rdec d,i 0 +1 , 最终 β A i 0 +1 = α(A i 0 +1 − A 1 ).
2+α(B 0 )
α(A 1 )(1+α(B 0 )) α(A 1 )
● 最内层循环最多执行 次, 每次 a 1 ,...,a i 0 −1 减 1, 从而 β(A i ) = , 1 ⩽ i < i 0.
2+α(B 0 ) 2+α(B 0 )
(
)
● ( ) ( ) −1, β B i 0 −1 = 1+α(B 0 ).
β B i 0 = α B i 0
( ) ( )
显然, β A i 0 = α A i 0 , 因此 i ⩽ i 0 +1 时, 计算结果与公式 (16) 一致, i ⩾ i 0 +1 时, rdec d,i 0 +1 可以保证 β 是 (i 0 + 1)-
好的, 因此 β 是对应编码 Eval(λ) 的好格局.
,
;
当 i 0 = 1 时, 同理可知, 最终 β(A 2 ) = α(A 2 − A 1 ) β(B 1 ) = α(B 1 )−1 β(B 0 ) = 1+2α(B 0 ). 若 2 整除 α(A 0 ), 则 β 是
对应编码 Eval(λ) 的好格局. 另外, Leroux [15] 证明了如下引理.
引理 14 [15] . 若 α 是一个对应非平凡编码 λ 的合法格局, 执行 eval d,i 后得到的 β 也是合法的; 若 β 是好的, 则 α
,
也是好的, 并且 i = index(λ) β 对应编码 Eval(λ).
此引理的证明只需假设从上到下 4 l、m、n、r 次, 根据程序推导出如下关系:
个循环分别执行了
( )
m ⩽ (1+α(B 0 ))l, n ⩽ (1+α(B 0 ))m, l+m ⩽ α(N 0 ), m+n ⩽ minα X j , r ⩽ 1+α(B 0 ) (17)
j∈[i]
( ) 是必要
随后对 α 和 β 进行分析即可, 由于步骤比较繁杂, 在此不再赘述. 值得注意的是, 关系 m+n ⩽ minα X j
j∈[i]
的, 这也解释了为何程序中总是出现形如 a i −=1, a i +=1 的语句: 尽管它们对 A i 没有作用效果, 但却可以限制循环
的次数. 上述分析可以总结成如下引理.
引理 15. 程序 eval d 满足如下两条性质.
eval d
1) 若 α 是对应非平凡编码 λ 的好格局且 α(A 0 ) 满足某些整除性条件时, 则存在 α −−−→ β 使得 β 是对应 Eval(λ)
的好格局.
eval d
2) 若 α 是对应非平凡编码 λ 的合法格局且 α −−−→ γ, 则 γ 也是合法格局; 若 γ 是好的, 则 α 也是好的且 γ 对应
编码 Eval(λ).
Leroux [38] 并没有严格给出一个放大器, 而是构造了一个 (1 + F d+1 (n))-生成器 Gen d = (P d ,X d ,(a,b,c),Z d ), 其功能
相当于一个无须输入计数器, 而是将 n 直接写进程序 P d 中的放大器. 其中, X d 包括上述所有的计数器 {b i ,b i } i∈[d] 0 、
{ }
、b、b 和新计数器 ; ∪ a d+1 ,a d+1 ,b . a、c 分别用于记录 A 0 、A 1 , 即对 A 0 、A 1 的每次
{a i ,a i } i∈[d+1] 0 a、c Z d = {b i ,b i } i∈[d] 0

