6

prefixAppベクトル関数をベクトルのプレフィックスに適用する Agda関数を作成しました。

split : {A : Set}{m n : Nat} -> 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 )

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k)
prefixApp f xs with split xs
... | ( ys , zs ) = f ys ++ zs

prefixApp長さの引数を明示的に指定せずに使用できるという事実が気に入っています。

gate : Vec Bool 4 -> Vec Bool 3
gate = prefixApp xorV

( xorV : Vec Bool 2 -> Vec Bool 1Vector-Xor-Function はどこにありますか)

postfixApp残念ながら、長さの引数を明示的に指定せずに使用できる -functionの書き方がわかりません。これまでの私の関数定義は次のようになります。

postfixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m)
postfixApp {_} {_} {_} {k} f xs with split {_} {_} {k} xs
... | ( ys , zs ) = ys ++ (f zs)

ただし、postfixApp常に長さの引数が必要なようです。例えば

gate : Vec Bool 4 -> Vec Bool 3
gate = postfixApp {k = 2} xorV

postfixAppこの非対称性を解消する方法、つまり、明示的な長さ引数なしで機能する関数を作成する方法を知っている人はいますか? 私は別の機能が必要だと思いsplitますか？

4

2 に答える 2

8

あなたprefixAppと、あなたは持っています

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k)

そしてあなたはそれに関数を渡すのでVec Bool 2 -> Vec Bool 1、それはそれを知ってn = 2おりm = 1、単純な統合によってです。次に、加算は左側の引数の再帰によって定義されるため、関数型の残りの部分はからに減少Vec A (2 + k) -> Vec A (1 + k)しVec A (suc (suc k)) -> Vec A (suc k)ます。Agdaは、次のような単純な統合（リテラル数の拡張）を適用できます。

Vec A (suc (suc k)) -> Vec A (suc k)
Vec Bool (suc (suc (suc (suc zero)))) -> Vec Bool (suc (suc (suc zero)))

それを推測するk = 2。

もう1つを見てください：

postfixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m)

xorV唯一の違いは、強制する既知の量が2nとm1になることですが、これにより、関数型の残りの部分のみがになりますVec A (k + 2) -> Vec A (k + 1)。加算は最初の引数の再帰によって定義されるため、このタイプはそれ以上減少しませんk。これは現時点では不明です。次に、とを統合しようとすると、k + 2Agdaは黄色を吐き出します。「でも明らかに」とあなたは言います！あなたは数学を知っていて、引き算や他の簡単な原理を適用できるのでそれを知っていますが、Agdaはそれを知りません。はそれに対する単なる別の機能であり、任意の機能アプリケーションを統合することは困難です。私があなたに統一するように頼んだらどうしますか4k + 13k = 2_+_(2 + x) * (2 + y)697、 例えば？タイプチェッカーは数を因数分解し、一意の因数分解がないことを不平を言うことを期待する必要がありますか？乗算は可換であるため、辺を制限しない限り、一般的にはありませんが、Agdaは乗算が可換であることを知っている必要がありますか？

とにかく、Agdaは、基本的に「構造的」量を互いに一致させる統合の方法しか知りません。データコンストラクターは、型コンストラクターと同様に、この構造的な品質を備えているため、すべてを明確に統合できます。それよりももっと凝ったことになると、「高階統一」の問題にぶつかりますが、これは一般的には解決できません。Agdaは、ミラーパターン統合と呼ばれる高度なアルゴリズムを実装しています。これにより、制限された種類のより複雑な状況を解決できますが、実行できないことがいくつかあり、関数適用の種類もその1つです。

標準ライブラリを見ると、型にナチュラルの加算が含まれるほとんどの場合、別の引数で完全に指定されていない限り、加数の1つ（左側）は一般に暗黙的ではないことがわかります（あなたの場合prefixApp）。

それをどうするかということに関しては、一般的に問題に取り組むことはあまりありません。しばらくすると、Agdaが推測できることと推測できないことについての感覚を身に付け、それから、否定できない議論を暗黙的にするのをやめます。の「対称」バージョンを定義することはできますが、_+_その両側で作業するのは同じように苦痛になるので、どちらもお勧めしません。

于 2012-10-20T02:30:59.747 に答える
1

実際、この関数はほぼ同じ型で定義できます。

postfixApp : {A : Set}{n m k : ℕ} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (k + m)
postfixApp f xs with splitAt' (reverse xs)
... | ys , zs = reverse zs ++ f (reverse ys)

test-func : Vec Bool 3 -> Vec Bool 2
test-func (x1 ∷ x2 ∷ x3 ∷ []) = (x1 ∧ x2) ∷ (x2 ∨ x3) ∷ []

test : postfixApp test-func (false ∷ false ∷ true ∷ false ∷ true ∷ [])
                           ≡ false ∷ false ∷ false ∷ true ∷ []
test = refl

コード全体: http://lpaste.net/107176

于 2014-07-09T13:18:44.383 に答える