わかったつもりになる
Gröbner基底
石井 大海

13年5月4日土曜日

自己紹介
石井大海（a.k.a. @mr_konn）
Twitter: @mr_konn
Blog: http://blog.konn-san.com/
Web: http://konn-san.com/
Haskell lover
早稲田大学数学科四年
本当はロジックの人間の筈が今年は縁あって代数幾何（特に Gröbner 基底） の研究室にcomputational-algebra の作者

13年5月4日土曜日

Table of Contents
Gröbner 基底の簡単な導入
Gröbner 基底の計算法
Buchberger アルゴリズム
最適化手法：syzygy, sugar strategy
Haskell の型レベルプログラミングの現在

13年5月4日土曜日

Table of Contents
Gröbner 基底の簡単な導入
Gröbner 基底の計算法
Buchberger アルゴリズム
最適化手法：syzygy, sugar strategy
Haskell の型レベルプログラミングの現在

13年5月4日土曜日

Gröbner 基底 の簡単な導入

13年5月4日土曜日

Gröbner 基底の応用
高次連立方程式の文字消去
初等幾何の自動証明
統計にも何か応用があるらしい
ロボティクス
計算機代数、代数幾何学

13年5月4日土曜日

Gröbner 基底

13年5月4日土曜日

Gröbner 基底“グレブナーきてい” と読む

13年5月4日土曜日

Gröbner 基底“グレブナーきてい” と読む1960s: 廣中平祐、B. Buchberger らが独立に発見

13年5月4日土曜日

Gröbner 基底“グレブナーきてい” と読む1960s: 廣中平祐、B. Buchberger らが独立に発見
Gröbner は Buchberger の師匠の名前

13年5月4日土曜日

Gröbner 基底“グレブナーきてい” と読む1960s: 廣中平祐、B. Buchberger らが独立に発見
Gröbner は Buchberger の師匠の名前
廣中は特異点解消のために考えた

13年5月4日土曜日

Gröbner 基底“グレブナーきてい” と読む1960s: 廣中平祐、B. Buchberger らが独立に発見
Gröbner は Buchberger の師匠の名前
廣中は特異点解消のために考えた技術の進歩で計算出来るようになり応用が出る

13年5月4日土曜日

Gröbner 基底“グレブナーきてい” と読む1960s: 廣中平祐、B. Buchberger らが独立に発見
Gröbner は Buchberger の師匠の名前
廣中は特異点解消のために考えた技術の進歩で計算出来るようになり応用が出る
体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

？？？

13年5月4日土曜日

体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

体
たい（≠からだ）と読む
足し算、引き算、掛け算、割り算（0以外）が出きるよ
うな構造
例：有理数体 ℚ とか複素数体 ℂ とか
例：整数全体 ℤ は体でない（1/2は整数じゃない）
以下では小文字の k で体を表す

13年5月4日土曜日

体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

体上の多項式環
k[X1, …, Xn] = {k を係数とする n-変数多項式全体}
変数の数が自明な時は k[𝕏] = k[X1, …, Xn] と書く
自然に足し算、引き算、掛け算が定義できる（割り算は出来るとは限らない）

例：X12 + 2 X1X2 + X22 ∈ k[X1, X2], y2 − x ∈ k[x, y]

13年5月4日土曜日

体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

イデアル
定義
環 R の部分集合 I が イデアル であるとは
1. 任意の x, y ∈ I について x − y ∈ I
2.任意の c ∈ R, x ∈ I について cx ∈ I

倍数概念の或る種の一般化になっている
イデアル I に属する ⇔ I の元で割れる
a が b の倍数 ⇔ ⟨a⟩ ⊆ ⟨b⟩

13年5月4日土曜日

なぜイデアル？

13年5月4日土曜日

なぜイデアル？
イデアルは幾何的にはその零点の成す図形と対応する（正確には根基イデアルが対応）

13年5月4日土曜日

なぜイデアル？
イデアルは幾何的にはその零点の成す図形と対応する（正確には根基イデアルが対応）⟨y − x2⟩：放物線

13年5月4日土曜日

なぜイデアル？
イデアルは幾何的にはその零点の成す図形と対応する（正確には根基イデアルが対応）⟨y − x2⟩：放物線⟨y2 + x2 − 1, y + 2x − 1⟩：円と直線の交点

13年5月4日土曜日

なぜイデアル？
イデアルは幾何的にはその零点の成す図形と対応する（正確には根基イデアルが対応）⟨y − x2⟩：放物線⟨y2 + x2 − 1, y + 2x − 1⟩：円と直線の交点
交点

13年5月4日土曜日

連立方程式の解

なぜイデアル？
イデアルは幾何的にはその零点の成す図形と対応する（正確には根基イデアルが対応）⟨y − x2⟩：放物線⟨y2 + x2 − 1, y + 2x − 1⟩：円と直線の交点
交点

連立方程式の解イデアルは連立された関係式とも見ることが出来る

13年5月4日土曜日

なぜイデアル？
イデアルは幾何的にはその零点の成す図形と対応する（正確には根基イデアルが対応）⟨y − x2⟩：放物線⟨y2 + x2 − 1, y + 2x − 1⟩：円と直線の交点
交点

連立方程式の解イデアルは連立された関係式とも見ることが出来る
Gröbner 基底を使うと色んな図形・連立方程式に関する計算が簡単に出来るようになる

13年5月4日土曜日

体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

生成元定義
f1, … , fr ∈ k[𝕏 ] について、⟨f1,…, fr⟩ := {a1 f1 +…+ ar fr ∣ ai ∈ k[𝕏] (i = 1, …r)}を f1,…, fr により生成されるイデアルという。
I = ⟨f1,…, fr⟩ の時、 f1,…, fr を I の基底、または生成元と呼ぶ。
上の ⟨f1,…, fr⟩ はさっきのイデアルの定義を満たす。
逆に、体上多項式環のイデアルは、適当な f1,…, fr により、すべてこの形で書ける（Hilbert の基底定理）
13年5月4日土曜日

Hilbert の基底定理
定理
Noether 環上の多項式環は Noether 環である

13年5月4日土曜日

Hilbert の基底定理
定理
Noether 環上の多項式環は Noether 環である

Noether 環とは「任意のイデアルが有限個の生成元で書ける（＝有限生成）」という条件を満たす環

13年5月4日土曜日

Hilbert の基底定理
定理
Noether 環上の多項式環は Noether 環である

Noether 環とは「任意のイデアルが有限個の生成元で書ける（＝有限生成）」という条件を満たす環計算機で扱うには、多項式環のイデアルは有限個の多項式の組として定義すれば十分

13年5月4日土曜日

Hilbert の基底定理
定理
Noether 環上の多項式環は Noether 環である

Noether 環とは「任意のイデアルが有限個の生成元で書ける（＝有限生成）」という条件を満たす環計算機で扱うには、多項式環のイデアルは有限個の多項式の組として定義すれば十分
証明はむずかしいが、体の場合については Gröbner 基底を使うと簡単に示せる。
（証明：Gröbner 基底を取ればよい■）

13年5月4日土曜日

体上多項式環のイデアルの性質のよい生成元

13年5月4日土曜日

よい性質？
問題 1
f1 = x3 + x2 + x + 1
f2 = x 2 − x − 2
I = ⟨ f1, f2 ⟩ ⊆ k[x]とすると、g = x − 1,3

h = x + 1 はそれぞれ2

I に属すか？

13年5月4日土曜日

左の問題を考える

f1 と f2 の “最大公約式”

f = GCD(f1, f2) がわ
かればよい

I = ⟨ f ⟩ となるので、あとは g, h を f で割り切れるか見る

最大公約式の求め方
Euclid の互除法を使う
整数だけでなく、割り算原理が成立する任意の環で使える
整数の場合：ある元が ⟨a, b⟩ に属する
a, b で割れる
a, b の最大公約数で割れる
同様のことが一変数多項式環でも成立

13年5月4日土曜日

Euclid の互除法
入力：f, g
1. f を g で割り算した余りを r0とする
2. g を r0 で割り算した余りを r1 とする
3. r0 を r1 で割り算した余りを r2 とする
4.以下ゼロになるまで繰り返し
出力：ゼロでない最後の rn

13年5月4日土曜日

一変数多項式の割り算
先程の問題で Euclidのx +2互除法を使うときの最初のステップx

23

2x 2 x +x+x +1

x3 x2 2x降冪の順に並べる

2x2 +3x +1
2x2 2x 4

大きい項との帳尻を合わせていく

13年5月4日土曜日

5x +5これを多変数に一般化できないか？

13年5月4日土曜日

多変数の場合13年5月4日土曜日

多変数の場合
問題 2
f1 = X2Y − 1
f 2 = X3 − Y2 − X
I = ⟨ f1, f2 ⟩ ⊆ k[X, Y]とすると、
g = X2Y2 − X3Y − XY − 1
は I に属すか？

13年5月4日土曜日

多変数の場合
問題 2
f1 = X2Y − 1
f 2 = X3 − Y2 − X
I = ⟨ f1, f2 ⟩ ⊆ k[X, Y]とすると、
g = X2Y2 − X3Y − XY − 1
は I に属すか？

13年5月4日土曜日

二変数の場合を考える

