読者です 読者をやめる 読者になる 読者になる

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

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

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

せっかくの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>、円と直線の交点
    • 図形や連立方程式に関する計算が簡単にできる
  • 生成元
  • 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判定法
  • 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)で割れない
  • 被約グレブナー基底は、一意。イデアルが等しいかの判定にも使える
  • 最適化手法 → ナイーブな実装だと遅い。千倍くらい変わる
  • ゼロ簡約関係
    • 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 さん

  • 有理数係数多項式の根になっている実数
  • 多項式制約の解、演算、計算可能、数値誤差もない(定理証明では誤差は困る)
  • 多項式の根は複数 → 多項式だけでは根は得的できない
    • 多項式+根を1つ含む区間で表現する (表現は一意ではない)
    • AReal (UPolynomial ...) (Interval ...)
    • 有理数係数の最小多項式 (最高次係数 1、割れない)
  • 他の表現
    • 根の番号
    • 代数的実数係数の多項式とか(表現は簡単)
  • realRoots 根を全て求める
    • 因数分解して、
    • 根の限界を係数の絶対値で評価できる
    • スツルムの定理で根を数える
  • 演算: 近似値計算、比較、四則演算、代数的実数係数の根
    • 近似値 → スツルムの定理で絞り込める
    • EqとOrdの実装
      • 等号は多項式が等しく、範囲の重複部分に根があるとき
      • 不等号はスツルムの定理で追い込んで判定
  • 四則演算: 有理数との演算は、変数変換と区間演算で簡単
  • 代数的演算同士の四則演算
    • α+βを根とする多項式を見つける
      • (α+β)^n が線形従属になるまで加える (いつかは線形従属になる)
    • 他にも根があるので除外する必要がある。αとβの区間から区間を割り出し。一意にならなければ狭めればよい
  • 連立方程式の解き方 → グレブナ基底
  • toRational :: a → Rational を実装しようがない(Haskellでは有理数より細かいものが考慮されてない?)
  • 多項式因数分解ボトルネック
  • パッケージング
    • 多項式を自前にするか既存の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
  • 問題: ベクトル空間V上で不変な多項式を全部決定する => 生成元を決定する
    • 不変式の例: x + y + z、xy + yz + zx、xyzが生成元
    • 三角形の合同変換で不変な式6つ: 2角挟辺
    • 線形変換の不変量: trace
    • 二次曲線の分類
    • Grassman多様体
    • エンタングルメントの不変式論
  • 生成元が有限とは限らない(が、有限なものに限定)
  • 生成元が独立とは限らない → 消去イデアルの計算に帰着される
  • Reynolds作用素: 群の作用と可換な射影作用素
  • primary invariants: 独立な斉次不変式でdim(<p...>)=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時間かかっても解けない
    • 人間に負けてる・・・(汎用的過ぎて遅い)
  • ボトルネックグレブナー基底の計算

*1:これは自然数ベクトル上。項だと積

*2:単項式順序だと、割り算は止まる

*3:昔のコンピュータなら2桁で駄目なレベル