0

我想了解为什么不接受此功能作为终止功能：

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 可以举出反例吗？

4

2 回答 2

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)
于 2020-07-06T17:10:21.560 回答
2

如教程中所述，默认情况下，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

于 2020-07-06T17:30:07.377 回答