多変数の場合
問題 2
f1 = X2Y − 1
f 2 = X3 − Y2 − X
I = ⟨ f1, f2 ⟩ ⊆ k[X, Y]とすると、
g = X2Y2 − X3Y − XY − 1
は I に属すか？

13年5月4日土曜日

二変数の場合を考える

f1 と f2 の “最大公約式”のような物を考えられるか？

多変数の場合
問題 2
f1 = X2Y − 1
f 2 = X3 − Y2 − X
I = ⟨ f1, f2 ⟩ ⊆ k[X, Y]とすると、
g = X2Y2 − X3Y − XY − 1
は I に属すか？

13年5月4日土曜日

二変数の場合を考える

f1 と f2 の “最大公約式”のような物を考えられるか？

➡ 出来ない！

最大公約式は取れない

13年5月4日土曜日

最大公約式は取れない
最大公約式が必ず取れるなら、任意のイデア
ルは一つの多項式により⟨ f ⟩ の形で書ける

13年5月4日土曜日

最大公約式は取れない
最大公約式が必ず取れるなら、任意のイデア
ルは一つの多項式により⟨ f ⟩ の形で書ける
しかし、例えば⟨x, y⟩について上のような fは存在しない！

13年5月4日土曜日

最大公約式は取れない
最大公約式が必ず取れるなら、任意のイデア
ルは一つの多項式により⟨ f ⟩ の形で書ける
しかし、例えば⟨x, y⟩について上のような fは存在しない！
別の手段を考えるべし

13年5月4日土曜日

最大公約式は取れない
最大公約式が必ず取れるなら、任意のイデア
ルは一つの多項式により⟨ f ⟩ の形で書ける
しかし、例えば⟨x, y⟩について上のような fは存在しない！
別の手段を考えるべし
割り算の余りが重要だった

13年5月4日土曜日

最大公約式は取れない
最大公約式が必ず取れるなら、任意のイデア
ルは一つの多項式により⟨ f ⟩ の形で書ける
しかし、例えば⟨x, y⟩について上のような fは存在しない！
別の手段を考えるべし
割り算の余りが重要だった➡ 割り算を一般化してみよう！
13年5月4日土曜日

割り算の一般化

13年5月4日土曜日

割り算の一般化
複数の多項式で一つの多項式を割ろう！
多項式を並べておいて順に割れないか試す
一変数多項式の場合の降冪の順のように、何か都合のよい並べ方を考える必要がある

13年5月4日土曜日

割り算の一般化
複数の多項式で一つの多項式を割ろう！
多項式を並べておいて順に割れないか試す
一変数多項式の場合の降冪の順のように、何か都合のよい並べ方を考える必要がある➡ 単項式順序！

13年5月4日土曜日

多項式の表現13年5月4日土曜日

多項式の表現
単項式順序の前に、多項式の表現について

13年5月4日土曜日

多項式の表現
単項式順序の前に、多項式の表現について
2

2

文字と指数の列（1, x , xy, y など）を単項式といい、それぞれに係数を書けて加えたものを多項式と呼ぶのだった

13年5月4日土曜日

多項式の表現
単項式順序の前に、多項式の表現について
2

2

文字と指数の列（1, x , xy, y など）を単項式といい、それぞれに係数を書けて加えたものを多項式と呼ぶのだった
文字の間に順番を決めれば、単項式は整数のベクトルと同一視出来る

13年5月4日土曜日

多項式の表現
単項式順序の前に、多項式の表現について
2

2

文字と指数の列（1, x , xy, y など）を単項式といい、それぞれに係数を書けて加えたものを多項式と呼ぶのだった
文字の間に順番を決めれば、単項式は整数のベクトルと同一視出来る

x > y とすれば、x2 ↔ (2, 0), xy ↔ (1, 1),
1 ↔ (0, 0) と言う具合に対応する

13年5月4日土曜日

多項式の表現
単項式順序の前に、多項式の表現について
2

2

文字と指数の列（1, x , xy, y など）を単項式といい、それぞれに係数を書けて加えたものを多項式と呼ぶのだった
文字の間に順番を決めれば、単項式は整数のベクトルと同一視出来る

x > y とすれば、x2 ↔ (2, 0), xy ↔ (1, 1),
1 ↔ (0, 0) と言う具合に対応する
そこで n-変数単項式全体をℤn≥0 と同一視する

13年5月4日土曜日

単項式順序定義

13年5月4日土曜日

単項式順序定義ℤn≥0 上の順序関係 > は、次の三つの条件を満たすとき単項式順序であると言う：

13年5月4日土曜日

単項式順序定義ℤn≥0 上の順序関係 > は、次の三つの条件を満たすとき単項式順序であると言う：
1. 全順序性： (α < β) or (α = β) or (α > β)

13年5月4日土曜日

単項式順序定義ℤn≥0 上の順序関係 > は、次の三つの条件を満たすとき単項式順序であると言う：
1. 全順序性： (α < β) or (α = β) or (α > β)2.加法性：α ≤ β ⇒ α + γ ≤ β + γ

13年5月4日土曜日

単項式順序定義ℤn≥0 上の順序関係 > は、次の三つの条件を満たすとき単項式順序であると言う：
1. 全順序性： (α < β) or (α = β) or (α > β)2.加法性：α ≤ β ⇒ α + γ ≤ β + γ
3.非負性：α ≥ 0 (任意の α ∈ ℤn≥0 について)

13年5月4日土曜日

単項式順序の補足

13年5月4日土曜日

単項式順序の補足
3 の非負性の条件は、全順序性と加法性の下で以下の二つと同値

13年5月4日土曜日

単項式順序の補足
3 の非負性の条件は、全順序性と加法性の下で以下の二つと同値
整列性：任意の空でない ℤn≥0 の部分集合が< に関して最小値を持つ

13年5月4日土曜日

単項式順序の補足
3 の非負性の条件は、全順序性と加法性の下で以下の二つと同値
整列性：任意の空でない ℤn≥0 の部分集合が< に関して最小値を持つ

降鎖条件： > に関する無限下降列" " " α0 > α1 > α2 > ⋯ > αn > ⋯は存在しない

13年5月4日土曜日

単項式順序の補足
3 の非負性の条件は、全順序性と加法性の下で以下の二つと同値
整列性：任意の空でない ℤn≥0 の部分集合が< に関して最小値を持つ

降鎖条件： > に関する無限下降列" " " α0 > α1 > α2 > ⋯ > αn > ⋯は存在しないこれらは、アルゴリズムの停止性の証明で使う

13年5月4日土曜日

単項式順序の例
以下 α = (a1, …, an), β = (b1, …, bn) とする
辞書式順序 >lex は単項式順序

α >lex β :⟺ a1 = b1, …, ai−1 = bi−1, ai > bi
逆辞書式順序 >revlex は単項式順序でない
α >revlex β :⟺ ai+1 = bi+1, …, an = bn, ai < bi（※最後の不等号の向きに注意！）

13年5月4日土曜日

単項式順序の例
次数付き辞書式順序 >grlex は単項式順序

α >grlex β :⟺ ∣α∣ > ∣β∣ or (∣α∣=∣β∣ and α >lex β)
ただし ∣α∣ = a1 + ⋯ + an（全次数）次数付き逆辞書式順序 >grevlex は単項式順序
α >grevlex β :⟺ ∣α∣>∣β∣ or (∣α∣=∣β∣ and α >revlex β)

13年5月4日土曜日

約束
単項式順序 > を固定する。多項式 f に現れる
（係数抜きの）単項式の中で、> について最大となるものを先頭単項式と云い、LM(f) で表す。LM(f) の係数を先頭係数といい、LC(f)で表す。LT(f) = LC(f) LM(f) を先頭項と呼ぶ。

13年5月4日土曜日

例
f = x + 2y2w + 3z3 (x > y > z >w)>lex ：LM(f) = x, LC(f) = 1, LT(f) = x>grlex：LM(f) = y2w, LC(f) = 2, LT(f) = 2y2w
>grevlex：LM(f) = z3, LC(f) = 3, LT(f) = 3z3

13年5月4日土曜日

多変数の割り算
以上を用いて多項式版の割り算を定義する
単項式順序を一つ決め、割る式、割られる式
ともに大きい単項式順に整列しておく
どの順番で割るかは固定する！

13年5月4日土曜日

実例：多変数の割り算
a1 =
a2 =

XY − 1 X2Y + XY2 + Y2
Y2 − 1XY − 1, Y2 − 1 で X2Y + XY2 + Y2 を割る。辞書式順序を使う。

13年5月4日土曜日

実例：多変数の割り算
a1 =
a2 =

XY − 1 X2Y + XY2 + Y2
Y2 − 1

先頭項に注目。最初の式で割れる
13年5月4日土曜日

実例：多変数の割り算
a1 = Xa2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X

X を掛ければ先頭項が消える。
13年5月4日土曜日

実例：多変数の割り算
a1 = Xa2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X
XY2 + X引く。
13年5月4日土曜日

実例：多変数の割り算
a1 = Xa2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X
XY2 + X + Y2

上から一つ降ろして、降冪の順に並べる
13年5月4日土曜日

実例：多変数の割り算
a1 = X +a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X
XY2 + X + Y2

先頭項に注目。 XY − 1 で割れる。
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X
XY2 + X + Y2
XY2 − YX + Y2 + Y

