如何在Dafny中定义相互递归函数的递减

Question

在"Dafny参考手册草案"；4.0.2它描述了为相互递归函数定义递减子句，但其中两个函数中递减的变量都是nat类型。我试过做同样的事情，但没有成功。一个区别是变量的类型不同。

datatype Trie = Trie(letters : map<char,Trie>, word : bool)
function  size(t:Trie) :(r:nat)
decreases t 
{ 
1 + sum_setT(t.letters.Values)
}
function  sum_setT(xs: set<Trie>) : (z:nat) 
decreases xs
{
var working := xs; //Needed!
if (|working| == 0) then 0
else  (
var x:Trie  :| x in working;
var sofar:nat := sum_setT(working-{x});
sofar + size(x)
)   
}

任何关于如何定义减少条款的想法都将不胜感激。

Answer 1

如果两个函数(可能是同一个函数(递归地相互调用，则需要显示每个调用以减少decreases函数给出的终止度量。更准确地说，如果在进入函数F时，F的decreases子句的计算结果为X，并且当F在G的decreases子句的计算值为Y时调用函数G时，则X必须显示为超过Y。

"；超过"；relation是一个内置的有充分根据的顺序，但您可以控制产生值X和Y的decreases子句。在您的示例中，定义这些的最简单方法是使用字典元组。在"；外部"；函数，size，使用t。在"；内部"；函数sum_setT将t, xs用于相同的t。为了解决这个问题，您还需要将t作为参数添加到sum_setT中。

在从size到sum_setT的调用中，X和Y是t和t, t.letters.Values，后者较小，因为Dafny中内置的有充分根据的顺序认为较短的decreases元组较大。

在sum_setT的递归调用中，X和Y具有相同的第一分量(t(，并且集合在Y中严格较小。

在从sum_setT返回size的调用中，值x在结构上包含在t中，因此t根据需要超过x。为了让验证器知道这个事实(也就是说，为了让它知道参数xs与t有某种关系(，您需要向sum_setT添加一个前提条件。

所以，最后的程序是

datatype Trie = Trie(letters: map<char, Trie>, word: bool)
function size(t: Trie): nat
decreases t
{ 
1 + sum_setT(t, t.letters.Values)
}
function sum_setT(t: Trie, xs: set<Trie>): nat
requires xs <= t.letters.Values
decreases t, xs
{
if |xs| == 0 then
0
else
var x :| x in xs;
var sofar := sum_setT(t, xs - {x});
sofar + size(x)
}