北海道苫小牧市出身のPGが書くブログ

今日は 圏論勉強会 第2回 の日です

math, レポート

圏論勉強会ではないモノイド勉・・・いや、圏論勉強会 第2回に来ました。資料とustreamは公開されています。

第2回: モノイド・群 / 講師 @9_ties さん

• モノイド、圏は計算機に必要な概念
  • 対象が1つの圏。シンプルだけどシンプル過ぎない圏
• 約束: 自然数は0以上。Haskell的なセクションの記法を使う
• モノイド: (M, ・)の組。結合率、単位元
  • M は台集合
• モノイドの例
  • 自然数(N, +), (N, ×)
  • 整数、有理数、実数、複素数も同様
  • Aの要素の有限列と、++
    • ([1,2] ++ [3, 4]) ++ [5,6] == [1,2] ++ ([3,4]++[5,6])
    • []が単位元
  • 文字列も同様
  • 論理和(単位元false)、論理積(単位元true)
  • 集合の∪(単位元Φ)と∩(単位元A)。(ただし、冪集合P(A)の元を使う)
  • max(単位元は最小値)、min(単位元は最大値)
  • 「有界半束はモノイド」
• データ列の集約・集積演算はモノイドと関連: folding
  • sum、filter、min、max、any、allなどなど
  • 直列化できるコンテナであれば、モノイドで畳み込みができる
  • 結合性により、部分列から畳み込む事ができる → 並列計算に応用できる
• 実用上はmapでモノイドの値にマッピングしてから畳み込む
  • foldMapという関数でOK
  • Data.Treeの例。IntはMonoidじゃないので、Sum*1にmapするといい
  • foldMap Sum tree でOK。
  • 接点を数える foldMap (\x -> Sum 1) tree
  • リストにする foldMap (\x -> [x]) tree
  • 集合にする foldMap (\x -> Data.Set.singleton x) tree
  • 論理 foldMap (All . even) tree、foldMap (Any . even) tree、
  • タプル foldMap (\x -> (Sum x, Product x)) tree
  • 文字列もモノイド foldMap show tree
• モノイドでできること、できないこと
  • 画像の集合から画像の集合への写像を集積すれば絵を描ける
  • ロボットの状態の集合からロボットの状態の集合への写像を集積すればロボットを操作できる
  • オートマトンとかでも。となると、正規表現も。
• endomorphism(自己準同型写像): ドメインとコドメインが同じ集合である
  • End(A)はモノイド(作用素モノイドの一例)
• instance Monoid (End a)が標準ライブラリに！
  • appEndo (foldMap (\x -> if even x then End (* x) else End (+ x)) tree) 0
  • 足し算とかけ算を混ぜられるようになった
  • 1つの"モノ"に対して、それを変化させる写像を集めると"モノ"イドになっている
• endmorphismで任意のモノイドを表せそう
  • 1 + 2 + 3 == (1 +) . (2 +) . (3 +)
  • これをきちんとした言葉で述べたい
• モノイド準同型 : モノイドからモノイドへの構造を保ったマッピング*2
  • 二項演算と単位元を保つ
  • 例 length:([A], ++) → (N, +)
• モノイドの同型
  • 同型写像: 準同型fで、f.g=id, g.f=id なるgがあるもの
  • 例: f(x) = 2^x。 f: (N,+) → ({2^n}, ×)
  • log により、かけ算を足し算にできるね、という話。天文学者の寿命が倍になったと言われた
• 部分モノイド: 台集合に包含関係がある2つのモノイド
• 定理: 任意のモノイドは、適当な集合AについてEnd Aの部分モノイドと同型
  • 表現定理の一例(線形写像を行列で表現、なども)。正体が掴みやすくなる
  • 米田の補題への第一歩
• 証明:
  • Mにたいして、a→(a・)を考えると、(a・).(b・) = (a.b・)、(e・) = idよりa→(a・)は準同型
  • 逆に(a・)→(a・)(e)を考えるとこれも準同型
  • 合成するとidになるので同型
• (・a)でとる場合は、反モノイド(合成を逆にとる)にする必要がある
• foldrとfoldl → 畳込みなのでモノイドと関連するはず
  • foldrはA×B→B、foldlはB×A→Bをとる
  • foldrで(p・).(q・).(r・)と書き直すと、End Bのなすモノイドになっている
  • foldlでは逆
  • 自己準同型へのマッピングをしていると考えられる
