idris - 将输入参数限制为函数

Question

假设我想将斐波那契函数定义为以下函数:

fibo : Int -> Int
fibo 1 = 1
fibo 2 = 2
fibo n = fibo (n-1) + fibo (n-2)

这个函数显然不是完全的，因为它对于小于 1 的整数是未定义的，所以我需要以某种方式限制输入参数..

我试过定义一个新的数据类型 MyInt .沿线的东西:

-- bottom is the lower limit
data MyInt : (bottom: Int) -> (n: Int) -> Type
  where
    ...

fibo : MyInt 1 n -> Int
...

但是我很快就迷路了。

例如，如何将输入参数限制为我的 fibo函数是 1 或以上的整数值？

Answer 1

idris 无法识别 fibo 实际上有两个原因。作为总的功能。首先，正如您所指出的，它不是为小于 1 的整数定义的，但其次，它递归地调用自己。尽管 Idris 能够识别递归函数的整体，但它通常只能在可以证明递归调用的参数比原始参数“更小”(即更接近基本情况*)时才能这样做(例如，如果函数接收一个列表作为参数，它可以用列表的尾部调用自己而不必牺牲整体性，因为尾部是原始列表的子结构，因此更接近 Nil )。像 (n-1) 这样的表达式的问题和 (n-2) , 当它们是 Int 类型时, 是虽然它们在数值上小于 n，但它们在结构上并不小，因为 Int没有归纳定义，因此没有基本情况。因此，总体检查器无法满足自己递归总是最终达到基本情况(即使对我们来说似乎很明显)，因此它不会考虑 fibo是总的。

首先，让我们解决递归问题。而不是 Int ，我们可以使用归纳定义的数据类型，例如 Nat :

data Nat =
  Z | S Nat

(一个自然数要么是零，要么是另一个自然数的后继者。)

这允许我们重写 fibo作为:

fibo : Nat -> Int
fibo (S Z)     = 1
fibo (S (S Z)) = 2
fibo (S (S n)) = fibo (S n) + fibo n

(注意在递归情况下，我们不是通过显式计算 (n-1) 和 (n-2)，而是通过参数的模式匹配来生成它们，从而向 Idris 证明它们在结构上更小。)
fibo的新定义尽管如此，仍然不是全部，因为它缺少 Z 的案例。 (即零)。如果我们不想提供这种情况，那么我们需要给 idris 一些保证，它不会被允许发生。我们可以做到这一点的一种方法是要求证明 fibo 的论点。大于或等于一(或等效地，一小于或等于参数):

fibo : (n : Nat) -> LTE 1 n -> Int
fibo Z LTEZero impossible
fibo Z (LTESucc _) impossible
fibo (S Z) _ = 1
fibo (S (S Z)) _ = 2
fibo (S (S (S n))) _ = fibo (S (S n)) (LTESucc LTEZero) + fibo (S n) (LTESucc LTEZero)

LTE 1 n是其值证明 1 ≤ n(在自然数内)的类型。 LTEZero表示零≤任意自然数的公理，且 LTESucc表示如果 n ≤ m，则(n 的后继)≤(m 的后继)的规则。 impossible关键字表示给定的情况不能发生。在上面的定义中， fibo 的第一个参数是不可能的。为零，因为无法证明 1 ≤ 0。对于任何其他自然数 n，我们可以使用 (LTESucc LTEZero) 证明 1 ≤ n .

现在终于 fibo是全部，但必须为其提供一个显式证明证明其参数大于或等于 1 是相当麻烦的。幸运的是，我们可以将证明参数标记为自动隐式:

fibo : (n : Nat) -> {auto p : LTE 1 n} -> Int
fibo Z {p = LTEZero} impossible
fibo Z {p = (LTESucc _)} impossible
fibo (S Z) = 1
fibo (S (S Z)) = 2
fibo (S (S (S n))) = fibo (S (S n)) + fibo (S n)

Idris 现在会在可能的情况下自动找到 1 ≤ n 的证明，否则我们仍然需要自己提供证明。

* 可能有一些与 codata 相关的微妙之处，我在这里掩盖了而没有意识到，但这是广泛的原则。