先程と同様に計算。
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X
XY2 + X + Y2
XY2 − YX + Y2 − Y

先頭項に注目。XY, Y2 どちらでも割れない。
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X

1

XY2 + X + Y2
XY2 − YX + Y2 − YX

Y2 − Y

割れないので X は余りとして横によける
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X

1

XY2 + X + Y2
XY2 − YX + Y2 − YX

Y2 − Y

先頭項に注目。 XY は無理だ
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X

1

XY2 + X + Y2
XY2 − YX + Y2 − YX

Y2 − YY2 − 1

Y+1

Y2 で割れるので、割る。
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X

1

XY2 + X + Y2
XY2 − YX + Y2 − Y
Y2 − YY2 − 1

Y+1

1
0

X

Y

1

Y, 1 共にどの項でも割れないので横によける
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X

1

XY2 + X + Y2
XY2 − YX + Y2 − Y
Y2 − YY2 − 1

Y+1

1
0

X

Y

1

r = X+Y+1

よけたのを足して、余り r が出る
13年5月4日土曜日

実例：多変数の割り算
a1 = X + Y
a2 =XY − 1 X2Y + XY2 + Y2
Y2 − 1 X2Y − X

1

XY2 + X + Y2
XY2 − YX + Y2 − Y
Y2 − YY2 − 1

Y+1

1
0

X

Y

1

r = X+Y+1

X2Y + XY2 + Y2 = (XY − 1) (X+Y) + (Y2 − 1) ⋅1 + X + Y + 1
13年5月4日土曜日

多変数割り算

これでいいのでは……！？
ところが、 あまり 嬉しくないことが……

13年5月4日土曜日

あまり の問題
a1 =a2 =Y2 − 1 X2Y + XY2 + Y2
XY − 1

割る順番を変え、Y2 − 1, XY − 1で X2Y + XY2 + Y2 を割る。
13年5月4日土曜日

余りの問題
a1 =
a2 =

X

X

+1

Y2 − 1 X2Y + XY2 + Y2
XY − 1 X2Y − X
XY2 + X + Y2
XY2 − X
2X + Y2

Y2
Y2 − 1

1
0

2X
1
r = 2X + 1

X2Y + XY2 + Y2 = (XY − 1) X + (Y2 − 1)(X + 1) + 2X + 1

13年5月4日土曜日

余りが違う！

13年5月4日土曜日

余りが違う！
多項式の割り算は 割る順番で余りが変わる！

13年5月4日土曜日

余りが違う！
多項式の割り算は 割る順番で余りが変わる！
単に「割って余りゼロ イデアルに入る！」とは出来ない！

13年5月4日土曜日

余りが違う！
多項式の割り算は 割る順番で余りが変わる！
単に「割って余りゼロ イデアルに入る！」とは出来ない！
与えられたイデアルに対して、割り算の余りが順番に依らないような生成元を取れないか？

13年5月4日土曜日

余りが違う！
多項式の割り算は 割る順番で余りが変わる！
単に「割って余りゼロ イデアルに入る！」とは出来ない！
与えられたイデアルに対して、割り算の余りが順番に依らないような生成元を取れないか？

➡ Gröbner 基底！
13年5月4日土曜日

Gröbner 基底
定義
単項式順序 > を一つ固定する。多項式環のイデア

ル I ⊆ k[𝕏] について、I の有限部分集合 G = {g1, …,gn} ⊆ I が次の条件を満たすとき、G は > に関する I の Gröbner 基底 であると言う。

⟨LT(I)⟩ = ⟨LT(g1), …, LT(gn)⟩(i.e. ⟨LT(f) ∣ f ∈ I ⟩ = ⟨LT(g1), …, LT(gn)⟩)

13年5月4日土曜日

Gröbner 基底の性質
定理

13年5月4日土曜日

Gröbner 基底の性質
定理
任意の多項式環イデアルに対し Gröbner 基底が存在する

13年5月4日土曜日

Gröbner 基底の性質
定理
任意の多項式環イデアルに対し Gröbner 基底が存在する
イデアル I の Gröbner 基底 G = {g1, …, gk} は I を生成する。即ち、I = ⟨g1, …, gk⟩

13年5月4日土曜日

Gröbner 基底の性質
定理
任意の多項式環イデアルに対し Gröbner 基底が存在する
イデアル I の Gröbner 基底 G = {g1, …, gk} は I を生成する。即ち、I = ⟨g1, …, gk⟩
Gröbner 基底による割り算の余りは順番に依らない。

13年5月4日土曜日

Gröbner 基底の性質
定理
任意の多項式環イデアルに対し Gröbner 基底が存在する
イデアル I の Gröbner 基底 G = {g1, …, gk} は I を生成する。即ち、I = ⟨g1, …, gk⟩
Gröbner 基底による割り算の余りは順番に依らない。
Gröbner 基底で割った余りがゼロである事と I に属することは同値： r = f G̅ =0⟺f∈I

13年5月4日土曜日

まとめ
Gröbner 基底は体上多項式環のイデアルの良い性質を持った生成元
単項式順序を決めると計算出来る
割り算の余りが順番に依らない
イデアル所属問題に使える
他にも応用多数

13年5月4日土曜日

ここまでで質問？

13年5月4日土曜日

Table of Contents
Gröbner 基底の簡単な導入
Gröbner 基底の計算法
Buchberger アルゴリズム
最適化手法：syzygy, sugar strategy
Haskell の型レベルプログラミングの現在

13年5月4日土曜日

Gröbner 基底の計算法

13年5月4日土曜日

Buchberger アルゴリズム

13年5月4日土曜日

Buchberger アルゴリズム
Gröbner 基底が便利そうなのはわかった

13年5月4日土曜日

Buchberger アルゴリズム
Gröbner 基底が便利そうなのはわかった
具体的な計算法：Buchberger アルゴリズム

13年5月4日土曜日

Buchberger アルゴリズム
Gröbner 基底が便利そうなのはわかった
具体的な計算法：Buchberger アルゴリズム
準備的な定義：f, g ∈ k[𝕏] の S-多項式

13年5月4日土曜日

Buchberger アルゴリズム
Gröbner 基底が便利そうなのはわかった
具体的な計算法：Buchberger アルゴリズム
準備的な定義：f, g ∈ k[𝕏] の S-多項式

S(f, g) :=13年5月4日土曜日

LCM(LT(f), LT(g))
LCM(LT(f), LT(g))
f−
g
LT(f)
LT(g)

Buchberger アルゴリズム
Gröbner 基底が便利そうなのはわかった
具体的な計算法：Buchberger アルゴリズム
準備的な定義：f, g ∈ k[𝕏] の S-多項式

S(f, g) :=LCM(LT(f), LT(g))
LCM(LT(f), LT(g))
f−
g
LT(f)
LT(g)

f, g の先頭項同士を打消し合わせた物

13年5月4日土曜日

Buchberger アルゴリズム
Gröbner 基底が便利そうなのはわかった
具体的な計算法：Buchberger アルゴリズム
準備的な定義：f, g ∈ k[𝕏] の S-多項式

S(f, g) :=LCM(LT(f), LT(g))
LCM(LT(f), LT(g))
f−
g
LT(f)
LT(g)

f, g の先頭項同士を打消し合わせた物
ただし LCM((a1, …, an), (b1, …, bn)):= (max{a1, b1}, …, max{an, bn})

13年5月4日土曜日

Buchberger 判定法
定理
I ⊆ k[𝕏]：イデアル>：単項式順序G = {g1, …, gk} ⊆ I：I の生成元
G’ = (g1, …, gk)：G の元を適当に並べたもの
このとき以下の二つは同値：
1. G は > に関する I の Gröbner 基底2.S(gi, gk)G’ = 0

13年5月4日土曜日(∀ i < j)Buchberger アルゴリズム
入力：G = (f1, …, fs)

R ← {S(p, q)G’ ∣ p ≠ q ∈ G} \ {0}R≠∅

G ← (G, R)

出力：G
13年5月4日土曜日

R=∅簡単な実装buchberger :: [Polynomial k ord n] → [Polynomial k ord n]
buchberger ideal =fst $ until (null ∘ snd) loop (ideal, calc ideal)
whereloop (ggs, acc) =let cur = nub $ ggs ++ acc
in (cur, calc cur)calc acc =[ q | f ← acc, g ← acc, f ≠ g, let q = sPolynomial f g `mod` acc, q ≠ zero]

13年5月4日土曜日

計算例

13年5月4日土曜日

計算例
I = ⟨x2y − 1, x3 − y2 − x⟩ の Gröbner 基底

13年5月4日土曜日

計算例
I = ⟨x2y − 1, x3 − y2 − x⟩ の Gröbner 基底
Grevlex で計算
G = {x2y − 1, x3 − y2 − x, y3 + xy − x, − y3 − xy + x}

13年5月4日土曜日

計算例
I = ⟨x2y − 1, x3 − y2 − x⟩ の Gröbner 基底
Grevlex で計算
G = {x2y − 1, x3 − y2 − x, y3 + xy − x, − y3 − xy + x}
割る順番で答えが変わらないことは、まあ、確
かめといてください。

13年5月4日土曜日

lex で計算すると？

13年5月4日土曜日