• 例: (1 :)、(2 :)、(3 :)みたいな作用を畳み込みたい
  • foldr (\x -> (x :)) [] [1, 2, 3]
  • 2が来たら捨てるような操作も → foldr (\x -> if x == 2 then const else (x :)) [1, 2, 3]
• foldrやfoldlは足し算とかに使うものではない。endomorphismのモノイドを生かして使うべき
• すべてfoldrでいい！という考え方ではダメ
  • foldrのB→Bの部分にありとあらゆるモノイドが存在する。
  • 何でも書けるが汎用的過ぎる。個性的なモノイドを生かさないと可哀想
  • (a×)と(+b)のendmorphismからなるモノイド → ax + bなモノイド。
  • つまり (a, b)・(c, d) := (ac, ad + b)とするとモノイドになる*3
  • foldMapで扱える
  • foldMapは並列化しやすいが、foldrは代入するので並列化しにくい、というのもある
• foldMap fも列のモノイドからのモノイド準同型
  • 列は特別。ありとあらゆる畳み込みが列のモノイドからできる
  • 列のモノイドは自由モノイドの性質を持つ
• 抽象的な自由モノイドの定義
  • 列のモノイドは、長さ1の列で現せる。情報が失われていない
  • モノイド準同型から、長さ1の列のマッピングがあれば、全ての列をマッピングできる
• ([A], ++) → (M,・) / A → M 随伴関係
  • i(a) = [a] とすると、 foldMap f . i = fが可換であれば、モノイド準同型foldMap fは唯一存在する。
