4

vector-sizesが 暗黙的なままでapplyPrefixある長いベクトルの最初の部分に固定サイズのベクトル関数を適用するAgda 関数を作成しました。ヘルパー関数と一緒の定義は次のとおりです。mnksplit

split : ∀ {A m n} → Vec A (n + m) → (Vec A n) × (Vec A m) 
split {_} {_} {zero}  xs        = ( [] , xs )
split {_} {_} {suc _} (x ∷ xs) with split xs 
... | ( ys , zs ) = ( (x ∷ ys) , zs )


applyPrefix : ∀ {A n m k} → (Vec A n → Vec A m) → Vec A (n + k) → Vec A (m + k)
applyPrefix f xs with split xs
... | ( ys , zs ) = f ys ++ zs

applyPostfix固定サイズのベクトル関数を長いベクトルの末尾部分に適用する対称関数が必要です。

applyPostfix ∀ {A n m k} → (Vec A n → Vec A m) → Vec A (k + n) → Vec A (k + m)
applyPostfix {k = k} f xs with split {_} {_} {k} xs
... | ( ys , zs ) = ys ++ (f zs)

の定義がapplyPrefix既に示しているように、k-ArgumentapplyPostfixは使用時に暗黙のままにすることはできません。例えば：

change2 : {A : Set} → Vec A 2 → Vec A 2
change2 ( x ∷ y ∷ [] ) = (y ∷ x ∷ [] )

changeNpre : {A : Set}{n : ℕ} → Vec A (2 + n) → Vec A (2 + n)
changeNpre = applyPrefix change2

changeNpost : {A : Set}{n : ℕ} → Vec A (n + 2) → Vec A (n + 2)
changeNpost = applyPost change2 -- does not work; n has to be provided

を使用するときに -argument が暗黙的なままにapplyPostfixなるように実装する方法を知っている人はいますか?kapplyPostfix

私がしたことは、校正/プログラミングです:

lem-plus-comm : (n m : ℕ) → (n + m) ≡ (m + n)

を定義するときにその補題を使用しますapplyPostfix。

postfixApp2 : ∀ {A}{n m k : ℕ} → (Vec A n → Vec A m) → Vec A (k + n) → Vec A (k + m)
postfixApp2 {A} {n} {m} {k} f xs rewrite lem-plus-comm n k | lem-plus-comm k n |     lem-plus-comm k m | lem-plus-comm m k = reverse (drop {n = n} (reverse xs))  ++ f (reverse (take {n = n} (reverse xs)))

残念ながら、k補題を呼び出すために -Parameter を使用しているため、これは役に立ちませんでした:-(

k明示的であることを避けるためのより良いアイデアはありますか? 多分私はベクトルでsnoc-Viewを使用する必要がありますか?

4

1 に答える 1

6

できることはpostfixApp2、 と同じ型を与えることですapplyPrefix。

問題の原因は、自然数が既知の場合にのみn統一できることです。これは、が最初の引数の帰納法によって定義されているためです。p + qp+

したがって、これは機能します（私は標準ライブラリバージョンの可換性を使用しています+）：

+-comm = comm
  where
    open IsCommutativeSemiring isCommutativeSemiring
    open IsCommutativeMonoid +-isCommutativeMonoid

postfixApp2 : {A : Set} {n m k : ℕ}
            → (Vec A n → Vec A m)
            → Vec A (n + k) → Vec A (m + k)
postfixApp2 {A} {n} {m} {k} f xs rewrite +-comm n k | +-comm m k =
  applyPostfix {k = k} f xs

はい、applyPostfixここでオリジナルを再利用して、2 回書き直して別のタイプにします。

そしてテスト：

changeNpost : {A : Set} {n : ℕ} → Vec A (2 + n) → Vec A (2 + n)
changeNpost = postfixApp2 change2

test : changeNpost (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ≡ 1 ∷ 2 ∷ 4 ∷ 3 ∷ []
test = refl
于 2012-11-21T14:01:55.927 に答える