lex で計算すると？
G = {x2y − 1, x3 − y2 − x, y3 + xy − x, − y3 − xy + x, y5 + y4 +y3 + x2 − x − 1, − y5 − y4 − y3 − x2 + x + 1, − y6 − y5 − y4 −y3 + x + y − 1, y7 + 2y6 + 2y5 + 2y4 + 2y3 − y2 − 2x + 1, y6 +y5 + y4 + y3 − x − y + 1, − y7 − 2y6 − 2y5 − 2y4 − 2y3 + y2 +2x − 1, − y9 − 2y8 − 3y7 + y4 − 4y + 3, − 1 / 2y10 − 3 / 2y9 −5 / 2y8 − 7 / 2y7 + 1 / 2y5 + 1 / 2y4 − 9 / 2y + 7 / 2, y7 − y2 + 2y
− 1, 1 / 2y8 + y7 − 1 / 2y3 + 3 / 2y − 1, − y7 + y2 − 2y + 1, −y8 − 2y7 + y3 − 3y + 2, − 1 / 2y9 − 3 / 2y8 − 5 / 2y7 + 1 / 2y4 +1 / 2y3 − 7 / 2y + 5 / 2, y9 + 2y8 + 3y7 − y4 + 4y − 3, y8 + 2y7 −y3 + 3y − 2, 1 / 2y7 − 1 / 2y2 + y − 1 / 2, 1 / 2y10 + 3 / 2y9 + 5 /2y8 + 7 / 2y7 − 1 / 2y5 − 1 / 2y4 + 9 / 2y − 7 / 2, − 1 / 2y8 − y7
+ 1 / 2y3 − 3 / 2y + 1, 1 / 2y9 + 3 / 2y8 + 5 / 2y7 − 1 / 2y4 − 1 /2y3 + 7 / 2y − 5 / 2, − 1 / 2y7 + 1 / 2y2 − y + 1 / 2}

13年5月4日土曜日

でかっ！

13年5月4日土曜日

効率の問題Grevlex が一番速くて基底も綺麗なものが求まりやすいとされる
lex は基底も複雑になるし時間がかかる物によっては Grevlex の方が遅いこともある
が、ほぼ大抵は Grevlex が圧倒的に速い
応用分野によっては grevlex ではなく lex を使う

13年5月4日土曜日

極小・被約Gröbner基底

13年5月4日土曜日

極小・被約Gröbner基底
Buchberger アルゴリズムで求めた基底には無駄がある

13年5月4日土曜日

極小・被約Gröbner基底
Buchberger アルゴリズムで求めた基底には無駄がある
極小・被約 Gröbner 基底！

13年5月4日土曜日

極小・被約Gröbner基底
Buchberger アルゴリズムで求めた基底には無駄がある
極小・被約 Gröbner 基底！
Gröbner基底 G が極小 ⇔ 任意の i についてLC(gi) = 1, LT(gi) はどの LT(gj) (j ≠ i) でも割れない

13年5月4日土曜日

極小・被約Gröbner基底
Buchberger アルゴリズムで求めた基底には無駄がある
極小・被約 Gröbner 基底！
Gröbner基底 G が極小 ⇔ 任意の i についてLC(gi) = 1, LT(gi) はどの LT(gj) (j ≠ i) でも割れない
G が被約 ⇔ 任意の i について LC(gi) = 1 かつ
gi のどの項も LT(gj) (j ≠ i) でも割れない

13年5月4日土曜日

被約 Gröbner 基底の一意性

13年5月4日土曜日

被約 Gröbner 基底の一意性
Gröbner 基底は複数存在しうる13年5月4日土曜日

被約 Gröbner 基底の一意性
Gröbner 基底は複数存在しうる
buchberger で求めた物、その極小化……etc

13年5月4日土曜日

被約 Gröbner 基底の一意性
定理
Gröbner 基底は複数存在しうる
buchberger で求めた物、その極小化……etc

I ⊆ k[𝕏]：イデアル>：単項式順序

それらは被約化すれば一致する！（単項式順序が同じなら）

I の > についての被約 Gröbner 基底は一
意に定まる

13年5月4日土曜日

被約 Gröbner 基底の一意性
定理
Gröbner 基底は複数存在しうる
buchberger で求めた物、その極小化……etc

I ⊆ k[𝕏]：イデアル>：単項式順序

それらは被約化すれば一致する！（単項式順序が同じなら）

I の > についての被イデアルが等しいかどうかを、

約 Gröbner 基底は一意に定まる

被約 Gröbner 基底の生成元が等しいかで判定出来る！

13年5月4日土曜日

被約化の手続13年5月4日土曜日

被約化の手続
まず極小化を行う
1. G の各元を最高次係数で割って LC(p) = 1
2. (2) の条件を満たさない物を取り除く

13年5月4日土曜日

被約化の手続
まず極小化を行う
1. G の各元を最高次係数で割って LC(p) = 1
2. (2) の条件を満たさない物を取り除く
それを被約化する
1. p ∈ G を取り、p’ = p̅G \ {p}, G’ = G \ {p} ∪ {p’} とする
2. q ∈ G’ \ {p’} について同様の事をする。以下同文。

13年5月4日土曜日

計算例

13年5月4日土曜日

計算例
先程のイデアルについて

13年5月4日土曜日

計算例
先程のイデアルについて
Grevlex に関する被約基底

G = {y3 + xy − x, x2y − 1, x3 − y2 − x}

13年5月4日土曜日

計算例
先程のイデアルについて
Grevlex に関する被約基底

G = {y3 + xy − x, x2y − 1, x3 − y2 − x}Lex に関する被約基底
G = {y7 − y2 + 2y − 1, − y6 − y5 − y4 − y3 + x+ y − 1}

13年5月4日土曜日

計算例
先程のイデアルについて
Grevlex に関する被約基底

G = {y3 + xy − x, x2y − 1, x3 − y2 − x}Lex に関する被約基底
G = {y7 − y2 + 2y − 1, − y6 − y5 − y4 − y3 + x+ y − 1}
うわっ…ナイーブな基底、無駄多すぎ…？

13年5月4日土曜日

計算例
先程のイデアルについて
Grevlex に関する被約基底

G = {y3 + xy − x, x2y − 1, x3 − y2 − x}Lex に関する被約基底
G = {y7 − y2 + 2y − 1, − y6 − y5 − y4 − y3 + x+ y − 1}
うわっ…ナイーブな基底、無駄多すぎ…？
最初から被約グレブナー基底を産むアルゴリズ
ムもある
13年5月4日土曜日

実装例
minimizeGroebnerBasis :: (Field k, IsPolynomial k n, IsMonomialOrder order)⇒ [OrderedPolynomial k ord n] → [OrderedPolynomial k ord n]
minimizeGroebnerBasis bs = runST $ doleft ← newSTRef bs
right ← newSTRef []whileM_ (not . null <$> readSTRef left) $ dof : xs ← readSTRef left
writeSTRef left xs
ys← readSTRef right
if any (λg → leadingMonomial g `divs` leadingMonomial f) xs ∨any (λg → leadingMonomial g `divs` leadingMonomial f) ys
then writeSTRef right yselse writeSTRef right (monoize f : ys)
readSTRef right

適宜アップデートする必要があるので ST で楽して書いた
被約化の実装も同様
13年5月4日土曜日

Table of Contents
Gröbner 基底の簡単な導入
Gröbner 基底の計算法
Buchberger アルゴリズム
最適化手法：syzygy, sugar strategy
Haskell の型レベルプログラミングの現在

13年5月4日土曜日

最適化手法
ナイーブな実装だと遅い！
代表的な実装である SINGULAR の千倍くらい遅い（推定）
何とか百倍くらいにする方法
指数オーダーなので〜倍っていう表現はおかしいのだけど・・・

13年5月4日土曜日

紹介する手法

ゼロ簡約関係
syzygy の基底
sugar strategy

13年5月4日土曜日

紹介する手法

ゼロ簡約関係
syzygy の基底
sugar strategy

13年5月4日土曜日

ゼロ簡約関係13年5月4日土曜日

ゼロ簡約関係
Buchberger は何故遅い？

13年5月4日土曜日

ゼロ簡約関係
Buchberger は何故遅い？
Buchberger は割り算のかたまり

13年5月4日土曜日

ゼロ簡約関係
Buchberger は何故遅い？
Buchberger は割り算のかたまり
lex より grevlex が速いのは、そっちのほうが割り算のステップが小さいから

13年5月4日土曜日

ゼロ簡約関係
Buchberger は何故遅い？
Buchberger は割り算のかたまり
lex より grevlex が速いのは、そっちのほうが割り算のステップが小さいから割り算の回数をもっと減らせない？

13年5月4日土曜日

ゼロ簡約関係「割って余りゼロ」を一般化したのが次13年5月4日土曜日

ゼロ簡約関係「割って余りゼロ」を一般化したのが次

定義
多項式 f ∈ k[𝕏] が G = {g1, …, gk} ⊆ k[𝕏] を法としてゼロに簡約（記号： f →G 0）される⇔ f = a1g1 + ⋯ + akgk (ai ∈ k[𝕏]) かつ[aigi = 0 または deg(f) ≥ deg(aigi)]
但し、deg(f) は f の多重次数 deg(f) = LM(f)13年5月4日土曜日

