5

Idris に、Vect のサイズを渡して Vect を作成する関数と、パラメータでインデックスを取得する関数を書き込もうとしています。これまでのところ、私はこれを持っています:

import Data.Fin
import Data.Vect

generate: (n:Nat) -> (Nat -> a) ->Vect n a
generate n f = generate' 0 n f where
  generate': (idx:Nat) -> (n:Nat) -> (Nat -> a) -> Vect n a
  generate' idx Z f = []
  generate' idx (S k) f = (f idx) :: generate' (idx + 1) k f

しかし、パラメーターで渡された関数が、Vect のサイズよりも小さいインデックスのみを取得していることを確認したいと思います。私はそれを試しました：

generate: (n:Nat) -> (Fin n -> a) ->Vect n a
generate n f = generate' 0 n f where
  generate': (idx:Fin n) -> (n:Nat) -> (Fin n -> a) -> Vect n a
  generate' idx Z f = []
  generate' idx (S k) f = (f idx) :: generate' (idx + 1) k f

しかし、エラーでコンパイルされません

    Can't convert
            Fin n
    with
            Fin (S k)

私の質問は次のとおりです。私がやりたいことは可能ですか？

4

2 に答える 2

4

Cactus の回答は、要求したものを取得するための最良の方法のようですが、実行時に使用できるものが必要な場合は、非常に非効率的です。これの本質的な理由は、 aFin nを aに弱体化するには、 aFin n+mを完全に解体してその の型を変更しFZ、それから再度構築する必要があるためです。Finそのため、各ベクトル要素に対して生成された値の間でまったく共有することはできません。Nat別の方法として、 aを、与えられた境界を下回っているという証明と組み合わせることです。これにより、消去の可能性が生じます。

data NFin : Nat -> Type where
  MkNFin : (m : Nat) -> .(LT m n) -> NFin n

lteSuccLeft : LTE (S n) m -> LTE n m
lteSuccLeft {n = Z} prf = LTEZero
lteSuccLeft {n = (S k)} {m = Z} prf = absurd (succNotLTEzero prf)
lteSuccLeft {n = (S k)} {m = (S j)} (LTESucc prf) = LTESucc (lteSuccLeft prf)

countDown' : (m : Nat) -> .(m `LTE` n) -> Vect m (NFin n)
countDown' Z mLTEn = []
countDown' (S k) mLTEn = MkNFin k mLTEn :: countDown' k (lteSuccLeft mLTEn)

countDown : (n : Nat) -> Vect n (NFin n)
countDown n = countDown' n lteRefl

countUp : (n : Nat) -> Vect n (NFin n)
countUp n = reverse $ countDown n

generate : (n : Nat) -> (NFin n -> a) -> Vect n a
generate n f = map f (countUp n)

Finアプローチのように、渡す関数generateはすべてのナチュラルで機能する必要はありません。未満のもののみを処理する必要がありますn。

タイプを使用して、すべての場合に証明を消去することNFinを明示的に示しました。LT m n私がそれを望まない/必要としない場合は、(m ** LT m n)代わりに使用できます。

于 2015-05-11T20:37:28.460 に答える
4

重要なアイデアは、ベクトルの最初の要素はf 0であり、テールの場合、 がある場合はk : Fin n、FS k : Fin (S n)その値とその型を同時にインクリメントする有限数の「シフト」です。

この観察を使用して、次のように書き換えることができますgenerate。

generate : {n : Nat} -> (f : Fin n -> a) -> Vect n a
generate {n = Z} f = []
generate {n = S _} f = f 0 :: generate (f . FS)

別の可能性は、@dfeuer が提案したことを実行してFins のベクトルを生成し、それをマップfすることです。

fins : (n : Nat) -> Vect n (Fin n)
fins Z = []
fins (S n) = FZ :: map FS (fins n)

generate' : {n : Nat} -> (f : Fin n -> a) -> Vect n a
generate' f = map f $ fins _

証明generate f = generate' fは、読者の課題として残されています。

于 2015-05-11T01:50:51.697 に答える