2

私は依存型に不慣れで、Haskell の経験があり、ゆっくりと Idris を学んでいます。演習として、ハフマン エンコーディングを書きたいと思います。現在、コード ツリーの「平坦化」によってプレフィックス コードが生成されるという証明を書こうとしていますが、量指定子に行き詰まっています。

あるリストは別のリストのプレフィックスであるという単純な帰納命題があります。

using (xs : List a, ys : List a)
    data Prefix : List a -> List a -> Type where
        pEmpty : Prefix Nil ys
        pNext  : (x : a) -> Prefix xs ys -> Prefix (x :: xs) (x :: ys)

  1. これは有効なアプローチですか？または、「xs ++ zs = ysのようなzsがある場合、 xsはysのプレフィックスです」のようなものが良いでしょうか?

  2. 「forall」量指定子を導入するのは正しい方法でしたか (私が理解できる限り、Agda では のようなものになりますpNext : ∀ {x xs ys} → Prefix xs ys → Prefix (x :: xs) (y :: ys))? pNext の最初の引数は暗黙的であるべきですか? 2 つのバリアントの意味上の違いは何ですか?

次に、どの要素も別の接頭辞を形成しないベクトル用に作成したいと思います。

data PrefVect : Vect n (List a) -> Type where

空ベクトルには接頭辞がありません:

    pvEmpty : PrefVect Nil

要素 x、ベクトル xs、および xs のどの要素も x の接頭辞ではない (およびその逆) という証明が与えられると、x :: xs はそのプロパティを保持します。

    pvNext  : (x : [a]) -> (xs : Vect n [a]) ->
              All (\y => Not (Prefix x y)) xs ->
              All (\y => Not (Prefix y x)) xs ->
              PrefVect (x :: xs)

これは無効な型であり、最初のものを処理した後に修正したいと考えていますが、pvNext の量指定子について同様の質問があります。

ありがとうございました。

4

1 に答える 1

4

[a]ここでの唯一の問題は、Haskell スタイルでは のリストのタイプとして使用したのaに対し、Idris では である必要があることだと思いますList a。

あなたのPrefixタイプは私には問題ないように見えますが、次のように書きます：

data Prefix : List a -> List a -> Type where
     pEmpty : Prefix [] ys
     pNext : Prefix xs ys -> Prefix (x :: xs) (x :: ys)

つまり、暗黙的にすることができ、 Idris はとの型を推測できるためx、 は必要ありません。これが正しいアプローチであるかどうかは、型を何に使用する予定かによって異なります。リストが別のリストのプレフィックスであるかどうかをテストするのは確かに簡単です。何かのようなもの：usingxsysPrefix

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Maybe (Prefix xs ys)
testPrefix [] ys = Just pEmpty
testPrefix (x :: xs) [] = Nothing
testPrefix (x :: xs) (y :: ys) with (decEq x y)
  testPrefix (x :: xs) (x :: ys) | (Yes Refl) = Just (pNext !(testPrefix xs ys
  testPrefix (x :: xs) (y :: ys) | (No contra) = Nothing

否定を証明したい場合は、次のようにする必要があります。

testPrefix : DecEq a => (xs : List a) -> (ys : List a) -> Dec (Prefix xs ys)

私はそれを練習として残します:)。

于 2014-12-03T09:27:41.493 に答える