改良 Buchberger 判定法
実は Buchberger 判定法はゼロ簡約で十分！

13年5月4日土曜日

改良 Buchberger 判定法
実は Buchberger 判定法はゼロ簡約で十分！

定理
I ⊆ k[𝕏]：イデアル>：単項式順序G = {g1, …, gk} ⊆ I：I の生成元
このとき以下の二つは同値：
1. G は > に関する I の Gröbner 基底
2. S(gi, gj) →G 0
13年5月4日土曜日(∀ i < j)具体的にいつゼロ簡約？
命題I ⊆ k[𝕏]：イデアル>：単項式順序G = {g1, …, gk} ⊆ I：I の生成元

13年5月4日土曜日

具体的にいつゼロ簡約？
命題I ⊆ k[𝕏]：イデアル>：単項式順序G = {g1, …, gk} ⊆ I：I の生成元S̅(f̅, ̅g̅)G’̅ = 0 ⇒ S(f, g) →G 0

13年5月4日土曜日

具体的にいつゼロ簡約？
命題I ⊆ k[𝕏]：イデアル>：単項式順序G = {g1, …, gk} ⊆ I：I の生成元S̅(f̅, ̅g̅)G’̅ = 0 ⇒ S(f, g) →G 0
LCM(LM(f), LM(g)) = LM(f) LM(g) ⇒ S(f, g)→G 0（f, g が 互いに素 なら S-多項式はゼロに簡約される）13年5月4日土曜日

互いに素判定
二番目の条件が使える！

x3 と z4 は互いに素なので S(x3 + y, z4) →G 0 となる
S(x3 + y, z4) = yz4∴ S(x3 + y, z4)G = y ≠ 0
今までの判定法だと無駄に割り算をする！
どれくらい改善？

13年5月4日土曜日

Benchmark
simpleprime

I1 = ⟨x2 + y2 + z2 − 1, x2 + y2 + z2 − 2x, 2x − 3y − z⟩
I2 = ⟨x2y − 2xy − 4z − 1, z − y2, x3 − 4zy⟩
I3 = ⟨2S − ay, b2 − (x2 + y2), c2 − ((a − x)2 + y2)⟩" I4 = ⟨z5 + y4 + x3 − 1, z3 + y3 + x2 − 1⟩

13年5月4日土曜日

Benchmark
simplelex01

prime
grlex02

grlex01

grevlex02

grevlex01

0.9s

lex03

1s

1.1s

1.2s

1.3s

grlex04

grlex03

grevlex04

grevlex03
0ms 22.5ms 45ms 67.5ms 90ms

0μs

150μs 300μs 450μs 600μs

I1 = ⟨x2 + y2 + z2 − 1, x2 + y2 + z2 − 2x, 2x − 3y − z⟩
I2 = ⟨x2y − 2xy − 4z − 1, z − y2, x3 − 4zy⟩
I3 = ⟨2S − ay, b2 − (x2 + y2), c2 − ((a − x)2 + y2)⟩" I4 = ⟨z5 + y4 + x3 − 1, z3 + y3 + x2 − 1⟩

13年5月4日土曜日

紹介する手法

ゼロ簡約関係
syzygy の基底
sugar strategy

13年5月4日土曜日

syzygy の基底
そもそも S-多項式とは何なのか？
実は syzygy と呼ばれるものの基底！
Gröbner 基底の基底とは意味が若干違う“syzygy のもと” と思えばよい

13年5月4日土曜日

syzygy
定義

13年5月4日土曜日

syzygy定義(h1, …, hs) ∈ k[𝕏]s が F = (f1, …, fs) ⊆ k[𝕏]s の 先頭項のsyzygy :⇔ h1 LT(f1) + ⋯ + hs LT(fs) = 0
F の先頭項 syzygy の全体を S(F) と書く。

13年5月4日土曜日

syzygy定義(h1, …, hs) ∈ k[𝕏]s が F = (f1, …, fs) ⊆ k[𝕏]s の 先頭項のsyzygy :⇔ h1 LT(f1) + ⋯ + hs LT(fs) = 0
F の先頭項 syzygy の全体を S(F) と書く。
T ⊆ S(F) が S(F) の基底 ⇔ S(F) のどの元も T の元の有限個の和で書ける。

13年5月4日土曜日

syzygy定義(h1, …, hs) ∈ k[𝕏]s が F = (f1, …, fs) ⊆ k[𝕏]s の 先頭項のsyzygy :⇔ h1 LT(f1) + ⋯ + hs LT(fs) = 0
F の先頭項 syzygy の全体を S(F) と書く。
T ⊆ S(F) が S(F) の基底 ⇔ S(F) のどの元も T の元の有限個の和で書ける。
ei = (0, …, 0, 1, 0, …, 0) (i 番目だけ 1) と書くことにする。このときSij :=LCM(LT(fi), LT(fj))
LT(fi)ei −LCM(LT(fi), LT(fj))
LT(fj)と置くと、 S(fi, fj) = Sij ⋅ F （内積）となる。
13年5月4日土曜日

ejsyzygy の基底とゼロ簡約

13年5月4日土曜日

syzygy の基底とゼロ簡約定理
I ⊆ k[𝕏]：イデアル>：単項式順序G = {g1, …, gk} ⊆ I：I の生成元

S ⊆ S(G)：G の先頭項 syzygy の基底
このとき以下の二つは同値：
1. G は > に関する I の Gröbner 基底
2.任意の T ∈ S に対し、k

T ⋅ G = ∑ i = 1 ti gi →G 0 (∀ i < j)
13年5月4日土曜日

S-多項式と syzygy

13年5月4日土曜日

S-多項式と syzygy
実は Sij の全体は S(G) の基底

13年5月4日土曜日

S-多項式と syzygy
実は Sij の全体は S(G) の基底
余分な基底も混じっているF = (x2y2 + z, xy2 − y, x2y + yz)
S12 = (1, -x, 0)

S13 = (1, 0, -y)S13 − S12 = (0, x, -y) = S23∴ S23 は要らない子

13年5月4日土曜日

S23 = (0, x, -y)S-多項式と syzygy
実は Sij の全体は S(G) の基底
余分な基底も混じっているF = (x2y2 + z, xy2 − y, x2y + yz)
S12 = (1, -x, 0)

S13 = (1, 0, -y)S23 = (0, x, -y)S13 − S12 = (0, x, -y) = S23∴ S23 は要らない子
余分な基底を予め判定出来ないか？
13年5月4日土曜日

無駄な syzygy 基底の判定

13年5月4日土曜日

無駄な syzygy 基底の判定
命題
G = (g1, …, gs)

gi, gj, gk ∈ G

𝒮 ⊆ {Sij ∣ 1 ≤ j < k ≤ s}：S(G) の基底
LT(gk) ∣ LCM(LT(gi), LT(gj)) かつ Sik, Sjk ∈ 𝒮⇒ S \ {Sij} も S(G) の基底

13年5月4日土曜日

無駄な syzygy 基底の判定
命題
G = (g1, …, gs)

gi, gj, gk ∈ G

𝒮 ⊆ {Sij ∣ 1 ≤ j < k ≤ s}：S(G) の基底
LT(gk) ∣ LCM(LT(gi), LT(gj)) かつ Sik, Sjk ∈ 𝒮⇒ S \ {Sij} も S(G) の基底
これで割り算の回数を大幅に減らせる！
13年5月4日土曜日

改良版 Buchberger・改

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F

13年5月4日土曜日

t := s改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：
1. (i, j) ∈ B を任意に選ぶ

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：
1. (i, j) ∈ B を任意に選ぶ
2. LCM(LT(fi), LT(fj)) ≠ LT(fi) LT(fj) かつ Test(fi, fj, B) が偽なら13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：
1. (i, j) ∈ B を任意に選ぶ
2. LCM(LT(fi), LT(fj)) ≠ LT(fi) LT(fj) かつ Test(fi, fj, B) が偽なら
1. S := S(fi, fj)G

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：
1. (i, j) ∈ B を任意に選ぶ
2. LCM(LT(fi), LT(fj)) ≠ LT(fi) LT(fj) かつ Test(fi, fj, B) が偽なら
1. S := S(fi, fj)G
2. S ≠ 0 ならば
t = t + 1, ft = S, G = G ∪ {ft}, B = B ∪ {(i, t)∣1 ≤ i ≤ t − 1}

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：
1. (i, j) ∈ B を任意に選ぶ
2. LCM(LT(fi), LT(fj)) ≠ LT(fi) LT(fj) かつ Test(fi, fj, B) が偽なら
1. S := S(fi, fj)G
2. S ≠ 0 ならば
t = t + 1, ft = S, G = G ∪ {ft}, B = B ∪ {(i, t)∣1 ≤ i ≤ t − 1}
3. B = B \ {(i, j)}

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：
1. (i, j) ∈ B を任意に選ぶ
2. LCM(LT(fi), LT(fj)) ≠ LT(fi) LT(fj) かつ Test(fi, fj, B) が偽なら
1. S := S(fi, fj)G
2. S ≠ 0 ならば
t = t + 1, ft = S, G = G ∪ {ft}, B = B ∪ {(i, t)∣1 ≤ i ≤ t − 1}
3. B = B \ {(i, j)}
出力：G

13年5月4日土曜日

