Question

How do I make Dafny termination checking happy with mutual recursion, like the following example:

datatype T = Y | N | B(T,T)

function f(x : T) : bool {
    match x {
        case Y => true
        case N => false
        case B(x,y) => g(x,y)
    }
}

function g(x : T, y : T) : bool {
    f(x) && f(y)
}

If g is inlined there is no problem. What should I do?

Answer

Termination of recursion is proved using a decreases clause. For the single function Dafny can successfully guess a decreases metric. But for this mutual recursion case, the user must supply on.

The termination metric for a recursive datatype (like T here) is the height of the tree denoted by the argument x, in this case. So there is definitely a decrease in the metric from the call of f to the call of g, but there is not when g calls f. One solution to this situation is the following:

datatype T = Y | N | B(T,T)

function f(x : T) : bool 
  decreases x, 1
{
    match x {
        case Y => true
        case N => false
        case B(x,y) => g(x,y)
    }
}

function g(x : T, y : T) : bool 
  decreases B(x,y), 0
{
    f(x) && f(y)
}

Here when f calls g, the metric goes from x, 1 to B(x.x, x.y), 0. Because x is the same as B(x.x, x.y), the lexicographic ordering looks at the next component, which does decrease from 1 to 0. Then in each case that g calls f, the metric goes from B(x,y), 0 to x,1 or y,1, which decreases on the first component.

Another solution, which is a pattern applicable in other circumstances as well, is to use a ghost parameter as follows:

datatype T = Y | N | B(T,T)

function f(x : T) : bool
  decreases x, 1
{
  match x {
    case Y => true
    case N => false
    case B(x',y') => g(x,x',y')
  }
}

function g(ghost parent: T, x : T, y : T) : bool
  decreases parent, 0
  requires x < parent && y < parent
{
  f(x) && f(y)
}

More on the topic of termination metrics can be found here.