### 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?

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.