Page 29 - 《软件学报》2026年第1期

26 软件学报 2026 年第 37 卷第 1 期

inv : A,B,C 7→ (A+C)− A·4 , 本节均考虑这种形式的 inv-三元组 (见定义 3). 该不变量也可以理解为
B
令
( B ) B B
C = A 4 −1 , 之所以使用 4 −1 而非 4 是为了使得 B = 0 当且仅当 C = 0, 最终判定 c = 0 即可, 否则需要判定
c = a, 但这是非平凡的, 还需额外的程序实现. 除了这一点改动之外, Czerwiński 等人 [37] 的方法本质上还是递归构
造 F d (n)-放大器, 在有了前文技术的基础上, 本节仅作简单介绍.
x、y, 一次成功的测零不应当对
首先, 使用新三元组模拟测零的方式与前文中不同. 不妨设待测零计数器为
x、y 产生影响. 直观上, b 记录了允许模拟测零的次数, 因此每次模拟测零只需减 1 即可. 前文中我们总是维持 a+ x+
( b−1 ) b −1
y = A 不变, 但此时这并不适用, 因为这样测零后必须令 b,c 7→ b−1, c 4 −1 (4 −1) , 这显然不是容易的. 计算
可知, 单独维持 C 不变也不容易, 最佳选择是保持 A+C = a+ x+y+c 始终不变. 假设模拟测零前格局 α 满足 α(a+ x+
y)4 α(b) = α(a+ x+y+c), 简单计算可知, 模拟测零过程只需要完成变换:

(a,b,c, x,y) 7→ (4a+3x+3y,b−1,c−3a−3x−3y, x,y) (19)
a、x、y 计算正确即可. 这需要额外引
c 的作用是和 a、x、y 互补, 它的行为由其他计数器确定, 设计程序时确保
入辅助计数器 t, 新的 zero-test( x) 模块如图 18 所示, zero-test( y) 同理.

loop a -=1, c -=1, t +=2;
loop y -=1, x +=1, c -=1, t +=1;
loop t -=1, c -=1, a +=2;
loop x -=1, y +=1, c -=1, a +=1;
b -=1;
图 18 zero-test( x)

若格局 α 满足 α(a+ x+y+t)4 α(b) ⩽ α(a+ x+y+c) 则称为合法的; 若该式子取等且 α(t) = 0, 则称其为好的. 考
zero-test(x)
虑从合法格局出发的执行 α −−−−−−−→ β, 易知 β 是合法的; 若 β 是好的, 则 α 也是好的, 且 β(x) = α(x) = 0, β(y) = α(y),
zero-test(x)
说明待测零计数器确实是 0 且没有副作用; 若 α 是好的并且满足 α(x) = 0, 则存在 α −−−−−−−→ γ 使得 γ 是好的, 且
c = 0 是否成立, 可以推断出终止
γ(y) = α(y), γ(x) = 0, 说明本次模拟测零正常运行且没有副作用. 最终通过检验
格局是否是好的, 进一步确定程序中 B 次模拟测零是否成功.
接着考虑 F d (n)-放大器的构造. 若初始格局为 τ s = (a,b ,c ,A,B,X 1 ), 计算 τ t = (a,b,c,A ,F d (B)) 的过程需维持
′
′
′
′ B ′ ′ F d (B) B ′
a+c +c = A·4 , 这样可以充分利用 τ s 进行一些模拟测零等行为, 直至 c = 0. 最终根据 A ·4 = A·4 可以确定 A =
A·4 B−F d (B) . 考虑快速增长函数的等价定义: F 1 (n) = 2n−1, F k+1 (n) = F (n−1) (1), 首先构造 F 1 (n)-放大器 Ampl 1 = (P 1 ,X 1 ,
k
,
,
(a,b ,c ),(a,b,c),Z 1 ), 其中, X 1 = {a,b,c,b ,c ,t} Z 1 = {c } P 1 如图 19 所示.
′
′
′
′
′

loop a -=1, t +=1; loop a -=1, t +=1;
loop t -=1, a +=1, c′ -=3, c +=3; loop t -=1, a +=1, k c + ′ 1 -=3, k c′ +=3;
b′ -=1, b +=1; k b + ′ 1 -=1, k b +=1;
loop loop
loop a -=1, t +=2, c′ -=1; loop a -=1, t +=1;
loop c -=1, a +=2, c′ -=1; loop t -=1, a +=4, k c + ′ 1 -=3;
loop a -=1, c +=2, c′ -=1; loop c -=1, k c′ +=4, k c + ′ 1 -=3;
k
loop t -=8, c +=15, c′ -=8, a +=1; loop b -=1, k b′ +=1;
k
b′ -=1, b +=2; k P ; b + ′ -=1;
k
1
P 1 P k+1
图 19 F d (n)-放大器的构造

′
′
′
P 1 的核心框架是“ b −=1, b +=1; loop b −=1, b +=2;”, 这一部分可以 {b } -计算出正确的 F 1 (B). 而最终需要得
′
′
到 A = A·4 1−B , 因此在第 1 处 b −=1 无须修改 a, 后续循环中每次令 a 7→ a/4 即可. 为了成功地执行对 a 的变换, 可
′
以借助初始格局给出的三元组 τ s , 因此 P 1 中除核心框架外的部分本质上是在利用三元组保证程序的任意 {c } -执行
(也是一个{b'}-执行) 中对 a 的变换达到了预期要求.
( ( ) ) { } { }
′ ′ ′ ′ , ′ , 则我们可以
若已经得到了 Ampl k = P k ,X k , a,b ,c ,(a,b k ,c k ),Z k , 定义 X k+1 = X k ∪ b k+1 ,c k+1 Z k+1 = Z k ∪ c k+1
k
k
(
(
得到 F k + 1 (n)-放大器 Ampl k+1 = P k+1 ,X k+1 , a,b ′ k+1 ,c ′ k+1 ) ,(a,b k ,c k ),Z k+1 , 其中, P k+1 如图 19 所示. 构造框架完全与图 11
)
( )
τ s = a,b ′ ,c ′ ,A,B,X k+1 确保程序中的操作 loop b k −=1, b +=1; 执行成功,
′
一致, 在细节上则和 P 1 相似, 即使用 k+1 k+1 k
便于利用 P k 进行下一次放大.
最终, 我们构造出了一族 F d (n)-放大器 {Ampl d } d∈N . 易知 |X d | = 2d +4 |Z d | = d, 由于 b 只会减少, 因此在后续使
,
′
d