咨询：FStar函数fnc被判定为终止的异常行为原因

嘿，这个问题的核心其实是你不小心踩了函数式语言模式匹配的一个常见坑！让我们把事情理清楚：

先看你的函数代码：

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

你原本想表达的是“当ni等于参数ni_max时返回false，否则递归”，但这里的模式匹配写法完全不符合你的预期：

• 在OCaml、Coq这类函数式语言中，模式里的标识符是用来绑定新变量的，不是和外部同名参数做相等比较。
• 你的| ni_max -> false分支，其实是把当前ni的值绑定到一个局部的新变量ni_max（和外部参数同名，但完全是两个独立的变量），然后直接返回false。这意味着不管ni是什么值，第一次进入match都会匹配这个分支，函数直接终止，根本不会触发递归！

这就是为什么你调用fnc 0 0 1会直接返回false——递归调用根本没机会执行。

如果你想实现“当ni等于ni_max时返回false，否则递归”，需要用**守卫（guard）**来做相等判断，比如在OCaml中：

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

这里的when n = ni_max就是守卫条件，只有当n（即ni）等于参数ni_max时，才会进入第一个分支。

假设你修正了模式匹配，那当nw=0时，每次递归的ni都是0+ni=ni，也就是永远不会等于ni_max（除非初始ni就等于ni_max），这时候函数才会无限递归。但因为你原来的写法根本没走到递归那一步，所以函数自然会终止。

内容的提问来源于stack exchange，提问作者Attila Karoly