为何Dafny中表达式求值的Decreases Clause无法证明终止性？

问题根源 #

这段代码的终止性无法被Dafny自动确立，核心原因是跨函数递归的递减关系无法被自动追踪：

• eval函数处理Add(e1,e2)时调用evalAdd(e1,e2)，而evalAdd内部又调用eval(e1)和eval(e2)，形成了跨函数的递归链。
• 虽然e1、e2的结构确实比Add(e1,e2)更小，但Dafny的终止检查器默认无法关联evalAdd中的eval调用与最初eval调用evalAdd时的原始表达式之间的递减关系——它看不到这个递归链的每一步都在处理更小的表达式。

无需内联或高度函数的解决方案 #

不用把代码揉成一个大函数，也不用额外定义height度量，只需明确告诉Dafny跨函数递归的递减逻辑即可，这里有两种简洁的实现方式：

方式1：传递父表达式作为上下文 #

给evalAdd增加一个参数，代表调用它的父表达式，然后用父表达式作为decreases的依据：

function eval(e: Expr) : nat
decreases e {
    match e
        case Const(v) => v
        case Add(e1,e2) => evalAdd(e1,e2, e)
}

function evalAdd(e1: Expr, e2: Expr, parent: Expr) : nat
decreases parent {
    var n1 := eval(e1);
    var n2 := eval(e2);
    n1 + n2
}

此时Dafny能明确看到：evalAdd的parent是eval中的原始表达式e，而eval(e1)、eval(e2)的参数都比parent小，递归链的递减性清晰可证。

方式2：显式指定跨函数的递减顺序 #

如果不想增加参数，也可以给eval调用evalAdd时补充递减提示，明确关联两个函数的递归逻辑：

function eval(e: Expr) : nat
decreases e {
    match e
        case Const(v) => v
        case Add(e1,e2) => evalAdd(e1,e2) {:decreases e}
}

function evalAdd(e1: Expr, e2: Expr) : nat
decreases e1, e2 {
    var n1 := eval(e1);
    var n2 := eval(e2);
    n1 + n2
}

通过{:decreases e}标注，明确告诉Dafny调用evalAdd时的递减依据是eval的当前参数e，让检查器能关联后续递归调用的大小关系。

为什么内联或高度函数能解决问题 #

• 内联方案：所有递归调用都收敛到eval内部，Dafny可以直接看到eval(e1)、eval(e2)的参数比Add(e1,e2)小，无需额外提示就能证明终止性。
• 高度函数方案：height(Expr)定义了表达式的结构深度，height(e1)、height(e2)必然小于height(Add(e1,e2))，用height(e)作为decreases的度量后，不管递归跨多少函数，只要度量值严格递减，Dafny就能认可终止性。

内容的提问来源于stack exchange，提问作者redjamjar