2017-12-24 13 views
2

私はIdrisを学んでおり、私はVectタイプのQuicksortを実装しようと考えていました。Idrisのクイックソート

しかし、ピボット要素とベクトルを指定すると、≤ピボット要素とピボット要素を持つ2つのベクトルを分割するユーティリティメソッドでは苦労しています。

splitListOn : Ord e => (pivot : e) -> List e -> (List e, List e) 
splitListOn pivot [] = ([], []) 
splitListOn pivot (x :: xs) = let (ys, zs) = splitListOn pivot xs in 
           if x <= pivot then (x :: ys, zs) 
              else (ys, x :: zs) 

*Test> splitListOn 3 [1..10] 
([1, 2, 3], [4, 5, 6, 7, 8, 9, 10]) : (List Integer, List Integer) 

しかしVECTのために私は2つの長さの合計がVectsが入力VECTの長さに等しい返されたという事実を表現する必要があります。

これはリストのための簡単です。

明らかに従属ペアを返す必要があります。ピボット≤要素の数は、最初の値のための良い候補だが、私の最初の試み:

splitVectOn : Ord e => e -> Vect n e -> (k ** (Vect k e, Vect (n - k) e)) 

は、k個の≤nのかどうか知らない(当然のように)文句を言う:

When checking type of Main.splitVectOn: 
When checking argument smaller to function Prelude.Nat.-: 
     Can't find a value of type 
       LTE k n 

そのようなものLTE k nをタイプシグネチャを再確認するために型シグネチャに追加することはできますが、再帰的にどのようにして述語を渡す戻り値kを作成するのかわかりません。

私はここで、n = K = 0、いない基本ケースのために、意味:

splitVectOn : Ord e => LTE k n => 
       e -> Vect n e -> (k ** (Vect k e, Vect (n - k) e)) 
splitVectOn _ [] = (_ ** ([], [])) 

エラータイプ署名に問題があるかもしれないことを示唆している​​とk、両方に言及:

splitVectOn : Ord e => e -> Vect n e -> 
       (k : Fin (S n) ** (Vect (finToNat k) e, Vect (??? (n - k)) e)) 
012:

When checking right hand side of splitVectOn with expected type 
     (k1 : Nat ** (Vect k e, Vect (0 - k) e)) 

When checking argument a to constructor Builtins.MkPair: 
     Type mismatch between 
       Vect 0 e (Type of []) 
     and 
       Vect k e (Expected type) 

     Specifically: 
       Type mismatch between 
         0 
       and 
         k 

私も不変を表現するためにFinを使用するのではと思いました

その後私は、減算を実行する方法がわからない(フィン(S n)が常にあるので、可能なはず≤n)はあなたがそうのような出力タイプに必要な証拠を追加することができます

答えて

2

ここで
(k ** pf : LTE k n ** (Vect k e, Vect (n - k) e)) 

私たちは、この関数を定義する方法です。

-- auxiliary lemma 
total 
minusSuccLte : n `LTE` m -> S (m `minus` n) = (S m) `minus` n 
minusSuccLte {m} LTEZero = cong $ minusZeroRight m 
minusSuccLte (LTESucc pf) = minusSuccLte pf 

total 
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
         (k ** pf : LTE k n ** (Vect k e, Vect (n - k) e)) 
splitVectOn pivot [] = (0 ** LTEZero ** ([], [])) 
splitVectOn pivot (x :: xs) = 
    let (k ** lte ** (ys, zs)) = splitVectOn pivot xs in 
    if x <= pivot then (S k ** LTESucc lte ** (x :: ys, zs)) 
    else 
    let xzs = replace {P = \n => Vect n e} (minusSuccLte lte) (x :: zs) in 
    (k ** lteSuccRight lte ** (ys, xzs)) 

は、同じ問題に対する別のアプローチは、splitVectOn fucntionに次の仕様を与えることです:

total 
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
       (k1 : Nat ** k2 : Nat ** (k1 + k2 = n, Vect k1 e, Vect k2 e)) 

すなわち、出力ベクトルの長さを定量化し、その長さの合計が入力ベクトルの長さに等しくなければならないという条件を追加します。このk1 + k2 = nの条件を省略することもできますが、実装を大幅に簡素化できます。

total 
splitVectOn : Ord e => (pivot : e) -> Vect n e -> 
       (k1 : Nat ** k2 : Nat ** (k1 + k2 = n, Vect k1 e, Vect k2 e)) 
splitVectOn pivot [] = (0 ** 0 ** (Refl, [], [])) 
splitVectOn pivot (x :: xs) = 
    let (k1 ** k2 ** (eq, ys, zs)) = splitVectOn pivot xs in 
    if x <= pivot then (S k1 ** k2 ** (cong eq, x :: ys, zs)) 
    else let eq1 = sym $ plusSuccRightSucc k1 k2 in 
     let eq2 = cong {f = S} eq in 
     (k1 ** S k2 ** (trans eq1 eq2, ys, x :: zs)) 
+0

ワウ:ここ

は変更仕様と機能の実装です。ありがとう!それは理にかなっているが、聖なる牛。それは私のための本に戻る – Tobia

+1

残念なことに、私はこのことについて哲学的な疑問を抱いていると思います。どうしてタイプシステムに何度も何度も基本的な算術を何度も証明する必要がありますか?私は、証明できない算定命題が存在することを知っています(ゲデルの不完全性定理?)が、これはそれほどです!ほとんどの場合、それはS(n + k)=(S n)+ kのような結合性の明白な応用である。それだけでそれを理解することはできませんか? – Tobia

+1

人々はこの問題を克服するためのツールを開発しようとします。例えば。 Coqは、主に戦術ベースの定理証明者であり、「オメガ」(プレスバーガー算術の場合)や「リング/フィールド」(リングとフィールドの平等のための作業)、「合同」のような戦術を提供します。問題は、一連のリライト+コンストラクタのプロパティを使用して解決できます)。 SMTソルバはまた、これらの証明の義務を免除するためにも使用できます。大規模な算術ライブラリが大きな助けになることがあります。しかし、IMOでは、 'Vect'を捨てて、' List'sと一緒に行き、後であなたの関数に関するプロパティを証明する方が良いです –