# HG changeset patch # User Shinji KONO # Date 1607033239 -32400 # Node ID 72ec93c67ab27fe71d8448396aea9283034e5d41 # Parent b169617e42e5b2a0be66e22b086f5db74606e7a7 ... diff -r b169617e42e5 -r 72ec93c67ab2 fig/fresh.graffle Binary file fig/fresh.graffle has changed diff -r b169617e42e5 -r 72ec93c67ab2 galois-prosym.ind --- a/galois-prosym.ind Thu Dec 03 17:50:45 2020 +0900 +++ b/galois-prosym.ind Fri Dec 04 07:07:19 2020 +0900 @@ -1,6 +1,6 @@ -title: Agda によるガロア理論 ---All connected +--All connected 数学の証明に計算機を使うのは既に古い歴史がある。Agda \cite{agda} は定理証明支援系だが、普通の関数型プログラミング言語でもあり、 群の要素の数え上げなどを直接に実行できる。この時に「正しく数え上げのか」ということが問題になる。4色問題が計算機を使って解かれた @@ -12,11 +12,9 @@ 計算結果が、ちゃんと要求された証明につなかっていることを示すことが可能である。つまり計算だけなくて、証明としてちゃんとつながっていることになる。 ここでは、例題としてガロア理論の一部である可解群を使い、証明を含むデータ構造として、 - Data.Fin 有限な自然数 FL 順列に対応する減少列 Data.List.Fresh Sorted List - を使う。一部は、AgdaのLibrary でる。 証明付きのデータ構造は assert と異なり、それを作成する段階で証明を構成する必要がある。証明は型の整合性の検査なので、 @@ -29,35 +27,26 @@ --ガロア理論 xの多項式f(x)が解を持てば因数定理により - -　 (x - α)(x - β)(x - γ) - + (x - α)(x - β)(x - γ) の形に因数分解可能である。αβγは定数だが、この三つを置換しても式は同じになる。つまり展開すれば同じ式になる。 つまり、順列の群である対称群が対応することになある。f(x)因数定理による分解 - -　 f(x) => (x - α)(g x) - + f(x) => (x - α)(g x) は、f(x)の対称群からg(x)の対称群への変換になる。具体的には三次の対称群から二次の対称群の変換がなければならない。 ここで二次式に帰着できれば変換があり、変換があれば三次式を二次式に変換できる。 三次の対称群、つまり三つの数の入れ替えは、αβγはγ..と.γ.と..γからなるが、 三次式を二次式に変換できるなら、αβγとβαγの二つの形にならないとおかしい。つまり、 - -　αγβ = αβγ - + αγβ = αβγ とγを移動できる必要がある。ということは、 - -　γβ=βγ - + γβ=βγ である必要がある。逆元をかけて - -　 β⁻¹γ⁻¹βh = e + e=β⁻¹γ⁻¹βγ +になれば良い(これは正確な話ではない)。左辺をCommutator(交換子)と呼び [β,γ]と書く。 -になれば良い。左辺がCommutator(交換子)と呼ぶ。ある群の二つの要素を取って交換子に変換したものを交換子群と呼ぶ。 +ある群の二つの要素を取って交換子に変換したものを交換子群と呼ぶ。 これは群から群への関手になる。交換子群を繰り返し作り、単元だけの群になる場合をSolvable 可解と呼ぶ。 -多項式に対応する対称群が可解であることがべき根を使って解けるための条件になる。 - -今回は可解と方程式がべき根で解ける部分には関与せず、2-5次の対称群が可解かどうかを計算で示す。 +多項式に対応する対称群が可解であることがべき根を使って解けるための条件になるとされている。 +今回は対称群が可解であることがが方程式がべき根で解ける条件であることには関与せず、2-5次の対称群が可解かどうかを計算で示す。 --Agdaによる Group の表現 @@ -70,7 +59,8 @@ Agda の型には Level があり、基本型の後に自然数で指定する。⊔ はLevelの最大値演算子である。 : の前が名前で、後ろが型である。 Carrier は要素の型であり、関係と演算子が{\tt Rel Carrier ℓ, Op₂ Carrier}と定義されているが、 -これらは{\tt Carrier → Carrier → Set ℓ} と {\tt Carrier →　Carrier →　Carrier } のことである。 +これらは{\tt Carrier → Carrier → Set ℓ} と {\tt Carrier → Carrier → Carrier } のことである。 +Agda は Haskell と同じく indent で構文のブロックを表している。 record Group c ℓ : Set (suc (c ⊔ ℓ)) where field @@ -83,33 +73,37 @@ open IsGroup isGroup public monoid : Monoid _ _ monoid = record { isMonoid = isMonoid } - open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid) - + open Monoid monoid public + using (rawMagma; magma; semigroup; rawMonoid) 群の構成要素は field で定義されているが、Monoid の公理 isMonoid などは module で定義されている。 -これらの field を適切に埋めれば良い。 +群を定義するにはこれらの field を適切に埋めれば良い。 順列は Agda に Data.Fin.Permutation - というのがあるので、それを使う。これは Data.Fin の間の Bijection として4抽象的に定義されている。 中括弧は省略可能な引数である。 +置換 p には二つの写像が中置演算子\verb+ ⟨$⟩,⟨$⟩ʳ+として定義されている。record の中にはBijectionの性質が入っている。 -- Data.Fin.Permutation.id pid : {p : ℕ } → Permutation p p - pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl } + pid = permutation ( λ x → x)( λ x → x) record + { left-inverse-of = λ x → refl + ; right-inverse-of = λ x → refl } -- Data.Fin.Permutation.flip pinv : {p : ℕ } → Permutation p p → Permutation p p - pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P } + pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record + { left-inverse-of = λ x → inverseʳ P + ; right-inverse-of = λ x → inverseˡ P } +という感じで簡単に逆元と単位元が求まる。 refl は data である {\tt x ≡ x} を生成する constructor である。 + +置換の同値性は写像が等しければよい。これを record で定義する。 record _=p=_ {p : ℕ } ( x y : Permutation p p ) : Set where field peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q - -という感じで簡単に逆元と単位元が求まる。Bijection の field は詳しく説明しないが二つの写像とBijectionの公理を表している。 - -identity の refl は data である {\tt x ≡ x} を生成する constructor である。 +これらを使って置換の群を以下のように定義できる。(prespとpassocなどはここでは記述していない) Symmetric : ℕ → Group Level.zero Level.zero Symmetric p = record { @@ -118,15 +112,20 @@ ; _∙_ = _∘ₚ_ ; ε = pid ; _⁻¹ = pinv - ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym } + ; isGroup = record { isMonoid = record { + isSemigroup = record { isMagma = record { + isEquivalence = record {refl = prefl + ; trans = ptrans ; sym = psym } ; ∙-cong = presp } ; assoc = passoc } - ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } )) } - ; inverse = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} )) + ; identity = ( (λ q → record { peq = λ q → refl } ) + , (λ q → record { peq = λ q → refl } )) } + ; inverse = ( (λ x → record { peq = λ q → inverseʳ x} ) + , (λ x → record { peq = λ q → inverseˡ x} )) ; ⁻¹-cong = λ i=j → record { peq = λ q → p-inv i=j q } } } +例えば identity は (ε ∙ x) =p= x だが、これは x ⟨$⟩ʳ q ≡ x ⟨$⟩ʳ q なので、refl で生成できる。 --Data.Fin @@ -136,10 +135,9 @@ data Fin : ℕ → Set where zero : {n : ℕ} → Fin (suc n) suc : {n : ℕ} (i : Fin n) → Fin (suc n) - zero と suc はNatと重なっているので Monomorphic な Agda では注意が必要である。このデータ構造は基本的には Nat と -同じだが、{\tt Fin zero }は作れない。{\tt # 1} と書く記法が用意されているが、{\tt n}が決まるように記述する必要が -ある。つまり、{\tt # 1} でも n が異なると別物になる。{\tt toℕ} で自然数を取り出すことができる。{\tt Fin n}を +同じだが、{\tt Fin zero }は作れない。\verb+# 1+ と書く記法が用意されているが、{\tt n}が決まるように記述する必要が +ある。つまり、\verb+# 1+ でも n が異なると別物になる。{\tt toℕ} で自然数を取り出すことができる。{\tt Fin n}を 作るためには、それが n よりも小さい証明が必要である。\verb+{n : ℕ}+ 省略可能で型推論により自動的に決まる。 決まらなければ Agda が黄色で instantiation が足りないと警告される。証明では黄色を全部消す必要がある。 計算自体は値が決まってなくても計算可能なところまで進む。これは関数型言語の特徴である。 @@ -164,7 +162,8 @@ この形で生成されるものを繰り返し生成したい。そのための生成演算子を以下のように定義する。 - data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where + data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) + : (f : Carrier) → Set (Level.suc n ⊔ m) where comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ] ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g @@ -179,7 +178,8 @@ という定義を持つ。交換子は積に付いて閉じてないので、交換子群を作る場合には以下の生成子も必要になる。しかし、 今回は単位元だけになるかどうかを知りたいだけなので、これは使わない。 - gen : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙ g ) + gen : {f g : Carrier} → Commutator P f → Commutator P g + → Commutator P ( f ∙ g ) 交換子の生成を繰り返すのが次の述語 deriving である。。これも Set (Level.suc n ⊔ m) を返してる。つまり証明するべき命題を返すような関数になっている。 証明はもちろん、Commutator で作られるλ項であり、⊤の構成子 tt で終わる。 @@ -209,7 +209,8 @@ counter-example : ¬ (abc 0<3 0<4 =p= pid ) counter-example = ? - end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid + end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x + → x =p= pid end5 = ? ¬sym5solvable : ¬ ( solvable (Symmetric 5) ) @@ -244,8 +245,10 @@ このListに大小関係を入れる。 data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where - f +
data List# : Set (a ⊔ r) fresh : (a : A) (as : List#) → Set r @@ -395,8 +403,8 @@ これを使うと -FList : {n : ℕ } → Set -FList {n} = List# (FL n) ⌊ _f ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) - FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a ¬a ¬b lt = + cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) + FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a