改良版 Buchberger・改
入力： F = (f1, …, fs)

初期化：B := {(i, j)∣1 ≤ i < j ≤ s}（syzygy基底の候補）
G := F t := s
手順： B = ∅ となるまで次を繰り返す：
1. (i, j) ∈ B を任意に選ぶ
2. LCM(LT(fi), LT(fj)) ≠ LT(fi) LT(fj) かつ Test(fi, fj, B) が偽なら
1. S := S(fi, fj)G
2. S ≠ 0 ならば
t = t + 1, ft = S, G = G ∪ {ft}, B = B ∪ {(i, t)∣1 ≤ i ≤ t − 1}
3. B = B \ {(i, j)}
出力：G
但しTest(fi, fj, B) ⇔ ∃ k ≠ i, j [(i, k), (i, j) ∉ B, LT(fk) ∣ LCM(LT(fi), LT(fj))]
13年5月4日土曜日

実装
syzygyBuchberger ideal = runST $ dobases ← newSTRef { Entry LM(f) f | f ← ideal }pairs ← newSTRef {(f, g) | (f, g) ← combinations ideal }len ← newSTRef $ length ideal
whileM_ (not . null <$> readSTRef pairs) $ do
Just ((f, g), rest) ← viewMin <$> readSTRef pairs
bases0 ← readSTRef bases
b .= rest
let redundant =any (λ(Entry _ h) → h ∉ {f, g} ∧ (all (∉ rest) [(f, h), (g, h)])∧ LM(h) | LCM(LM(f), LM(g))) bases
when (LCM(LM(f), LM(g)) ≠ LM(f) LM(g) ∧ not redundant) $ do
len0 ← readSTRef len
let s = S(f, g) `mod` map payload (toList bases0)
when (s ≠ zero) $ dopairs += { (q, s) | Entry _ q ← qs }bases %= insert (Entry LM(s) s)
len *= 2
map payload . toList <$> readSTRef bases

13年5月4日土曜日

実装の解説13年5月4日土曜日

実装の解説効率のため ST モナドにした

13年5月4日土曜日

実装の解説効率のため ST モナドにした{} で囲まれているのは優先度キューのつもり

13年5月4日土曜日

実装の解説効率のため ST モナドにした{} で囲まれているのは優先度キューのつもり
経験的に、割り算をする際は先頭項を昇順に並べておくとよい

13年5月4日土曜日

実装の解説効率のため ST モナドにした{} で囲まれているのは優先度キューのつもり
経験的に、割り算をする際は先頭項を昇順に並べておくとよい
どんどん割れて回数が少なくなる

13年5月4日土曜日

実装の解説効率のため ST モナドにした{} で囲まれているのは優先度キューのつもり
経験的に、割り算をする際は先頭項を昇順に並べておくとよい
どんどん割れて回数が少なくなる
基底候補を先頭項を優先度とするキューとして持っておいて、割るときに toList で昇順に並べている

13年5月4日土曜日

Benchmark
simple13年5月4日土曜日

prime

syzygyBenchmark
simple
lex01

prime

syzygygrlex02

grlex01

grevlex02

grevlex01

0s

0.375s 0.75s 1.125s 1.5s

0μs

150μs 300μs 450μs 600μs

lex03
grlex04

grlex03

grevlex04

grevlex03
0ms 22.5ms 45ms 67.5ms 90ms

13年5月4日土曜日

Benchmark
simple
lex01

prime

syzygygrlex02

grlex01

grevlex02

grevlex01

0s

0.375s 0.75s 1.125s 1.5s

0μs

150μs 300μs 450μs 600μs

lex03
grlex04

grlex03

grevlex04

grevlex03
0ms 22.5ms 45ms 67.5ms 90ms

速すぎて見えない……
13年5月4日土曜日

互いに素判定との比較
prime
lex01

syzygygrlex02

grlex01

grevlex02

grevlex01

0s

0.375s 0.75s 1.125s 1.5s

lex03
grlex04

grlex03

grevlex04

grevlex03
0ms 2.5ms 5ms

13年5月4日土曜日

7.5ms 10ms

58μs 59.25μs60.5μs61.75μs 63μs

互いに素判定との比較
prime
lex01

syzygygrlex02

grlex01

grevlex02

grevlex01

0s

0.375s 0.75s 1.125s 1.5s

lex03
grlex04

grlex03

grevlex04

grevlex03
0ms 2.5ms 5ms

7.5ms 10ms

58μs 59.25μs60.5μs61.75μs 63μs

それでも速い ！
13年5月4日土曜日

紹介する手法

ゼロ簡約関係
syzygy の基底
sugar strategy

13年5月4日土曜日

Buchberger の自由度

13年5月4日土曜日

Buchberger の自由度
基底の候補 (i, j) を検討していく順番は自由13年5月4日土曜日

Buchberger の自由度
基底の候補 (i, j) を検討していく順番は自由
この順番の選び方をどうするか？ = selection
strategy

13年5月4日土曜日

Buchberger の自由度
基底の候補 (i, j) を検討していく順番は自由
この順番の選び方をどうするか？ = selection
strategy
ヒューリスティックな戦略が知られている

13年5月4日土曜日

selection strategy

13年5月4日土曜日

selection strategy
normal strategy

13年5月4日土曜日

selection strategy
normal strategy
先頭項の LCM が常に最小になるもの

13年5月4日土曜日

selection strategy
normal strategy
先頭項の LCM が常に最小になるもの
lex 順序など次数を保たない順序では逆効果

13年5月4日土曜日

selection strategy
normal strategy
先頭項の LCM が常に最小になるもの
lex 順序など次数を保たない順序では逆効果
sugar strategy

13年5月4日土曜日

selection strategy
normal strategy
先頭項の LCM が常に最小になるもの
lex 順序など次数を保たない順序では逆効果
sugar strategy
仮想的な斉次化次数が最小の物を選ぶ

13年5月4日土曜日

selection strategy
normal strategy
先頭項の LCM が常に最小になるもの
lex 順序など次数を保たない順序では逆効果
sugar strategy
仮想的な斉次化次数が最小の物を選ぶ
いずれも同率一位が出たら早く出て来た方を選ぶ

13年5月4日土曜日

selection strategy
normal strategy
先頭項の LCM が常に最小になるもの
lex 順序など次数を保たない順序では逆効果
sugar strategy
仮想的な斉次化次数が最小の物を選ぶ
いずれも同率一位が出たら早く出て来た方を選ぶ
この条件を抜かすと恐しく遅くなる……

13年5月4日土曜日

斉次化次数13年5月4日土曜日

斉次化次数
斉次式（各単項式の全次数が等しい多項式）を生成元とするイデアルの計算は経験的に速い

13年5月4日土曜日

斉次化次数
斉次式（各単項式の全次数が等しい多項式）を生成元とするイデアルの計算は経験的に速い
余分な変数で生成元を斉次化してから計算するというヒュー
リスティクスが知られている

13年5月4日土曜日

斉次化次数
斉次式（各単項式の全次数が等しい多項式）を生成元とするイデアルの計算は経験的に速い
余分な変数で生成元を斉次化してから計算するというヒュー
リスティクスが知られている
斉次化の例：xy + 2x + y3 + 3 ⇒ xyz + 2xz2 + y3 + 3z3

13年5月4日土曜日

斉次化次数
斉次式（各単項式の全次数が等しい多項式）を生成元とするイデアルの計算は経験的に速い
余分な変数で生成元を斉次化してから計算するというヒュー
リスティクスが知られている
斉次化の例：xy + 2x + y3 + 3 ⇒ xyz + 2xz2 + y3 + 3z3

問題点：得られた基底から余分な変数を消去してもGröbner 基底になるとは限らない

13年5月4日土曜日

斉次化次数
斉次式（各単項式の全次数が等しい多項式）を生成元とするイデアルの計算は経験的に速い
余分な変数で生成元を斉次化してから計算するというヒュー
リスティクスが知られている
斉次化の例：xy + 2x + y3 + 3 ⇒ xyz + 2xz2 + y3 + 3z3

問題点：得られた基底から余分な変数を消去してもGröbner 基底になるとは限らない
斉次化して得られた元に対してもう一度 Buchbergerを使うことになる（それでも多少は速くなる場合があるらしい）

13年5月4日土曜日

sugar strategy

13年5月4日土曜日

sugar strategy
普通に Buchberger を計算するが、(i, j) を選択するときだけ仮想的な斉次化を行い、その次数最小のものを選ぶ

13年5月4日土曜日

sugar strategy
普通に Buchberger を計算するが、(i, j) を選択するときだけ仮想的な斉次化を行い、その次数最小のものを選ぶ
この仮想的な次数のことを sugar という

13年5月4日土曜日

sugar多項式 (fi, fj) の sugar を次のように定める。

13年5月4日土曜日

sugar多項式 (fi, fj) の sugar を次のように定める。

Sfᵢ = deg(fi), Sfⱼ = deg(fj)

13年5月4日土曜日

sugar多項式 (fi, fj) の sugar を次のように定める。

Sfᵢ = deg(fi), Sfⱼ = deg(fj)Sf：given で t が単項式なら Stf = deg(t) + Sf

13年5月4日土曜日

sugar多項式 (fi, fj) の sugar を次のように定める。