• 自由モノイドは同型を除いて一意。列・連結からなるモノイドと同じと見なせる
• プログラムもモノイド(2項演算は文を並べる事。単位元は何もしない)
  • モナドは自己関(以下略
• 群 : モノイド。逆元(inverse)が存在
• 群の例
  • Z、Q、R、Cと足し算
  • Q/{0}、R/{0}とかけ算
  • 逆に、(N, +)、(N,×)、([A], ++)は群ではない
  • 正二面体群: 正3角形。120度回転、対称移動、恒等変換、を組み合わせると群
  • 対称性を表すものが群
  • 暗号: 文章の集合のhomomorphismであるAut。復号化できる=群。逆元の計算が困難な部分群を探す事が強力な暗号を探す事
• Aut(automorphism)とは・・・全単射なhomomorphism。自己同型写像
  • Aut(X)は自己同型写像を集めた群
• 定理: 群Aは集合AについてAut(A)の部分群と同型
• 対称群 Sym(A):集合上の自己同型群、置換群: 対称群の部分群
  • 数値で表せる。分解できる→計算機で扱いやすい
• ケイリーの定理: 任意の群は適当な置換群と同型
  • 先ほどの定理と同じことを言っているが置換は計算機で扱いやすいのがポイント
• 有限群(= ルービックキューブ、48次対称群)を持参しました。
  • 3カ所のみ色を変えるデモ
  • 置換群と同型のはず。構造を調べる
  • できること、できないことは群の構造をみるとわかる
• 今日の話はAwodeyの1章。結構読めるようになったのでは？

ツイートする

Permalink | コメント(0) | トラックバック(0) | 19:57

fmap head VS sequence

haskell

sequenceを使えば、複数個あるモナド値を1つのモナド値に集められる。

xs :: (Functor m, Monad m) => m [()]
xs = sequence [return x' | x' <- [(),()..]]

xsはモナドに包まったリストなので、fmapを使ってheadを持ち上げれば先頭要素がとれる。

x :: (Functor m, Monad m) => m ()
x = fmap head xs

これをIdentityモナドとして動かしてみる。

> runIdentity x
()

よし！ Writerモナドとして動かしてみる。

> runWriter (x :: Writer () ())
((),())

よし！ ただ、()はMonoidとはいえ何も情報を持てなくてあんまりなので、[()]くらいにしてみる。

> runWriter (x :: Writer [()] ())
((),  C-c C-cInterrupted.

WTF!! なんてこった！ どうしてこうなったのか。

検証

直感的には、xsはm [()]という型を持っているが、リストなのは値であって副作用の側には言及してない。headがかかるのも値だけであり、副作用については無限リストすべてから集めてみないとわからず、そのため停止しないってことじゃないかと予想できる。

確かめてみよう。扱うのがモナドであっても、圏論なんて全く関係なくて必要なのは単なるλ計算だ。実際の実装とだいぶ違うが、わかりやすさのために以下の項を定義として調べてみる。headやfst、sndなんかはよく知ってる定義通りとしておく。

return = λv -> (v, [])
(>>=) = λ(v,n) f -> (fst (f v),n ++ snd (f v))
sequence = λ((v,n):xs) -> (v,n) >>= (λv -> ((v:fst (sequence xs)),snd (sequence xs)))
fmap = λf (v,n) -> (f v,n)

問題の項xに該当するのは以下。

fmap head (sequence [((),[]), ((),[])..])

簡約してみる。

fmap head (sequence [((),[]), ((),[])..])
↓
(λ(v,n) -> (head v,n)) (sequence [((),[]), ((),[])..])
↓ F1 = (λ(v,n) -> (head v,n)) と置く
F1 (((),[]) >>= (λv -> ((v:fst (sequence [((),[])..])),snd (sequence [((),[])..]))))
↓ F2 = λv -> ((v:fst (sequence [((),[])..])),snd (sequence [((),[])..])) と置く
F1 ((λf -> (fst (f ()),[] ++ snd (f ()))) F2)
↓
F1 (fst (F2 ()),[] ++ snd (F2 ()))
↓ F1を展開
(head (fst (F2 ())),[] ++ snd (F2 ()))

これでタプルの状態、すなわちWriterモナドの値にまで簡約できた。先ほど残念な結果となった出力をよく見てみるとわかるが、タプルの1要素目、つまり値の側は実はきちんと計算が終わっている。まずはこちらを簡約してみる。

head (fst (F2 ()))
↓ F2を展開
head (fst ((():fst (sequence [((),[])..])),..略..))
↓
head (():fst (sequence [((),[])..]))
↓
()

fmap headが効いてくれてうまく簡約できた。じゃあ、2つ目の要素、つまり副作用を表す側はどうかと言えば・・・。

[] ++ snd (F2 ())
↓
snd (F2 ())
↓ F2を展開
snd (..略..,snd (sequence [((),[])..]))
↓
snd (sequence [((),[])..])
↓
snd (((),[]) >>= F2)
↓
snd (fst (F2 ()), [] ++ snd (F2 ()))
↓
[] ++ snd (F2 ())

戻ってしまった。ということで、第2要素は⊥であることがわかった。

ところで、そうなるともう1つ疑問なのが、なぜ Writer () () に関しては⊥とならず値を求めることができたのか、ということだ。これは()に対する`mappend`の定義を見るとわかる。

_ `mappend` _ = ()

そう、mappendは非正格な関数なのである。よって、

() `mappend` snd (F2 ()) == () `mappend` ⊥ == ()

となり、計算はきちんと停止する。

ツイートする

Permalink | コメント(0) | トラックバック(0) | 16:28

今日は 圏論勉強会 第1回 の日です

レポート, math

圏論勉強会ではない圏論勉強会 第1回に来ました。資料とustreamは公開されています。

@seizans さんより

• ekmett勉強会でekmettさんが圏論勉強するといいよというから開催
• 日本始まったな

講師 @9_ties さん

• 圏論だけではなく、圏論を題材に色んなことを学ぶ会
• 関数型言語を学ぶ会ではない。前提知識はなし
• 教科書はSteve AwodeyさんのCategory Theory。数学専攻してない人向け
  • 記法などは「圏論の基礎」。数学専攻者向け。リファレンス
• 今日は、圏論とは何か。随伴までいく
• 対 → (A, B)とかPair A B
  • (double, double)だと複素数型になる
  • a << 16 | b という自然数もpair
  • 対の具体例はいくらでもある
• 抽象概念を考えるには、定義が重要
  • 定義を飛ばしては行けない
  • 抽象的な定義。より多くの具体例を持つもの
• 対P
  • first : P → A, second : P → B 中身を取り出す関数
  • firstとsecondを持つPはいくらでも考えられる
  • firstとsecondもいくらでも考えられる
  • f : X→A、g：X→Bを考える。
  • fとgをまとめるu : X → Pがあるはず
  • f == first . u, g == second . u → 図式が可換(commutative)である
  • 可換 → 合成結果が全て等しい
  • 唯一性が必要 → Pに余分なデータがない、と言えるだろう
• 等式を図式で表現できるのが圏論のいいところ。等式を弄らなくて良い
• P、first、secondの"普遍性"。「一意的に分解」
  • Pを定めるとuが一意に定まる
• 定数1は、const 1として表現する*1
• 抽象化 → "型"、"関数"、"関数合成"で説明したが、その具体的性質は使ってない
  • "物"と"矢印"。
  • "物"を部分集合、"矢印"を包含関係としてみてみる → {1, 2}と{1, 3}の対は{1}。対=共通部分
  • "物"を自然数、"矢印"を大小関係 → 4と6の対は4。対=min
  • 「積(product)」という → 無関係と思われるの概念が繋がった
• 内部構造ではなく、外部との関係で物事を特徴付けている
• 圏論は「良い言葉」。Haskellを使う時はもちろん、それ以外の場面でも役に立つ
  • 何かを考える時は、矢印で考える
• Q. なぜ3は1と4の積じゃないの？ → 4 を分解できない
• 圏の定義
  • 対象(object)、射(arow, morphism)、合成(composition)
    • dom, cod : 射の元の対象と先の対象 : f : A→Bならdom f = A、cod f = B
    • 合成 g . f
  • 結合律(associative law) : (h.g).f = h.(g.f)
  • 恒等射(identity) 1 : A→A、f.1=1.f=f
• 「対象と射の集まりで、合成ができ、合成の順は気にしなくて良く、恒等射がある」
• 恒等射を1_Aと書くのは？ → 対象Aについて一意に定まるから(複数個ない)
  • 証明 : 1_A と 1_A' があるとすると、1_A = 1_A . 1_A' = 1_A'
  • 圏論の証明はdiagram chasingと呼ばれる
• 同型 : "等しさ"の定義の1つ。
  • {0,1,2}と{1,3,5}は"等しい"だろうか？
  • 数が同じ。「ある意味等しい」だろう
  • 圏論には色々な等しさの定義がある*2
  • g . f = 1, f . g = 1 であるときfは同型射(isomorphism)。gは逆射(inverse)
  • 同型射があるなら、2つの対象は同型
• 「この圏では同型である」「この圏では同型ではない」ということが起こる
  • 集合が対象、射が恒等関数とすると、{0,1,2}と{1,3,5}は同型ではない
  • 集合が対象、射が任意の関数とすると、{0,1,2}と{1,3,5}は同型(同型射は6つある)
  • 周りの関係性から、"等しさ"を考えている
• 逆射は一意に定まる
  • gとhが逆射とすると、g = g . 1 = g . f . h = 1 . h = h
• 関手(functor) : 圏から圏へ構造を保つマッピング
  • 構造とは？ → 対象、射、合成、恒等射
  • F(g . f) = Fg . Ff, F 1 = 1
  • 定義を音読して訓練
• 関手は可換図式を保つ
  • 同型射、逆射も保たれる
• sizeは有限集合と包含関係の圏から自然数と順序関係の圏への関手となる
• Listは関手 (型Aを型[A]に移す)
  • map (show . (* 2)) == (map show) . (map (* 2))
  • 数学的には同じだが、(一般的には)メモリ効率が違うと予想される。運算に使える
• 双対性 : 表裏一体
  • 双対圏 射を引っくり返したもの
  • 双対圏でminをとるとmaxになる
  • 双対圏で共通集合をとると和集合になる
• 積(product)の双対は余積(coproduct) *3
• 対の双対は？ → 貼りあわせ Either
• 代数的データ型 → 対は直積、貼りあわせは直和と呼ぶ
• AとBの積は、全部同型 → 同型を除いて一意、という
  • 一意なのでA×Bと書ける*4、一意の射を<f, g>と書ける
• 自然性
  • sumとlength、リストの概念において自然と言えるのはどちら？
  • sumは要素の方で決まる。lengthは型に依存しない
  • 関手Fは、元の圏の対象をパラメータに持つ概念だと思える
  • 「自然」とは、対応関係がパラメータの構造に依存しないこと
• 自然変換 (natural transformation)
  • 概ね、多相関数のこと → length : [a] → a
• 自然変換は関手と関手の対応
  • 関手圏 : 対象が関手、射が自然変換
  • 「モナドは単なる自己"関手の圏"におけるモノイド対象だよ？」
• 様々な抽象概念は随伴(adjunction)という概念で統一される
  • 積圏C×C内のf, g と 圏Cの<f, g> と1対1の対応関係がある(全単射がある)
  • この対応関係は自然である
  • F X = (X, X)とG (A, B) = A×Bで定義される2つの関手は随伴となる
  • π_1とπ_2は、id_A×Bを考えれば、余単位元(counit)として現れる
  • 単位元(unit)というものもある
  • 随伴は関手と自然変換で語れる。具体的な対象、射に基づかない。汎用的
  • 随伴に関する定理を知っておくと、様々な例に適用できる
  • 全てのモナド、コモナドは随伴から作れる

ツイートする

Permalink | コメント(0) | トラックバック(0) | 19:57

スツルムの定理の直感的な解説

math

昨日の計算機代数勉強会で代数的実数の実装のために出てきたスツルムの定理、共立出版の数値解析でも近似値の算出に使っており、証明も詳しく載っている。互除法だけではなく3重対角行列の主小行列式がスツルム列をなすことを使って固有値の算出をしたりもしている。

スツルムの定理は直感的にはそんなに難しいことは言ってない。

図の黒線のように根を何個か持つ多項式から始まって紫線のように最終的に根を持たない多項式に至る列がスツルム列だ。

wikipediaに書いてある4.のルールにより、根を持つ点で傾きが正の部分であれば上に、傾きが負であれば下方向にグラフが抜ける。そのため、スツルム列の0番目から1番目において根は左方向に動くことになる。また、2.のルール(wikipediaの記述は間違っているが)のために1番目以降も根はひたすら左に動き続ける。

aでの符号が変わることは、根が1つ区間の左側に抜けて消えたことを意味する。

bでの符号が変わることは、区間の右側から新たな根が混入したことを意味する。

最終的に根がない状態でスツルム列は終わっているので、aの符号の変化からbの符号の変化を引けば、0番目の多項式が何個根を持っていたかわかるという寸法である。

ツイートする

Permalink | コメント(0) | トラックバック(0) | 15:27

今日は Haskellで計算機代数勉強会 の日です

レポート, math

せっかくのGWなので、朝からHaskellで計算機代数勉強会に来ています。内容が内容なので正確性は保証できませんが、自分用のメモということで。

HALでもわかるGröbner基底 / @mr_konn さん

• グレブナー基底
  • 高次連立方程式、初等幾何、統計ロボティクス、計算機代数などに使える
  • 1960年代、廣中さんが特異点解消のために作った → 技術の進歩で計算可能に
• 体上多項式環のイデアルのよい生成元
• 体(たい): 四則演算ができる構造。整数はだめ(割り算が) k (ドイツ語だとケルパーらしい)
• 多項式環 k[x,y,...]。和、差、積がある。割り算はできるとは限らない
• イデアル: c∈Rに対してcx∈I。倍数の概念の一般化。
  • <a>⊂<b> aはbの倍数
  • 零点の成す図形(根基イデアル)
  • <y-x^2> 放物線、<y^2 + x^2 - 1, y + 2x - 1>、円と直線の交点
  • 図形や連立方程式に関する計算が簡単にできる
• 生成元
  • <f1, ..., fn>で生成されるイデアルは、線形和
  • 体上多項式環のイデアルは有限個のf1...frで書ける(ヒルベルトの基底定理)
• Noether環上の多項式環はNoether環である
  • 任意のイデアルが有限個の生成元で書ける = 計算機で扱うには有限個の多項式
  • 体の場合にはグレブナー基底を使うと簡単に済ませる
• 性質がよい、とは？
  • x^3+x^2+x+1、x^2-x-2で生成されるイデアルに、x^3-1とx^2+1に含まれるか？
  • 最大公約式を求めると良い→Euclidの互除法 (割った余りで再帰的に割る)
  • I = <x + 1>なので、どちらも属さない (x^3 + 1なら属しそう)
• 多変数に一般化したい
  • X^2Y - 1、X^3-Y^2-Xで生成されるイデアルにX^2Y^2-X^3Y-XY-1は含まれる
  • 最大公約式はとれない (<X, Y>を考えれば単項で生成できない)
  • 割り算を一般化。多項式を並べておいて、順に割れないか試す
  • 都合の良い並べ方が必要 → 単項型順序
• 1, x^2, xy, y^2 → 単項式
  • 係数をかけて加えたものが多項式
  • 順序を入れると、自然数ベクトルと同一視できる(x^2 = (2, 0))
• 単項式順序(monomial order)
  • 全順序性、加法性(α<=β ならば α+γ<=β+γ)、α>=0 (非負性) *1
  • 整列性(< に対して最小値を持つ)と降鎖条件(>に関する無限か後列が存在しない)と非負性は、全て同値
• 単項式順序の例
  • 辞書式順序は単項式順序、逆辞書式順序は単行式順序じゃない
  • 次数付辞書式順序 : 全次数で先に比べて、辞書順
  • 次数付逆辞書式順序は単項式順序 (grevlex) → グレブナー基底の計算で速いのはこれ
• 記号 → 単項式順序で一番大きい項について、先頭単項式(LM(f))、先頭係数(LC(f))、先頭項(LT(f))
• f = x + 2y^2w + 3z^2 には (1,0,0,0) (0,2,0,1) (0,0,2,0)がある
  • lex LT(f) = x
  • grlex LT(f) = n2y^2w
  • grevlex LT(f) = 3z^3
• 多項式版の割算を定義
  • 先頭項に着目して割っていく。割れない先頭項は横によけていく。
  • あまりの問題 → 割る順で余りが変わってしまう *2
  • 割り算の余りが順番に寄らないような生成減が欲しい → グレブナー基底
• イデアルの元の先頭項が、基底の先頭項で生成される
  • グレブナー基底は、簡約すると一意に決まる
• グレブナー基底の計算方法 : Buchbergerアルゴリズム
• S-多項式 → S(f, g) 先頭項同士を打ち消す
• Buchberger判定法
  • 単項式順序は決めてある。GはIの生成元
  • 「Gが>に関するグレブナー基底」と「S-多項式が余り0」は同値
• Buchbergerアルゴリズム → 余りが0じゃないものを再帰的に集める
  • 例: x^2y-1, x^3-y^2-xのグレブナー基底
  • grevlexは少ないけど、lexだと非常に多くの基底になる
• grevlexが小さい基底が求められやすいとされる(ヒューリスティック)
  • lex を使う場合もある → 変数消去。grevlexは駄目だが、lexを嫌って直積順序や重み付け順序も使ったりする
• Buchbergerアルゴリズム には無駄がある
  • 被約グレブナー基底
  • 極小 → LT(g) = 1、LG(g)は他のLT(g)で割れない
  • 被約 → どの項もLT(g)で割れない
• 被約グレブナー基底は、一意。イデアルが等しいかの判定にも使える
  • 極小化 → LT(g)でわって、条件を満たさないものを除く、そして被約化
  • 最初から 被約グレブナー基底 を求めるアルゴリズムも
• 最適化手法 → ナイーブな実装だと遅い。千倍くらい変わる
• ゼロ簡約関係
  • Buchbergerアルゴリズムは割り算なので遅い。grevlexは割り算が少ない
  • 「割って余りゼロ」を一般化 → ゼロ簡約規定で置き換えるとよい
  • S-多項式の余りが0の時、先頭単項式が互いに素の時、ゼロに簡約される
  • 互いに素かどうかを判定し、除く
• S-多項式はsyzygyの基底。syzygyとは先頭項を打ち消せるもの
  • 余分な基底を予め除く
• 実装の改良 → STモナドを使う。先頭項を昇順に並べる(割り算を少なく)
• sugar strategy
  • 基底の候補を選ぶ方法は自由
  • normal strategy → LCMが最小のもの (lexなどはNG)
  • sugar strategy → 斉次化次数(仮想的)なもの
  • 斉次式 → 全ての次数が等しいもの(項を勝手に足す)。
  • 最終結果に影響を与えないため仮想的にやる(sugar)
• selection strategy → 優先度キューの優先度として実現できる
  • 論文に出て来る例については、sugar strategyは速い
• 並列での実装もあり、そちらだと非常に速いらしい(F4アルゴリズム。F5もあるらしい)
  • 行列計算になるので、HaskellのようにGCだとメモリ管理とか厳しいかも
• computation-algebra パッケージでは依存型と証明のオンパレード
  • DataKinds、GADTsなどを利用
  • (haskel platformでは)外部ライブラリが使えなかったりもする
• イデアルはリストではない。sized-vectorにしている
• 帰納法はコストがかかる。(nとの比較、nステップかかる)
• シングルトンもコストがかかるので、依存型の実用はまだ厳しい
  • 証明は実行時に遅延されてしまう
• GHC7.4.*では厳しい

グレブな基底の応用について / @ikegami__ さん

• 書籍
  • グレブナー基底の計算 基礎編
  • グレブナ基底と代数多様体入門
  • グレブナ道場 (最新の話題、Linuxの上での環境構築など。1冊で分からないのはきついかも)
• アンケートの結果、初等幾何の自動証明の話をする
  • 他、Computational Oriented Matroids (例がHaskellで書いてある)
• 数式処理 → シンボルに基づいた計算をコンピュータにさせる
• 数式処理の対象 → シンボルや代数。幾何は特殊
• 山本先生は、「学習過程とグレブナ基底は同じ」とおっしゃってる
• 初等幾何の自動証明
  • 「自動」→証明をするわけではない
• 「初等幾何は、右脳と左脳を扱うのでいいらしい」
• 「コンピュータは計算をさせるものではなく、洞察を得るもの」
• 証明とは？ → 結論が前提から飛躍なく求められること
  • ユークリッドの公理。ユークリッド座標に翻訳
  • 多項式が並ぶ
  • 証明を作るのは諦める。前提と制約をわけて、前提において結論が満たされること
• グレブナ基底の発表。普通の人は15分しかない。
  • 全てを解くのを諦める
• グレブナ基底による初等幾何
  • 前提から制約を導出して、結論もあわせて多項式に変換(人間がやる)
  • 前提と制約をすべて=0の形の方程式に。グレブナ基底が{1}なら常に満たされるという意味
• 問題点
  • 人間が翻訳している
  • 翻訳方法が一意じゃない
  • 変数量が多いとメモリ・計算量が無理*3
  • 翻訳によると実数上に解がないこともある → コンピュータではお手上げ
  • 平行四辺形が潰れることもある(退化)
  • 複素数体(代数的閉体)と実数体の違い
• ウーの方法
  • 擬除算、擬剰余 (グレブナー基底も忘れて解決する)
• おまけ: コンピュータの成長
• ピタゴラスの定理をコンピュータはわかるのか
  • QuickCheckで3 4 5の組は探せる(maxSuccess=12345)
• Z3
  • IntでやるとNG。Realでやるべき
  • 有料だがアカデミックであれば大丈夫無料。もしくはZ3py
• 初等幾何の問題をコンピュータが理解する ⊃ 2021年 東ロボプロジェクト 21robot.org
• おまけのおまけ: 幾何の証明における誤り
  • 1). 明白な誤り、2). 前提の誤り、3). 有限回の適用で証明できない (適用の誤りがないのはなぜ？)
  • 証明は無限だと駄目だけど、命題の記述が可算無限になる体系は存在
  • 「Inferential Analysis(推理解析学)」流行らなかったぽい
  • Wangさん、Gelernterさんとか
  • ゴールから逆向き推論。枝狩り(Gelernter's distance)

代数的実数とCADの実装紹介 / @masahiro_sakai さん

• 有理数係数多項式の根になっている実数
  • √2や-√2
  • 複素数iや超越数πやeは含まない
• 多項式制約の解、演算、計算可能、数値誤差もない(定理証明では誤差は困る)
• 多項式の根は複数 → 多項式だけでは根は得的できない
  • 多項式+根を1つ含む区間で表現する (表現は一意ではない)
  • AReal (UPolynomial ...) (Interval ...)
  • 有理数係数の最小多項式 (最高次係数 1、割れない)
• 他の表現
  • 根の番号
  • 代数的実数係数の多項式とか(表現は簡単)
• realRoots 根を全て求める
  • 因数分解して、
  • 根の限界を係数の絶対値で評価できる
  • スツルムの定理で根を数える
• 演算: 近似値計算、比較、四則演算、代数的実数係数の根
  • 近似値 → スツルムの定理で絞り込める
  • EqとOrdの実装
    • 等号は多項式が等しく、範囲の重複部分に根があるとき
    • 不等号はスツルムの定理で追い込んで判定
• 四則演算: 有理数との演算は、変数変換と区間演算で簡単
• 代数的演算同士の四則演算
  • α+βを根とする多項式を見つける
    • (α+β)^n が線形従属になるまで加える (いつかは線形従属になる)
  • 他にも根があるので除外する必要がある。αとβの区間から区間を割り出し。一意にならなければ狭めればよい
• 連立方程式の解き方 → グレブナ基底
• toRational :: a → Rational を実装しようがない(Haskellでは有理数より細かいものが考慮されてない？)
• 多項式の因数分解がボトルネック
  • Kronecker's method
  • 有限体やp進体で因数分解してから有理数体に展開 : Berlekampアルゴリズム。finite-field
  • 重根さえ除けばいいので、因数分解しなくてもいいかも
• パッケージング
  • 多項式を自前にするか既存のhackageにある何かを使えるのか
  • 実数に限らない代数的数も → スツルムの定理を使えない(Graeffe's Method?)
• 実閉体の決定可能性 (実数、代数的実数、などなど)
  • 順序体、奇数次の多項式は根、正の元は平方根
  • 論理式をどのモデルでも決定可能で、真偽が同じになる (自然数論ではそうならない)
• 量化子除去
  • 量化子を消せる (∃a, x^2+bx+c=0 を b^2-4ac >= 0 に変換)
  • 射影と実体の関係
  • Fourier-Motzkin、Cooper, OmegaTestなどのアルゴリズム
  • Tarskiのアルゴリズムは効率が悪い (non-elementary)
• CAD(Cylindrical Algebraic Decomposition)
  • double-exponentialで済む
• =,<,>のみを含み、頭に∃があるものを考える (これに帰着できる)
  • 一変数かつ線形の時: 各多項式の根を元に各区間での符号を考える。当てはまる区間があれば T に変換すれば終わり
  • 一変数かつ非線形 → 符号が等しくても根があるかもしれない
    • 微分したp'で区間分割しておけば
    • p mod qの符号を先に求めるために先に区間分割
    • 次数の低いものから区間分割
  • 多変数の場合 → 剰余がとれない。modの代わりにzmodを使う。
    • 最高次の場合分けが必要
• 量化子∃を一番右へ。∀は∃へ。これで帰着できる
• 結果は代数的実数で表現できる
• 単純化が必要 (BDD/ZDDで単純化したり)

Haskellは使わない計算不変式論 / @maophilia さん

• computation invariant theory
  • http://github.com/maophilia/invar
• 問題: ベクトル空間V上で不変な多項式を全部決定する => 生成元を決定する
• 例
  • 不変式の例: x + y + z、xy + yz + zx、xyzが生成元
  • 三角形の合同変換で不変な式6つ: 2角挟辺
  • 線形変換の不変量: trace
  • 二次曲線の分類
  • Grassman多様体
  • エンタングルメントの不変式論
• 生成元が有限とは限らない(が、有限なものに限定)
• 生成元が独立とは限らない → 消去イデアルの計算に帰着される
• Reynolds作用素: 群の作用と可換な射影作用素
• primary invariants: 独立な斉次不変式でdim(<p...>)=0のもの
  • 代数的独立や0次元性判定はグレブナー基底を用いてできる
• secondary invariants: primary invariantsで割れない単項式を基底にとってReynolds作用素を適用したものの中から探せる
• 線形独立な不変式の個数 → Hilbert級数で
• 代数群 SL(2) : 行列式が1の2行2列
• 線形簡約群に対して不変式環は有限生成
  • Hilbertイデアルを生成する斉次不変式をとれば不変式環の生成元が得られる
• Darksenイデアルの計算 → 代数群では直接計算できない
• Reynolds作用素の計算 → 完全なものはない
• ベンチマーク : n=4で2秒、n=5では30時間以上(あきらめ)
  • 19世紀の学者はn=6まで出しているので負けてる
  • Dixmierが1987年に解いた問題(Noetherは挫折したらしい)も、60時間かかっても解けない
  • 人間に負けてる・・・(汎用的過ぎて遅い)
• ボトルネックはグレブナー基底の計算

ツイートする

Permalink | コメント(0) | トラックバック(1) | 10:19