约束输入参数的函数

可以说，我想定义斐波那契函数如下功能：约束输入参数的函数

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或更大的整数值？

来源

2016-06-30 Michelrandahl

Idris实际上不会将fibo函数视为总共有两个原因。首先，正如你所指出的，它没有定义小于1的整数，但其次，它自己递归地调用它自己。虽然Idris能够识别整个递归函数，但通常只有在能够显示递归调用的参数比原始参数“更小”（即更接近基本情况*）时才可以这样做（例如，如果一个函数收到一个列表作为参数，它可以使用列表的尾部调用它自己而不必牺牲整体性，因为尾部是原始列表的子结构，因此更接近于Nil）。与像(n-1)(n-2)和，表达的问题，当它们是Int型的是，虽然它们是数值小于n，它们不是结构小一些，因为Int不感应地定义，因此没有基的情况。因此总体检查者无法确定递归总是最终会达到基本情况（即使它对我们来说可能很明显），所以它不会认为总数是fibo。

首先，我们来解决递归问题。代替Int，我们可以使用一个电感定义的数据类型如Nat：

data Nat = 
    Z | S Nat

（A自然数是零，或另一个自然数的继任者。）

这使我们能够改写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)明确如何在递归的情况下，我们生产他们通过图案参数匹配，从而DEM onstrating到伊德里斯它们在结构上是较小的。）

这种新的fibo定义仍然不完全总，但是，因为它缺乏对Z的情况下（即零）。如果我们不想提供这样的情况，那么我们需要给伊德里斯一些保证它不会被允许发生。我们能做到这一点的方法之一是需要证明的参数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≤米，然后（的Ñ后继）≤（的米后继）。关键字impossible表示不会发生特定情况。在上面的定义中，fibo的第一个参数不可能是零，因为没有办法证明1≤0。对于任何其他自然数n，我们可以证明1≤n使用(LTESucc LTEZero)。

现在终于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)

伊德里斯现在会自动找到1≤n的证明，否则我们仍然会被要求自己提供一个。

_{*有可能是一些CODATA相关的细微之处，我在这里粉饰没有意识到，但是这是大原则。}

来源

2016-07-02 13:27:20 j11c

约束输入参数的函数

回答

相关问题