Sfᵢ = deg(fi), Sfⱼ = deg(fj)Sf：given で t が単項式なら Stf = deg(t) + Sf
f = g + h の時、Sf = max(Sg, Sf)

13年5月4日土曜日

sugar多項式 (fi, fj) の sugar を次のように定める。

Sfᵢ = deg(fi), Sfⱼ = deg(fj)Sf：given で t が単項式なら Stf = deg(t) + Sf
f = g + h の時、Sf = max(Sg, Sf)(fi, fj) の sugar は、上に従って計算した S-多項式の sugar とする。
13年5月4日土曜日

実際の実装13年5月4日土曜日

実際の実装おあつらえ向きに優先度キューを使っていた13年5月4日土曜日

実際の実装おあつらえ向きに優先度キューを使っていた“selection strategy = 優先度の計算方法”
として抽象化出来る！

13年5月4日土曜日

実際の実装おあつらえ向きに優先度キューを使っていた“selection strategy = 優先度の計算方法”
として抽象化出来る！
double sugar という手法はこれだけでは無理（でもそこまで効果がないらしいので無視）13年5月4日土曜日

実際の実装おあつらえ向きに優先度キューを使っていた“selection strategy = 優先度の計算方法”
として抽象化出来る！
double sugar という手法はこれだけでは無理（でもそこまで効果がないらしいので無視）(i, j) を保存する時に重みも保存しておく
13年5月4日土曜日

実装
syzygyBuchbergerWithStrategy strategy ideal = runST $ dolet gens = zip [1..] ideal
bases ← newSTRef { Entry LM(f) f | (_, f) ← gens }pairs ← newSTRef { Entry (calcWeight strategy f g, j) (f, g)| ((i, f), (j, g)) ← combinations ideal }len ← newSTRef $ length ideal
whileM_ (not . null <$> readSTRef pairs) $ do
Just (Entry _ (f, g), rest) ← viewMin <$> readSTRef pairs-- 中略when (s ≠ zero) $ dopairs += { Entry (calcWeight strategy q s, j) (q, s)| Entry _ q ← qs | j ← [len0 + 1 ..] }bases %= insert (Entry LM(s) s)
len *= 2
map payload . toList <$> readSTRef bases

重みを追加するだけで実装出来てしまった……
13年5月4日土曜日

Benchmark
syzygy13年5月4日土曜日

sugar

Benchmark
syzygy
lex01

sugar

grlex02

grlex01

grevlex02

grevlex01

16ms

17ms 18ms 19ms 20ms

lex03
grlex04

grlex03

grevlex04

grevlex03
0ms 0.15ms 0.3ms 0.45ms 0.6ms

13年5月4日土曜日

58μs 58.1μs 58.2μs58.3μs58.4μs

Benchmark（論文版）
syzygysugar

I1 = ⟨35y4 − 10xy2 − 210y2z + 3x2 + 30xz − 105z2 + 140yt − 21u,

5xy3 − 140y3z − 3x2y + 45xyz − 420yz2 + 210y2t − 25xt + 70zt + 126yu⟩

I2 = ⟨x + y + z + w, xy + yz + zw + wx, xyz + yzw + zwx + wxy, xyzw − 1⟩
I3 = ⟨x31 − x6 − x − y, x8 − z, x10 − t⟩

13年5月4日土曜日

Benchmark（論文版）
syzygygrevlex01

sugar
lex01
0ms 0.5ms

lex02
grevlex02

1ms

1.5ms

grevlex03
0ms

10ms 20ms 30ms 40ms

0ms 700ms1400ms2100ms2800ms

I1 = ⟨35y4 − 10xy2 − 210y2z + 3x2 + 30xz − 105z2 + 140yt − 21u,

5xy3 − 140y3z − 3x2y + 45xyz − 420yz2 + 210y2t − 25xt + 70zt + 126yu⟩

I2 = ⟨x + y + z + w, xy + yz + zw + wx, xyz + yzw + zwx + wxy, xyzw − 1⟩
I3 = ⟨x31 − x6 − x − y, x8 − z, x10 − t⟩

13年5月4日土曜日

2ms

考察

13年5月4日土曜日

考察
論文に出てくる例については sugar が速い

13年5月4日土曜日

考察
論文に出てくる例については sugar が速い
それでも驚くほど速いようには見えない

13年5月4日土曜日

考察
論文に出てくる例については sugar が速い
それでも驚くほど速いようには見えない
こちらで選んだデータセットに関してはsugar のほうが遅い場合もある？

13年5月4日土曜日

考察
論文に出てくる例については sugar が速い
それでも驚くほど速いようには見えない
こちらで選んだデータセットに関してはsugar のほうが遅い場合もある？
追跡調査予定13年5月4日土曜日

ここまでで質問？

13年5月4日土曜日

Table of Contents
Gröbner 基底の簡単な導入
Gröbner 基底の計算法
Buchberger アルゴリズム
最適化手法：syzygy, sugar strategy
Haskell の型レベルプログラミングの現在

13年5月4日土曜日

Haskell の型レベルプログラミングの現在

13年5月4日土曜日

Haskell の型レベルプログラミングの現在
computational-algebra では型機能をふんだんに利用している13年5月4日土曜日

Haskell の型レベルプログラミングの現在
computational-algebra では型機能をふんだんに利用している
変数の数、体の種類、単項式順序、選択戦略…

13年5月4日土曜日

Haskell の型レベルプログラミングの現在
computational-algebra では型機能をふんだんに利用している
変数の数、体の種類、単項式順序、選択戦略…
全て型にパラメトライズ

13年5月4日土曜日

Haskell の型レベルプログラミングの現在
computational-algebra では型機能をふんだんに利用している
変数の数、体の種類、単項式順序、選択戦略…
全て型にパラメトライズ
依存型と証明のオンパレード

13年5月4日土曜日

依存型と証明のオンパレード

13年5月4日土曜日

依存型と証明のオンパレードDataKinds や GADTs といった拡張機能を多用

13年5月4日土曜日

依存型と証明のオンパレードDataKinds や GADTs といった拡張機能を多用
単項式は指数ベクトルで表現しているので、変数の数の区別をしっかりつけたい

13年5月4日土曜日

依存型と証明のオンパレードDataKinds や GADTs といった拡張機能を多用
単項式は指数ベクトルで表現しているので、変数の数の区別をしっかりつけたい
長さつきベクトル！

13年5月4日土曜日

依存型と証明のオンパレードDataKinds や GADTs といった拡張機能を多用
単項式は指数ベクトルで表現しているので、変数の数の区別をしっかりつけたい
長さつきベクトル！
境界条件も証明しよう！

13年5月4日土曜日

依存型と証明のオンパレードDataKinds や GADTs といった拡張機能を多用
単項式は指数ベクトルで表現しているので、変数の数の区別をしっかりつけたい
長さつきベクトル！
境界条件も証明しよう！
これだけでもかなり大変なので、「アルゴリズムの妥当性」とかは示していないです（死ぬ）

13年5月4日土曜日

詳しくはコード参照-- | N-ary Monomial. IntMap contains degrees for each xi.
type Monomial (n :: Nat) = Vector Int n-- | Monomial with monomial order.
newtype OrderedMonomial (ord :: ⋆) n =OrderedMonomial { getMonomial :: Monomial n }deriving instance (Eq (Monomial n)) ⇒ Eq (OrderedMonomial ordering n)type MonomialOrder = ∀n. Monomial n → Monomial n → Ordering-- | Class to lookup ordering from its (type-level) name.
class IsOrder (ordering :: ⋆) where
cmpMonomial :: Proxy ordering → MonomialOrder-- | Class for Monomial orders.
class IsOrder name ⇒ IsMonomialOrder name where

13年5月4日土曜日

詳しくはコード参照
data Lex = Lexdata Revlex = Revlex
data Grevlex = Grevlex
lex :: MonomialOrderlex Nil Nil = EQ
lex (x :- xs) (y :- ys) = x `compare` y <> xs `lex` ys
lex _ _ = error "cannot happen"
revlex :: Monomial n → Monomial n → Ordering
revlex (x :- xs) (y :- ys) = xs `revlex` ys <> y `compare` x
revlex Nil
Nil= EQ
revlex _ _ = error "cannot happen!"
graded :: (Monomial n → Monomial n → Ordering) → (Monomial n → Monomial n →Ordering)
graded cmp xs ys = comparing totalDegree xs ys <> cmp xs ys
instance IsOrder Grevlex where
cmpMonomial _ = graded revlex
instance IsOrder Revlex where
cmpMonomial _ = revlex

13年5月4日土曜日

cannot happen!

13年5月4日土曜日

cannot happen!
型レベルで禁止されるパターン

13年5月4日土曜日

cannot happen!
型レベルで禁止されるパターン
しかし、 -fwarn-incomplete-pattern を指定
すると「このパターン抜けてるよ！」

13年5月4日土曜日

cannot happen!
型レベルで禁止されるパターン
しかし、 -fwarn-incomplete-pattern を指定
すると「このパターン抜けてるよ！」
そのパターンを書くと型エラーで弾かれる

13年5月4日土曜日

cannot happen!
型レベルで禁止されるパターン
しかし、 -fwarn-incomplete-pattern を指定
すると「このパターン抜けてるよ！」
そのパターンを書くと型エラーで弾かれるだから wildcard pattern

