为什么这个FStar函数没有被接受？

Question

我想了解为什么这个函数不被接受为终止函数：

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拒绝它并发送以下消息：

(错误)无法证明此递归调用的终止:求解器找到了一个(部分)反例.

这可能与我在FStar函数奇异行为下相关问题中的绑定问题不同

FStar可以显示反例吗？

Answer 1

正如在本教程中所解释的，在默认情况下，F*使用一种递减度量，将所有参数按字典顺序排列。

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

这不适用于证明此函数终止，因为很明显，ni + nw并不比ni小。

如果有一个正确的减少措施和nw为正的前提条件，这确实可以通过：

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

不完全是最初的例子，但是对于nw=0来说，这个例子肯定是永远循环的！无论如何，即使在这个修复之后，这段代码也没有什么意义，而且使用这样的循环对于函数式编程来说也不是惯用的。

最后，F*无法生成反例，最近修复了此错误消息：https://github.com/FStarLang/FStar/pull/2075

Answer 2

此函数并不终止于所有输入。比如ni < ni_max和nw=0。不幸的是，F*没有找到像这样的具体反例。

您可以证明函数的一个变体正在终止，但是您必须明确地告诉F*什么是递减的。我们用的是有充分根据的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)