Idris总体检查

Question

我正在使用Idris2编译以下简单程序。

import Data.Fin

%default total

negate : {k:_} -> Fin k -> Fin k
subt : {k:_} -> Fin k -> Fin k -> Fin k
add : {k:_} -> Fin k -> Fin k -> Fin k

mult : {k:_} -> Fin k -> Fin k -> Fin k
mult FZ b = FZ
mult (FS a) b = add b $ mult (weaken a) b

但是，编译器产生一个错误：

Error: mult is not total, possibly not terminating due to recursive
path Main.mult -> Main.mult -> Main.mult

对输入a的递归调用不是比(FS a)小吗？为什么整个检查失败了？

谢谢!

Answer 1

我不知道为什么编译器没有意识到weaken a比FS a小，尽管我怀疑问题是weaken。

您可以通过断言weaken a比FS a小来绕过它。

module Misc

import Data.Fin

%default total

add : Fin k -> Fin k -> Fin k
add a b = ?add_rhs

mult : Fin k -> Fin k -> Fin k
mult FZ _ = FZ
mult a@(FS a') b = add b $ mult (assert_smaller a (weaken a')) b

请注意，在通常对整数进行加法和乘法的定义下，结果可能大于k。我假设您的add实现会处理这个问题。