Feature request: better termination metrics for functions that recurse on maps

[wilcoxjay]

Consider the following program:

datatype D = D(m: map<int, D>)

function Foo(d: D): D
{
  D(Bar(d.m))  // Error: cannot prove termination; try supplying a decreases clause
}

function Bar(m: map<int, D>): map<int, D>
{
  map i | i in m :: Foo(m[i])  // Error: cannot prove termination; try supplying a decreases clause
}

The program declares a datatype D that is sort of a strange arbitrary-arity tree, where the children of each node are stored in a (partial, possibly empty) map indexed by integers. Functions Foo and Bar implement a trivial recursive traversal over these trees, which just returns a fresh copy of the tree, so to speak.

However, Dafny reports the errors shown in comments, which are related to termination. Even supplying the obvious (and intuitively correct) decreases clauses to Foo and Bar does not help the situation.

There seem to be two issues going on here. The first is that the call made by Bar to Foo does not satisfy Dafny's termination check, seemingly because Dafny does not allow recursion "through maps", even though it does allow recursion through sequences. The second issue is that the call from Foo to Bar also fails the termination check for no apparent reason, d.m is clearly smaller than d.

What's going on here? Is there a way to write any nontrivial recursive function over a type like D?

[cpitclaudel]

Well, three years later, here's an answer in three parts:

First, Dafny Dafny does not have a general termination metric (a "Rank") for maps, unlike sequences (Seq#Rank) and datatypes. Instead, termination for maps is special-cased to comparing the ranges:

https://github.com/dafny-lang/dafny/blob/e3494683da6c5a161363795853e9b68b10d9ed47/Source/Dafny/Verifier/Translator.cs#L9200-L9206

This means that you can easily verify this function:

  function CountMapItems<K, V>(m: map<K, V>) : int {
    if |m| == 0 then 0
    else var k :| k in m; 1 + CountMapItems(m - {k})
  }

… but not so easily this one:

  datatype D = D(m: map<int, D>)
  function method IncrementKeys(m: map<int, D>) : map<int, D> {
    map i | i in m :: i+1 := D(IncrementKeys(m[i].m))
  }

Indeed, unlike sequences, maps don't assert that their contents are "smaller" than them.

Second, datatypes. When you define a datatype, like D above, you get a set of axioms that compare it with its own children of the same type. Hence, the following verifies:

  function method IncrementKeys'(d: D) : D {
    D(map i | i in d.m :: i+1 := IncrementKeys'(d.m[i]))
  }

It would be nice if both of these functions worked, and for this I suspect we would need to generate a separate Map#Rank axiomatization.

This heuristic is convenient but far from complete: it allows a function that takes an argument d:D to call itself on descendants of d of type D, but not to call (mutually) recursive functions on containers (like seqs or maps within d).

Finally, your question. Hopefully from the two points above it's clear what's happening in both cases. The fix is to force the recursion to go through a D:

  datatype D = D(m: map<int, D>)

  function Foo(d: D): D
    decreases d, 1
  {
    D(Bar(d.m))
  }

  function Bar(m: map<int, D>, d: D := D(m)): map<int, D>
    decreases d, 0
    requires forall i | i in m :: m[i] < d
  {
    map i | i in m :: Foo(m[i])
  }

So, TL;DR:

What's going on here?

Incomplete termination metrics for maps and datatypes.

Is there a way to write any nontrivial recursive function over a type like D?

Yes, but it's not as nice as you'd hope.

[cpitclaudel]

For future implementers, here are additional examples that show this issue and contrast it with sequences:

We accept this:

  datatype D = D(m: map<int, D>)
  function method IncrementKeys(m: map<int, D>) : map<int, D> {
    map i | i in m :: i+1 := D(IncrementKeys(m[i].m))
  }

But reject this:

  datatype D = D(i: int, s: seq<D>)
  function method Increment(s: seq<D>) : seq<D> {
    seq(|s|, i requires 0 <= i < |s| => D(s[i].i + 1, Increment(s[i].s)))
  }

This is because we do not have a general map rank, so Dafny doesn't know that m[i] is smaller than m, and it doesn't know that m[i].m is smaller than m[i]. It knows both of these facts for sequences.

Similarly, we reject the following two functions (like in the OP in this thread):

module M0' {
  datatype D = D(m: map<int, D>)

  function method IncrementM(m: map<int, D>) : map<int, D> {
    map i | i in m :: i+1 := IncrementD(m[i])
  }

  function method IncrementD(d: D) : D {
    D(IncrementM(d.m))
  }
}

In contrast, we accept both of these:

module M0 {
  datatype D = D(i: int, s: seq<D>)

  function method IncrementS(s: seq<D>) : seq<D> {
    seq(|s|, i requires 0 <= i < |s| => IncrementD(s[i]))
  }

  function method IncrementD(d: D) : D {
    D(d.i + 1, IncrementS(d.s))
  }
}

Here, Dafny knows that d.s is smaller than d, while it doesn't know that d.m is smaller than d