5

Agdaで、同じ長さでなければならないベクトルのペアを定義するにはどうすればよいですか？

-- my first try, but need to have 'n' implicitly  
b : ∀ ( n : ℕ ) → Σ (Vec ℕ n) (λ _ → Vec ℕ n) 
b 2 = (1 ∷ 2 ∷ []) , (3 ∷ 4 ∷ [])
b 3 = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ [])
b _ = _

-- how can I define VecSameLength correctly?
VecSameLength : Set
VecSameLength = _

c : VecSameLength
c = (1 ∷ 2 ∷ []) , (1 ∷ 2 ∷ [])

d : VecSameLength
d = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ [])

-- another try
VecSameLength : Set
VecSameLength = Σ (Vec ℕ ?) (λ v → Vec ℕ (len v))
4

1 に答える 1

9

タイプの一部として長さを保持したい場合は、同じサイズのインデックスを持つ2つのベクトルをパックする必要があります。最初に必要なインポート：

open import Data.Nat
open import Data.Product
open import Data.Vec

特別なことは何もありません。通常のサイズのベクトルを書くのと同じようにn、これを行うことができます。

2Vec : ∀ {a} → Set a → ℕ → Set a
2Vec A n = Vec A n × Vec A n

つまり、2Vec A nはsのベクトルのペアのタイプでありA、両方ともn要素を持ちます。私はそれを任意の宇宙レベルに一般化する機会を得たことに注意してください-これはSet、たとえば、sのベクトルを持つことができることを意味します。

2つ目の注意点は_×_、通常の非依存ペアであるを使用したことです。Σこれは、2番目のコンポーネントが最初のコンポーネントの値に依存しない特殊なケースとして定義されます。

サイズを非表示にしておきたい例に移る前に、このタイプの値の例を次に示します。

test₁ : 2Vec ℕ 3
-- We can also infer the size index just from the term:
-- test₁ : 2Vec ℕ _    
test₁ = 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ []

このペアに不均一なサイズの2つのベクトルを詰め込もうとすると、Agdaが正しく文句を言うことを確認できます。

インデックスを非表示にすることは、従属ペアにぴったりです。手始めに、1つのベクトルの長さを非表示にする方法は次のとおりです。

data SomeVec {a} (A : Set a) : Set a where
  some : ∀ n → Vec A n → SomeVec A

someVec : SomeVec ℕ
someVec = some _ (0 ∷ 1 ∷ [])

サイズインデックスは型シグネチャの外側に保持されているため、内側のベクトルのサイズが不明であることがわかります（事実上リストが表示されます）。もちろん、インデックスを非表示にする必要があるたびに新しいデータ型を作成するのは面倒なので、標準ライブラリで提供されますΣ。

someVec : Σ ℕ λ n → Vec ℕ n
-- If you have newer version of standard library, you can also write:
-- someVec : Σ[ n ∈ ℕ ] Vec ℕ n
-- Older version used unicode colon instead of ∈
someVec = _ , 0 ∷ 1 ∷ []

2Vecこれで、これを上記のタイプに簡単に適用できます。

∃2Vec : ∀ {a} → Set a → Set a
∃2Vec A = Σ[ n ∈ ℕ ] 2Vec A n

test₂ : ∃2Vec ℕ
test₂ = _ , 0 ∷ 1 ∷ 2 ∷ [] , 3 ∷ 4 ∷ 5 ∷ []

コパンプキンは優れた点を提起します。ペアのリストを使用するだけで同じ保証を得ることができます。これらの2つの表現は、まったく同じ情報をエンコードします。見てみましょう。

ここでは、名前の衝突を防ぐために別のインポートリストを使用します。

open import Data.List
open import Data.Nat
open import Data.Product as P
open import Data.Vec as V
open import Function
open import Relation.Binary.PropositionalEquality

2つのベクトルから1つのリストに移動するには、2つのベクトルを一緒に圧縮する必要があります。

vec⟶list : ∀ {a} {A : Set a} → ∃2Vec A → List (A × A)
vec⟶list (zero  , []     , [])     = []
vec⟶list (suc n , x ∷ xs , y ∷ ys) = (x , y) ∷ vec⟶list (n , xs , ys)

-- Alternatively:
vec⟶list = toList ∘ uncurry V.zip ∘ proj₂

戻るとは、解凍するだけです。ペアのリストを取得して、リストのペアを作成します。

list⟶vec : ∀ {a} {A : Set a} → List (A × A) → ∃2Vec A
list⟶vec [] = 0 , [] , []
list⟶vec ((x , y) ∷ xys) with list⟶vec xys
... | n , xs , ys = suc n , x ∷ xs , y ∷ ys

-- Alternatively:
list⟶vec = ,_ ∘ unzip ∘ fromList

これで、ある表現から別の表現に移動する方法がわかりましたが、これら2つの表現が同じ情報を提供することを示す必要があります。

まず、リストを取得し、それをベクトルに変換して（経由）、次にlist⟶vecリストに戻す（経由）とvec⟶list、同じリストが返されることを示します。

pf₁ : ∀ {a} {A : Set a} (xs : List (A × A)) → vec⟶list (list⟶vec xs) ≡ xs
pf₁ []       = refl
pf₁ (x ∷ xs) = cong (_∷_ x) (pf₁ xs)

そしてその逆：最初にリストするベクトル、次にリストするベクトル：

pf₂ : ∀ {a} {A : Set a} (xs : ∃2Vec A) → list⟶vec (vec⟶list xs) ≡ xs
pf₂ (zero  , []     , [])     = refl
pf₂ (suc n , x ∷ xs , y ∷ ys) =
  cong (P.map suc (P.map (_∷_ x) (_∷_ y))) (pf₂ (n , xs , ys))

あなたが何をするのか疑問に思っている場合cong：

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

との間で同型list⟶vecをvec⟶list形成することを示しました。これは、これら2つの表現が同型であることを意味します。List (A × A)∃2Vec A

于 2013-03-16T03:36:30.387 に答える