約束輸入參數的函數

可以說，我想定義斐波那契函數如下功能：約束輸入參數的函數

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

約束輸入參數的函數

回答

相關問題