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

现在终止检查人员应该抱怨。