fstar - FStar 函数异常行为

Question

以下简单函数被接受为终止函数似乎是不正确的：

val fnc : (nw: nat) -> (ni: nat) -> (ni_max: nat) -> bool
let rec fnc nw ni ni_max =
  match ni with 
  | ni_max -> false
  | _      -> fnc nw (nw + ni) ni_max

令人惊讶的是，该函数确实在评估它时终止，例如，通过fnc 0 0 1和返回false。我错过了什么？

Answer 1

模式的ni_max第一个分支中的 是一个新的活页夹，与函数的参数无关ni_max。您的代码相当于：

let rec fnc nw ni ni_max =
  match ni with 
  | _ -> false
  | _      -> fnc nw (nw + ni) ni_max

这是一个始终返回 false 的函数。

你可能打算写

let rec fnc nw ni ni_max =
  if ni = ni_max then false
  else fnc nw (nw + ni) ni_max

现在终止检查器应该抱怨。