Странное поведение функции 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

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