在Dafny纯函数式代码中使用:|实现集合递归的方法

阿华AIGC实验室

2026-5-27

在Dafny纯函数式代码中对集合执行递归操作的方法

嘿，这个问题问到了Dafny纯函数式编程里的关键细节——确实，命令式里随便用:|选元素递归没问题，但纯函数要求引用透明（相同输入必须返回相同输出），无约束的:|是不确定的，没法直接用。下面给你几种靠谱的解决思路：

1. 给`:|`加确定性约束，选唯一确定的元素

最直接的办法是给选择操作符加上足够的谓词，让它每次都选同一个元素。比如如果集合元素是可比较的（比如int、string这种），可以选集合里的最小/最大元素：

function Sum(S: set<int>): int
  decreases |S|  // Dafny需要递归终止证明，这里用集合大小递减
{
  if S == {} then 0
  else
    // 明确选取集合中的最小元素，保证每次选的都一样
    var s :| s in S && s == min(S);
    s + Sum(S - {s})
}

这里的min(S)是Dafny内置的集合最小值函数，通过这个约束，:|的选取结果完全确定，函数也就满足纯函数的要求了。

如果是自定义类型，只要你能定义一个唯一标识元素的规则，比如自定义类型的某个字段是唯一的，也可以用同样的思路：

datatype Product = Product(sku: string, price: int)

function TotalPrice(S: set<Product>): int
  decreases |S|
{
  if S == {} then 0
  else
    // 选取sku字典序最小的商品，保证确定性
    var p :| p in S && p.sku == min({x.sku | x in S});
    p.price + TotalPrice(S - {p})
}

2. 先把集合转成有序序列再递归

集合是无序的，但序列是有序的，你可以先把集合转换成一个确定顺序的序列，然后对序列做递归操作——因为序列的第一个元素是明确的，递归过程自然就是确定的：

// 把集合转成按元素从小到大排序的序列
function SetToSortedSeq(S: set<int>): seq<int>
  ensures forall x :: x in S <==> x in SetToSortedSeq(S)
  decreases |S|
{
  if S == {} then []
  else
    var s :| s in S && s == min(S);
    [s] + SetToSortedSeq(S - {s})
}

// 借助序列实现集合的求和递归
function SumSet(S: set<int>): int
{
  SumSeq(SetToSortedSeq(S))
}

// 对序列的递归求和（纯函数，完全确定）
function SumSeq(s: seq<int>): int
  decreases |s|
{
  if s == [] then 0
  else s[0] + SumSeq(s[1..])
}

这种方法的好处是把集合的无序问题转化为序列的有序问题，递归逻辑更直观，也更容易让Dafny验证终止性。