Why isn't this FStar function accepted?

Question

I'd like to understand why this function is not accepted as a terminating one:

val while_items: ni: nat -> ni_max: nat -> nw: nat -> bool
let rec while_items ni ni_max nw = 
  (if   ni < ni_max 
   then while_items (ni + nw) ni_max nw 
   else true)

FStar rejects it and sends the following message:

(Error) Could not prove termination of this recursive call: The solver found a (partial) counterexample...

It's likely not the same binding issue here as the one in my related question under FStar function strange behavior

Can FStar show the counter example?

Answer 1

As explained in the tutorial, by default F* uses a decreases measure that puts all arguments in lexicographic order

val while_items: ni: nat -> ni_max: nat -> nw: nat -> Tot bool (decreases %[ni,ni_max;nw])

which doesn't work for proving this function terminating, since clearly ni + nw is not smaller than ni.

With a correct decreases measure and a precondition that nw is positive this does go through:

val while_items: ni: nat -> ni_max: nat -> nw: pos ->
  Tot bool (decreases (if ni < ni_max then ni_max-ni else 0))

Not exactly the original example, but that one definitely loops forever for nw=0! And anyway, even after this fix this code makes little sense as is and using such loops is not idiomatic for functional programming.

Finally, F* can't produce counterexamples, and this error message has recently been fixed: https://github.com/FStarLang/FStar/pull/2075

Answer 2

This function does not terminate on all inputs. Consider ni < ni_max and nw=0. Unfortunately, F* does not find concrete counterexamples like this.

You can prove a variant of your function terminating, but you have to tell F* explicitly what's decreasing. Here we're using the well-founded ordering on nat.

let as_nat (x:int) : nat = if x < 0 then 0 else x
val while_items: ni: nat -> ni_max: nat -> nw: nat{ni < ni_max ==> nw > 0} -> Tot bool
                 (decreases (as_nat (ni_max - ni)))
let rec while_items ni ni_max nw =
  (if   ni < ni_max
   then while_items (ni + nw) ni_max nw
   else true)