13年5月4日土曜日

イデアル hackdata Ideal r = ∀n. Ideal (Vector r n)
instance Eq r ⇒ Eq (Ideal r) where(≡) = (≡) `on` generators
generators :: Ideal r → [r]generators (Ideal is) = toList is
addToIdeal :: r → Ideal r → Ideal r
addToIdeal i (Ideal is) = Ideal (i :- is)
toIdeal :: NoetherianRing r ⇒ [r] → Ideal r
toIdeal = foldr addToIdeal (Ideal Nil)

13年5月4日土曜日

イデアル hackdata Ideal r = ∀n. Ideal (Vector r n)
instance Eq r ⇒ Eq (Ideal r) where(≡) = (≡) `on` generators
generators :: Ideal r → [r]generators (Ideal is) = toList is
addToIdeal :: r → Ideal r → Ideal r
addToIdeal i (Ideal is) = Ideal (i :- is)
toIdeal :: NoetherianRing r ⇒ [r] → Ideal r
toIdeal = foldr addToIdeal (Ideal Nil)

イデアルはリスト……ではない！

13年5月4日土曜日

イデアル hackdata Ideal r = ∀n. Ideal (Vector r n)
instance Eq r ⇒ Eq (Ideal r) where(≡) = (≡) `on` generators
generators :: Ideal r → [r]generators (Ideal is) = toList is
addToIdeal :: r → Ideal r → Ideal r
addToIdeal i (Ideal is) = Ideal (i :- is)
toIdeal :: NoetherianRing r ⇒ [r] → Ideal r
toIdeal = foldr addToIdeal (Ideal Nil)

イデアルはリスト……ではない！
非常に深遠なる理由により存在量化された sized-vector

13年5月4日土曜日

イデアル hackdata Ideal r = ∀n. Ideal (Vector r n)
instance Eq r ⇒ Eq (Ideal r) where(≡) = (≡) `on` generators
generators :: Ideal r → [r]generators (Ideal is) = toList is
addToIdeal :: r → Ideal r → Ideal r
addToIdeal i (Ideal is) = Ideal (i :- is)
toIdeal :: NoetherianRing r ⇒ [r] → Ideal r
toIdeal = foldr addToIdeal (Ideal Nil)

イデアルはリスト……ではない！
非常に深遠なる理由により存在量化された sized-vector
消去イデアルの計算の時に暗黙裏に型を合わせる為13年5月4日土曜日

辻褄を合わせに用意されたdata Monomorphic k = ∀a. Monomorphic (k a)-- | A types which have the monomorphic representation.
class Monomorphicable k where-- | Monomorphic representation
type MonomorphicRep k :: ⋆-- | Promote the monomorphic value to the polymophic one.
promote :: MonomorphicRep k → Monomorphic k-- | Demote the polymorphic value to the monomorphic representation.
demote :: Monomorphic k → MonomorphicRep k-- | Convinience function to demote polymorphic types-into monomorphic one directly.
demote' :: Monomorphicable k ⇒ k a → MonomorphicRep k
demote' = demote ∘ Monomorphic-- | Demote polymorphic nested types directly into-monomorphic representation.
demoteComposed :: Monomorphicable (f :∘: g)⇒ f (g a) → MonomorphicRep (f :∘: g)demoteComposed = demote ∘ Monomorphic ∘ Comp13年5月4日土曜日

制約付けてる感じ
thEliminationIdeal :: ( IsMonomialOrder ord, Field k, IsPolynomial k m, IsPolynomial k (m :-: n), (n ≼ m) ~ True)⇒ SNat n→ Ideal (OrderedPolynomial k ord m)→ Ideal (OrderedPolynomial k ord (m ⊖ n))
thEliminationIdeal n =case singInstance n of
SingInstance →mapIdeal (changeOrderProxy Proxy) ∘thEliminationIdealWith (weightedEliminationOrder n) n

13年5月4日土曜日

制約付けてる感じ
thEliminationIdeal :: ( IsMonomialOrder ord, Field k, IsPolynomial k m, IsPolynomial k (m :-: n), (n ≼ m) ~ True)⇒ SNat n→ Ideal (OrderedPolynomial k ord m)→ Ideal (OrderedPolynomial k ord (m ⊖ n))
thEliminationIdeal n =case singInstance n of
SingInstance →mapIdeal (changeOrderProxy Proxy) ∘thEliminationIdealWith (weightedEliminationOrder n) n

Gröbner 基底を使うと、連立方程式から文字を消去出来る（すごい！）13年5月4日土曜日

制約付けてる感じ
thEliminationIdeal :: ( IsMonomialOrder ord, Field k, IsPolynomial k m, IsPolynomial k (m :-: n), (n ≼ m) ~ True)⇒ SNat n→ Ideal (OrderedPolynomial k ord m)→ Ideal (OrderedPolynomial k ord (m ⊖ n))
thEliminationIdeal n =case singInstance n of
SingInstance →mapIdeal (changeOrderProxy Proxy) ∘thEliminationIdealWith (weightedEliminationOrder n) n

Gröbner 基底を使うと、連立方程式から文字を消去出来る（すごい！）n 文字目までを消去したい
13年5月4日土曜日

変数は最低でも n 個

証明してる感じ
intersection :: ∀ r k n ord.
( IsMonomialOrder ord, Field r, IsPolynomial r k, IsPolynomial r n, IsPolynomial r (k ⊕ n))
⇒ Vector (Ideal (OrderedPolynomial r ord n)) k→ Ideal (OrderedPolynomial r ord n)intersection Nil = Ideal $ singletonV one
intersection idsv@(_ :- _) =let sk = sLengthV idsv
sn = sing :: SNat n
ts = genVars (sk %+ sn)
tis = zipWith (λ ideal t → mapIdeal ((t *) . shiftR sk) ideal)(toList idsv) ts
j = foldr appendIdeal (principalIdeal (one - foldr (+) zero ts)) tis
in case plusMinusEqR sn sk of
Eql → case propToBoolLeq (plusLeqL sk sn) of
LeqTrueInstance → thEliminationIdeal sk j

13年5月4日土曜日

今気付いたけど全部説明するの無理だ

13年5月4日土曜日

もうだめだ
13年5月4日土曜日

詳しくは直接捕まえて訊いてください

13年5月4日土曜日

最後にいいたいこと

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる
証明は実行時に遅延されるからタダじゃない

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる
証明は実行時に遅延されるからタダじゃない
シングルトンもコストがかかる

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる
証明は実行時に遅延されるからタダじゃない
シングルトンもコストがかかる
Haskell での依存型で実用的なアプリ書くのはむずい

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる
証明は実行時に遅延されるからタダじゃない
シングルトンもコストがかかる
Haskell での依存型で実用的なアプリ書くのはむずい
HP 標準添付の GHC 7.4.* はクソ

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる
証明は実行時に遅延されるからタダじゃない
シングルトンもコストがかかる
Haskell での依存型で実用的なアプリ書くのはむずい
HP 標準添付の GHC 7.4.* はクソ
コンパイルする度に rm *.hi *.o しないと型機能が使えない

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる
証明は実行時に遅延されるからタダじゃない
シングルトンもコストがかかる
Haskell での依存型で実用的なアプリ書くのはむずい
HP 標準添付の GHC 7.4.* はクソ
コンパイルする度に rm *.hi *.o しないと型機能が使えない
種多相な外部ライブラリとリンク出来ない

13年5月4日土曜日

最後にいいたいこと
帰納法はコストがかかる
証明は実行時に遅延されるからタダじゃない
シングルトンもコストがかかる
Haskell での依存型で実用的なアプリ書くのはむずい
HP 標準添付の GHC 7.4.* はクソ
コンパイルする度に rm *.hi *.o しないと型機能が使えない
種多相な外部ライブラリとリンク出来ない
案外型の辻褄はあう

13年5月4日土曜日

まとめ

13年5月4日土曜日

まとめ
Gröbner基底を使うと代数の計算が出来るように

13年5月4日土曜日

まとめ
Gröbner基底を使うと代数の計算が出来るように
イデアル商とか共通部分とか13年5月4日土曜日

まとめ
Gröbner基底を使うと代数の計算が出来るように
イデアル商とか共通部分とか文字消去、連立方程式の解

13年5月4日土曜日

まとめ
Gröbner基底を使うと代数の計算が出来るように
イデアル商とか共通部分とか文字消去、連立方程式の解高速化手法が幾つかあって、切磋琢磨

13年5月4日土曜日

まとめ
Gröbner基底を使うと代数の計算が出来るように
イデアル商とか共通部分とか文字消去、連立方程式の解高速化手法が幾つかあって、切磋琢磨
Haskell 型システムの今後に期待

13年5月4日土曜日

参考文献
D. Cox, J. Little and D. O’Shea. Ideals, Varieties
and Algorithms. UTM. Springer.
A. Giovini, T. Moran, G. Niesi, L. Robbiano and C.
Traverse. "One sugar cube, please" OR Selection
strategies in the Buchberger algorithm.
楫元. グレブナー基底は面白い！. 講義録.
2012年度早稲田大学基幹理工学部数学科代数学C1
講義資料

13年5月4日土曜日

Any Questions?

13年5月4日土曜日

御清聴
ありがとうございました

13年5月4日土曜日