せっかくのGWなので、朝からHaskellで計算機代数勉強会に来ています。内容が内容なので正確性は保証できませんが、自分用のメモということで。
HALでもわかるGröbner基底 / @mr_konn さん
- グレブナー基底
- 体上多項式環のイデアルのよい生成元
- 体(たい): 四則演算ができる構造。整数はだめ(割り算が) k (ドイツ語だとケルパーらしい)
- 多項式環 k[x,y,...]。和、差、積がある。割り算はできるとは限らない
- イデアル: c∈Rに対してcx∈I。倍数の概念の一般化。
- 生成元
- <f1, ..., fn>で生成されるイデアルは、線形和
- 体上多項式環のイデアルは有限個のf1...frで書ける(ヒルベルトの基底定理)
- Noether環上の多項式環はNoether環である
- 性質がよい、とは？
- 多変数に一般化したい
- 1, x^2, xy, y^2 → 単項式
- 単項式順序(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
- 多項式版の割算を定義
- イデアルの元の先頭項が、基底の先頭項で生成される
- グレブナー基底は、簡約すると一意に決まる
- グレブナー基底の計算方法 : Buchbergerアルゴリズム
- S-多項式 → S(f, g) 先頭項同士を打ち消す
- Buchberger判定法
- 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)で割れない
- 被約グレブナー基底は、一意。イデアルが等しいかの判定にも使える
- 最適化手法 → ナイーブな実装だと遅い。千倍くらい変わる
- ゼロ簡約関係
- S-多項式はsyzygyの基底。syzygyとは先頭項を打ち消せるもの
- 余分な基底を予め除く
- 実装の改良 → STモナドを使う。先頭項を昇順に並べる(割り算を少なく)
- sugar strategy
- 基底の候補を選ぶ方法は自由
- normal strategy → LCMが最小のもの (lexなどはNG)
- sugar strategy → 斉次化次数(仮想的)なもの
- 斉次式 → 全ての次数が等しいもの(項を勝手に足す)。
- 最終結果に影響を与えないため仮想的にやる(sugar)
- selection strategy → 優先度キューの優先度として実現できる
- 論文に出て来る例については、sugar strategyは速い
- 並列での実装もあり、そちらだと非常に速いらしい(F4アルゴリズム。F5もあるらしい)
- computation-algebra パッケージでは依存型と証明のオンパレード
- DataKinds、GADTsなどを利用
- (haskel platformでは)外部ライブラリが使えなかったりもする
- イデアルはリストではない。sized-vectorにしている
- 帰納法はコストがかかる。(nとの比較、nステップかかる)
- シングルトンもコストがかかるので、依存型の実用はまだ厳しい
- 証明は実行時に遅延されてしまう
- GHC7.4.*では厳しい
グレブな基底の応用について / @ikegami__ さん
- 書籍
- アンケートの結果、初等幾何の自動証明の話をする
- 他、Computational Oriented Matroids (例がHaskellで書いてある)
- 数式処理 → シンボルに基づいた計算をコンピュータにさせる
- 数式処理の対象 → シンボルや代数。幾何は特殊
- 山本先生は、「学習過程とグレブナ基底は同じ」とおっしゃってる
- 初等幾何の自動証明
- 「自動」→証明をするわけではない
- 「初等幾何は、右脳と左脳を扱うのでいいらしい」
- 「コンピュータは計算をさせるものではなく、洞察を得るもの」
- 証明とは？ → 結論が前提から飛躍なく求められること
- グレブナ基底の発表。普通の人は15分しかない。
- 全てを解くのを諦める
- グレブナ基底による初等幾何
- 前提から制約を導出して、結論もあわせて多項式に変換(人間がやる)
- 前提と制約をすべて=0の形の方程式に。グレブナ基底が{1}なら常に満たされるという意味
- 問題点
- ウーの方法
- 擬除算、擬剰余 (グレブナー基底も忘れて解決する)
- おまけ: コンピュータの成長
- ピタゴラスの定理をコンピュータはわかるのか
- 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 さん
- 有理数係数多項式の根になっている実数
- 多項式制約の解、演算、計算可能、数値誤差もない(定理証明では誤差は困る)
- 多項式の根は複数 → 多項式だけでは根は得的できない
- 他の表現
- 根の番号
- 代数的実数係数の多項式とか(表現は簡単)
- realRoots 根を全て求める
- 因数分解して、
- 根の限界を係数の絶対値で評価できる
- スツルムの定理で根を数える
- 演算: 近似値計算、比較、四則演算、代数的実数係数の根
- 近似値 → スツルムの定理で絞り込める
- EqとOrdの実装
- 等号は多項式が等しく、範囲の重複部分に根があるとき
- 不等号はスツルムの定理で追い込んで判定
- 四則演算: 有理数との演算は、変数変換と区間演算で簡単
- 代数的演算同士の四則演算
- 連立方程式の解き方 → グレブナ基底
- toRational :: a → Rational を実装しようがない(Haskellでは有理数より細かいものが考慮されてない？)
- 多項式の因数分解がボトルネック
- パッケージング
- 多項式を自前にするか既存のhackageにある何かを使えるのか
- 実数に限らない代数的数も → スツルムの定理を使えない(Graeffe's Method?)
- 実閉体の決定可能性 (実数、代数的実数、などなど)
- 量化子除去
- CAD(Cylindrical Algebraic Decomposition)
- double-exponentialで済む
- =,<,>のみを含み、頭に∃があるものを考える (これに帰着できる)
- 量化子∃を一番右へ。∀は∃へ。これで帰着できる
- 結果は代数的実数で表現できる
- 単純化が必要 (BDD/ZDDで単純化したり)
Haskellは使わない計算不変式論 / @maophilia さん
- computation invariant theory
- 問題: ベクトル空間V上で不変な多項式を全部決定する => 生成元を決定する
- 例
- 生成元が有限とは限らない(が、有限なものに限定)
- 生成元が独立とは限らない → 消去イデアルの計算に帰着される
- 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時間かかっても解けない
- 人間に負けてる・・・(汎用的過ぎて遅い)
- ボトルネックはグレブナー基底の計算
