Странное поведение функции 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 в первой ветви шаблона является связывателем fre sh и не имеет отношения к параметру 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

, и теперь программа проверки завершения должна пожаловаться.