How can I define a decreases for mutually recursive functions in Dafny?

Question

In the "Draft Dafny Reference Manual" 4.0.2 it describes defining decreases clauses for mutually recursive functions but where the variables decreasing in both functions are of the type nat. I have tried to do the same thing but it has not worked. One difference is that the variables are not of the same type.

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)
    )   
  }

Any idea how to define the decreases clause much appreciated.

Answer 1

If two functions (possibly the same function) call each other recursively, then each call needs to be shown to decrease the termination metric given by the decreases functions. More precisely, if on entry to a function F, the decreases clause of F evaluates to X, and when F calls function G at a time when G's decreases clause evaluates to Y, then X must be shown to exceed Y.

The "exceeds" relation is a built-in well-founded order, but you have control over the decreases clauses that give rise to the values X and Y. In your example, the easiest way to define these is to use lexicographic tuples. In the "outer" function, size, use t. In the "inner" function, sum_setT, use t, xs for the same t. To get this to work out, you'll need to add t as a parameter to sum_setT as well.

In the call from size to sum_setT, X and Y are t and t, t.letters.Values, which is smaller because the built-in well-founded order in Dafny considers shorter decreases tuples to be larger.

In the recursive call of sum_setT, X and Y have the same first component (t) and the set is strictly smaller in Y.

In the call from sum_setT back to size, the value x is structurally included in t, so t exceeds x as required. For the verifier to know this fact (that is, for it to know that parameter xs has some relation to t), you'll need to add a precondition to sum_setT.

So, the final program is

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)
}