信用分配终止检测

每份未完成责任都必须带走一点信用。根若还缺哪怕极小一份，可能是一个活动工作者还拿着，也可能是基本任务在途中，还可能是归还信用的控制消息没到。

不能让发送者把全部信用随任务发走，自己却仍保持active。那会出现仍可继续工作的零信用节点，根收齐1不再能排除它。只分出严格小于现有信用的一部分，让发送者与新任务各自有正数见证。

这与按任务数量计数不同。一次任务可以派生任意多次有限分流，每次把现有信用再分开；只要使用精确分数并且总量不变，就不必预先知道会产生多少任务。

分流与归还分别记账 ​

令r先给p发送1/2信用，再给q发送1/4，自己保留1/4。p收到后再分出1/4给q。按表中顺序交付：

假定r派发后已经被动。倒数第二行基本计算已经真正终止，但检测器还不能宣布，因为有1/2信用正在RETURN中。最后一行才得到根的本地完成证书。允许晚宣布是正确的；提前宣布则可能丢掉仍在途的基本任务。

守恒式必须包含控制消息 ​

令B为在途基本消息，R为在途RETURN消息。核心不变量公理库不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。是

每次发送把信用从节点转入消息，每次接收把它从消息转入节点，因此保持等式。归还也遵循同一规则：若只计算基本信道，非根发RETURN时总量会凭空减少；若发RETURN后不清本地信用，总量则被重复计入。

根被动且w[r]=1时，其他各项都只能为0。活动非根必须有正信用，在途基本消息也必须有正信用，所以二者都不存在。这给出安全性。基本计算若最终终止，每个非根最终把全部信用归还；有限多条归还消息最终送达，根便收齐1，给出最终检测。

精确性是一项算法条件 ​

假设某个活动节点仍持有 $\epsilon =2^{-54}$，根实际持有 $1-\epsilon$。若根用常见双精度浮点存储，后者可能舍入成1。用浮点相等宣布完成，会把尚未归还的正信用抹掉。把“差小于某容差”当成完成条件也有同样问题。

另一种失效是反复减半后下溢为0，导致基本消息或活动节点不再持有正信用。解决需要精确数值表示，或者另行证明带补充信用握手的协议；不能由节点自行补一份信用，却不先让根更新其总量账本。

若消息可能重复，同一RETURN被算两次也会破坏守恒。消息身份、去重及信用入账必须配合，不能仅因有效载荷恰好是同一个分数就猜测它是否重传。

检测控制层在每次发送/接收做常数次有理数加减与分割；但“常数次数”不是常数位复杂度。若总共M次发送都采用减半，精确二进制分母的指数可达到O(M)，普通分子表示也可能需要O(M)位。

单根模型中，每个非根的active区间至少由一条基本消息启动，故归还消息数至多M；若RETURN要经多跳到根，还应乘上相应路由长度。暂停或崩溃节点若一直扣着信用，检测不能结束；无故障假设在这里直接支撑活性。

Dijkstra–Scholten公理库Dijkstra–Scholten 终止检测Dijkstra–Scholten algorithm · Diffusing computation termination为单源扩散计算维护未清回执与动态父树，使根的被动和零欠账同时排除活动后代与在途任务。记录责任的父链和回执数量，信用算法记录可加的份额。二者都要覆盖在途任务，差别在于保留什么证明信息。信用分配适合递归分流清楚的工作池，代价是数值表示和信用生命周期必须受到严格管理。