[Coq] TPPmark2014 : Theorem Prover Advent Calendar

　TPP (Theorem proving and provers for reliable theory and implementations) 2014 という定理証明系に関するワークショップがあり、毎年秋〜冬に日本で開催されています。
 　TPPでは毎年TPPmarkという問題が出題され、参加者（あるいは解きたい人）が、各自自分の好きな定理証明系で問題を解いてその解答を紹介したりします。で、今年の問題は2014年の九州大学の入試問題（数IIB問題の[2]。リンクは河合塾サイト）の問題だ、と種明かしがありました。
 　参加者の解答はgithubで公開されています。

 　で、自分の解答の解説を。基本的に誘導に従い、高校数学の範囲で解いたつもりです。 

まず色々便利な様に、３づつ大きくなる場合の自然数の帰納法を定義します。

Theorem nat_ind_3 : forall P: nat -> Prop, P 0 -> P 1 -> P 2 -> 
  (forall n, P n -> P (S(S(S n)))) -> forall n, P n. 

次に３での商とか余りを定義します。

Fixpoint div3(n:nat):nat := match n with 
| S(S(S n')) => S (div3 n') 
| _ => 0 
end. 

Fixpoint mod3(n:nat):nat := match n with 
| S(S(S n')) => mod3 n' 
| _ => n 
end. 

これらに関する簡単な補題を幾つか証明しますが、特に３で割った余りに関する場合分け

Lemma mod3_012 : forall n, (mod3 n = 0) \/ (mod3 n = 1) \/ (mod3 n = 2). 

を証明しておくと、場合分け出来る様になるので便利です。
mod 3に関しては下記のような性質を証明し、以後の書き換えで使用します。

Lemma mod3_idem : forall n, mod3 (mod3 n) = mod3 n. 
Lemma mod3_add_hom: forall p q, mod3 (mod3 p + mod3 q) = mod3 (p + q). 
Lemma mod3_mul_hom: forall p q, mod3 (mod3 p * mod3 q) = mod3 (p * q). 

ここは３で割った剰余系をsetoidで作ることも考えましたが、そこまで必要無いと考え止めました。

問題１は、mod3_012で場合分けと、mod3_add_homでの書き換えを行えばOKです。

Theorem mod3_square_01 : forall a, (mod3 (a*a) = 0) \/ (mod3 (a*a) = 1). 

問題２もほぼ同様に a, b, cについて３で割った余りについて計算すればなんとかなります。

Theorem all_mod3_0 : forall a b c, a*a + b*b = 3*c*c -> 
  (mod3 a = 0) /\ (mod3 b = 0) /\ (mod3 c = 0). 

問題２と

Lemma mod3_0_q : forall n, mod3 n = 0 -> exists q, n = 3*q. 

とを使うと、a, b, cはそれぞれ３の倍数であることが言え、次の様な補題が言えます。

Lemma shrink_by_3 : forall a b c, a*a + b*b = 3*c*c -> 
  (exists a' b' c', a = 3*a' /\ b = 3*b' /\ c = 3*c' /\ 
  a'*a' + b'*b' = 3*c'*c'). 

上記の補題から無限降下列が得られます。 で、無限降下法はCoqのライブラリに無いので、整楚帰納法から証明します。

Theorem infinite_descent : forall P : nat -> Prop, 
  (forall n : nat, P n -> exists2 m : nat, m < n & P m) -> 
  forall n : nat, ~ P n. 

この整楚帰納法を使いやすい証明課題を３つ作ります。

Lemma cond_of_a: forall a, ~( ~(a=0) /\ (exists b c:nat, a*a+b*b = 3*c*c)). 
Lemma cond_of_b: forall b, ~( ~(b=0) /\ (exists a c:nat, a*a+b*b = 3*c*c)). 
Lemma cond_of_c: forall c, ~( ~(c=0) /\ (exists a b:nat, a*a+b*b = 3*c*c)). 

これは無限降下法とshrink_by_3を用いて証明出来ます。 この３つから問題３の証明を出来ます。

Theorem abc_are_0 : forall a b c:nat, a*a+b*b = 3*c*c -> 
  (a = 0 /\ b = 0 /\ c = 0). 

　最後に宣伝。東京ではCoqの勉強会であるSF読み進捗ダメです会議 #13 #readcoqart #Coqというのを月一回、開催しています。Coqに興味のある方は、一度遊びにきませんか？ 　

[IVA] Chapter 2, Section 9, Exercise 13

Exercise 13 について自作コードで試してみた。(あれからIntではなくBigIntを使う様にしてみたり、計算順序の最適化を実施したりなど。sugerや斉次化はまだ未実装。) が、色々やばいですね、lexでの計算。grevlexなら簡単に終わるのに。

scala> import basic._
import basic._

  val f13_1_grevlex = Poly(Seq(
     (Mono(Seq(5,0,0))(grevlex), Q(1,1)),
     (Mono(Seq(0,4,0))(grevlex), Q(1,1)),
     (Mono(Seq(0,0,3))(grevlex), Q(1,1)),
     (Mono(Seq(0,0,0))(grevlex), Q(-1,1))
     ))(grevlex)                                  //> f13_1_grevlex  : basic.Poly = x^5 + y^4 + z^3 + -1
  val f13_2_grevlex = Poly(Seq(
     (Mono(Seq(3,0,0))(grevlex), Q(1,1)),
     (Mono(Seq(0,2,0))(grevlex), Q(1,1)),
     (Mono(Seq(0,0,2))(grevlex), Q(1,1)),
     (Mono(Seq(0,0,0))(grevlex), Q(-1,1))
     ))(grevlex)                                  //> f13_2_grevlex  : basic.Poly = x^3 + z^2 + y^2 + -1
  val buch3_base13_grevlex = Poly.reduce(Poly.buchberger(Seq(f13_1_grevlex, f13_2_grevlex))(grevlex))(grevlex)
                                                  //> buch3_base13_grevlex  : Seq[basic.Poly] = List(
                                                  //| x^3 + z^2 + y^2 + -1,  
                                                  //| y^4 + -x^2z^2 + -x^2y^2 + z^3 + x^2 + -1)

scala> val lex = LexOrder(List('x,'y,'z))
lex: basic.LexOrder = LexOrder(List('x, 'y, 'z))

scala> val f13_1_lex = Poly(Seq(
     |      (Mono(Seq(5,0,0))(lex), Q(1,1)),
     |      (Mono(Seq(0,4,0))(lex), Q(1,1)),
     |      (Mono(Seq(0,0,3))(lex), Q(1,1)),
     |      (Mono(Seq(0,0,0))(lex), Q(-1,1))
     |      ))(lex) 
f13_1_lex: basic.Poly = x^5 + y^4 + z^3 + -1

scala> val f13_2_lex = Poly(Seq(
     |      (Mono(Seq(3,0,0))(lex), Q(1,1)),
     |      (Mono(Seq(0,2,0))(lex), Q(1,1)),
     |      (Mono(Seq(0,0,2))(lex), Q(1,1)),
     |      (Mono(Seq(0,0,0))(lex), Q(-1,1))
     |      ))(lex)
f13_2_lex: basic.Poly = x^3 + y^2 + z^2 + -1

scala> val buch3_base13_lex = Poly.reduce(Poly.buchberger(Seq(f13_1_lex, f13_2_lex))(lex))(lex)
buch3_base13_lex: Seq[basic.Poly] = List(x^3 + y^2 + z^2 + -1, x^2y^2 + x^2z^2 + -x^2 + -y^4 + -z^3 + 1, xy^4 + xz^3 + -x + y^4 + 2y^2z^2 + -2y^2 + z^4 + -2z^2 + 1, xy^2z + -xy^2 + 273/1408xz^12 + 1011/1408xz^11 + -227/1408xz^10 + -9665/4224xz^9 + 211/704xz^8 + 85/32xz^7 + -749/528xz^6 + 1/2xz^4 + -1/2xz^3 + -xz + x + -81/1408y^14 + -459/1408y^12z^2 + -9/176y^12z + 321/704y^12 + -819/1408y^10z^4 + -273/704y^10z^3 + 1323/704y^10z^2 + 39/176y^10z + -4373/4224y^10 + 273/1408y^8z^6 + -501/352y^8z^5 + 2329/1408y^8z^4 + 8551/4224y^8z^3 + -5871/1408y^8z^2 + 13/88y^8z + 395/352y^8 + -819/704y^6z^7 + 8373/1408y^6z^6 + 3213/704y^6z^5 + -3341/176y^6z^4 + -7555/2112y^6z^3 + 1219/66y^6z^2 + 53/88y^6z + -23341/4224y^6 + 273/704y^4z^9 + 9189/1408y^4z^8 + 773/352y^4z^7 + -33823/1056y^4z^6 + -17/3y^4z^5…
scala> buch3_base13_lex.length
res0: Int = 7

scala> buch3_base13_lex(0)
res2: basic.Poly = x^3 + y^2 + z^2 + -1

scala> buch3_base13_lex(1)
res3: basic.Poly = x^2y^2 + x^2z^2 + -x^2 + -y^4 + -z^3 + 1

scala> buch3_base13_lex(2)
res4: basic.Poly = xy^4 + xz^3 + -x + y^4 + 2y^2z^2 + -2y^2 + z^4 + -2z^2 + 1

scala> buch3_base13_lex(4)
res5: basic.Poly = xz^11 + 4xz^10 + xz^9 + -10xz^8 + -4xz^7 + 8xz^6 + 13145211549469524099276049970825174332001934982726555617/49464457656842324243991404386798887698363025825966149632y^22 + 336469772395565067430728152218633828000517403338752050447/98928915313684648487982808773597775396726051651932299264y^20z^2 + 41246821025682957247777391063405260354876124127586033329/98928915313684648487982808773597775396726051651932299264y^20z + -186688514037649654164494156802783046785181037030518263195/49464457656842324243991404386798887698363025825966149632y^20 + 3748115348128909106405657431258725581362590226678884005481/197857830627369296975965617547195550793452103303864598528y^18z^4 + 532878767777869557858761862556643001207912197601994175895/98928915313684648487982808773597775396726051651932299264...

scala> buch3_base13_lex(5)
res6: basic.Poly = y^12 + -y^10 + 3y^8z^3 + -5y^8z^2 + 2y^8 + -10y^6z^4 + 20y^6z^2 + -10y^6 + -7y^4z^6 + 30y^4z^4 + -6y^4z^3 + -30y^4z^2 + 13y^4 + -5y^2z^8 + 20y^2z^6 + -30y^2z^4 + 20y^2z^2 + -5y^2 + -z^10 + z^9 + 5z^8 + -13z^6 + 10z^4 + 3z^3 + -5z^2

scala> buch3_base13_lex(6)
res7: basic.Poly = x^2z^4 + x^2z^3 + -2x^2z^2 + -1/6xz^10 + -2/3xz^9 + -1/4xz^8 + 7/6xz^7 + -1/12xz^6 + -xz^5 + xz^4 + 1/2y^10z^2 + 1/3y^10z + -5/12y^10 + -1/6y^8z^4 + 1/3y^8z^3 + 1/4y^8z^2 + 1/2y^8 + y^6z^5 + -5/3y^6z^4 + -17/6y^6z^3 + 17/6y^6z^2 + 2/3y^6z + -1/3y^6 + -1/3y^4z^7 + -7/2y^4z^6 + -3y^4z^5 + 131/12y^4z^4 + 23/4y^4z^3 + -13y^4z^2 + -8/3y^4z + 29/6y^4 + -17/6y^2z^8 + -4y^2z^7 + 119/12y^2z^6 + 17/2y^2z^5 + -16y^2z^4 + -14/3y^2z^3 + 12y^2z^2 + 5/3y^2z + -55/12y^2 + -7/6z^10 + -7/6z^9 + 55/12z^8 + 21/4z^7 + -31/4z^6 + -15/2z^5 + 83/12z^4 + 41/12z^3 + -31/12z^2

scala>

[IVA] Chapter 2, Section 9, Exercise 1, 6, 11

Exersise 1.

$S=(c_1, \cdots, c_s)$, $T=(d_1, \cdots, d_s)$ は $F=(f_1, \cdots, f_s)$ の syzygy ゆえ、
$$\sum_{i=1}^s c_i \mathrm{LT}(f_i) = \sum_{i=1}^s d_i \mathrm{LT}(f_i) = 0$$.

$$\sum_{i=1}^s (c_i + d_i)  \mathrm{LT}(f_i) = \sum_{i=1}^s c_i \mathrm{LT}(f_i) + \sum_{i=1}^s d_i \mathrm{LT}(f_i) = 0$$,
$$\sum_{i=1}^s (g c_i)  \mathrm{LT}(f_i) = g \sum_{i=1}^s c_i \mathrm{LT}(f_i) = 0$$,
より
$S+T=(c_1 + d_1, \cdots, c_s + d_s)$, $g \cdot S = (g c_1, \cdots, g c_s)$ もまた syzygy となる。

Exercise 6.

$S_j$ が $S(G)$ の multideg $\gamma_j$ の homogeneous syzygy であるとき、$S_j \cdot G$ の multideg $< \gamma_j$ を示せ。

$G = (g_1, \cdots, g_s)$ とする。

$S_j \cdot G = \sum_{i=1}^s c_i x^{\alpha(i)} g_i$ であるが、
$$\mathrm{multideg}(S_j \cdot G) $$
$$= \mathrm{multideg}(\sum_{i=1}^s c_i x^{\alpha(i)} g_i) \leq \max_{i=1}^s \mathrm{multideg}(x^{\alpha(i)} g_i) $$
$$= \max_{i=1}^s \mathrm{multideg}(x^{\alpha(i)} \mathrm{LT}(g_i))$$

ここで等号成立は $\sum_{i=1}^s x^{\alpha(i)} \mathrm{LT}(g_i) \neq 0$ の場合であるが、

$S_j \subset S(G)$ であるから $\sum_{i=1}^s c_i x^{\alpha(i)} \mathrm{LT}(g_i) = 0$

より等号は成立しない。よって $\mathrm{multideg}(S_j \cdot G) < \max_{i=1}^s \mathrm{multideg}(x^{\alpha(i)} g_i)$ であるが、

homogeneous syzygy の定義より

$S_j = (c_1 x^{\alpha(1)}, \cdots, c_s x^{\alpha(s)})$ where $c_i \in k$ かつ $c_i \neq 0$ ならば $\alpha(i) + \mathrm{multideg}(g_i) = \gamma_j$

であるから、
 $\mathrm{multideg}(S_j \cdot G) < \gamma_j$ となる。

Exersise 11.

元の Buchberger では除算を 17 回、syzygy を使用したものは 4 回で済んでいる。

用いたコードは https://github.com/tmiya/scala_Buchberger にあります。

   // buchberger
  val buch_f1 = Poly(Seq(
     (Mono(Seq(3,0,0))(grlex), Q(1,1)),
     (Mono(Seq(1,1,0))(grlex), Q(-2,1))
     ))(grlex)                                    //> buch_f1  : basic.Poly = x^3 + -2xy
  val buch_f2 = Poly(Seq(
     (Mono(Seq(2,1,0))(grlex), Q(1,1)),
     (Mono(Seq(0,2,0))(grlex), Q(-2,1)),
     (Mono(Seq(1,0,0))(grlex), Q(1,1))
     ))(grlex)                                    //> buch_f2  : basic.Poly = x^2y + -2y^2 + x
  val buch_base1 = Poly.buchberger(Seq(buch_f1, buch_f2))(grlex)
                                                  //> divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| buch_base1  : Seq[basic.Poly] = ArrayBuffer(x^3 + -2xy, x^2y + -2y^2 + x, -
                                                  //| x^2, -2xy, -2y^2 + x)
  val buch_base2 = Poly.reduce(buch_base1)(grlex) //> buch_base2  : Seq[basic.Poly] = List(x^2, xy, y^2 + -1/2x)
  
  val buch2_base1 = Poly.buchberger2(Seq(buch_f1, buch_f2))(grlex)
                                                  //> divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| divmod
                                                  //| buch2_base1  : Seq[basic.Poly] = ArrayBuffer(x^3 + -2xy, x^2y + -2y^2 + x, 
                                                  //| -x^2, -2y^2 + x, -2xy)

ProofSummit 2014 & JSSST Coq Tutorial

名古屋で開催された ProofSummit 2014 と、同じく名古屋大学で開催されている日本ソフトウェア科学会のチュートリアル：定理証明支援系Coq入門 に参加しました。

ProofSummit は各種の定理証明系(今年は Coq, Agda, Mizarの話がありました)とその応用について年に一回（大体８月末〜９月初に）開催しているイベントで、2010年に開催された Coq庵 から数えると今年で５回目です。「Coq を使ってみた」的な初心者の発表から、定理証明系を使って計算機科学の研究をしているような研究者による発表など幅広い内容の発表があります。今年の発表のかなりの部分に付いては、上記リンクから発表資料が参照出来ると思います。
ProofSummit 今年は定理証明イベントと一緒に開催する関数型言語イベントが中止になったり、東京で ScalaMatsuri が開催されていたりなどで、ちょっと参加人数が減りましたが、来年もまた開催したいし、来年こそはなんかネタを用意して参加したいです。

Coq チュートリアルは、産総研でCoqを使って研究されている Affeldt さんによる、Coq を使う意義/Coqについて/Coqの拡張であるssreflectのチュートリアル、でした。聞きに行った主眼はssreflectのチュートリアルだったのですが、前半の定理証明系やCoqについての話の部分も非常に面白かったです。発表資料は Affeldt さんのページ から取得出来ます。
Coq チュートリアルは、100人以上が参加の、非常に盛況なチュートリアルでした。

その前の NII Shonan Coq セミナーと合わせて、この夏は Coq が熱い夏でした。今年のイベントとしてはあと、12/3-5に「高信頼な理論と実装のための定理証明および定理証明器」というのが九州で開催されます。

[IVA] Chapter 2, Section 8, Exercise 1,7

Mac版のAsirで計算しました

Exersise 1

$ /Applications/cfep.app/OpenXM/bin/openxm asir
[2189] G=gr([-x^3+y, x^2*y-z], [x,y,z], 0);
[-z*x+y^2,y*x^2-z,-x^3+y]
[2190] p_nf(x*y^3-z^2+y^5-z^3, G, [x,y,z], 0);
0

Exersise 7

$ /Applications/cfep.app/OpenXM/bin/openxm asir
[1891] load("gr");
[1998] load("noro_pd.rr");
[2182] B=[u*t-x, 1-u-y, u+t-u*t-z];
[-x+t*u,-y-u+1,-z+(-t+1)*u+t]
[2183] V=[u,t,x,y,z];
[u,t,x,y,z]
[2184] G=gr(B,V,2);
[y*x+y^2+(z-2)*y-z+1,-x-y-z+t+1,-y-u+1]
[2185] noro_pd.elimination(G,[x,y,z]);
[y*x+y^2+(z-2)*y-z+1]

NII Shonan School on Coq 参加報告

Coq というのは定理証明支援系のソフトウェアです。関数型言語に興味のある方の中にはカリー＝ハワード対応という言葉をご存知の方もいるのではないかと思いますが、これはプログラム⇔証明、型⇔命題という対応がある、というものです。Coq は依存型という、通常の静的型付け言語 (Haskell とか Scala など) より強力な型システムを用いることで、述語論理 (「全てのεに対して、あるδが存在して、どうのこうの」の様な量化子を含んだ式を表現出来る論理) の証明に対応するプログラムを書き、そしてその証明が正しいかを型検査することで機械的に確認出来ます。

じゃあ Coq を使うと何が良いのかというと、まず数学的な定理の証明を機械検証可能な形で証明出来ます。最近だとケプラー予想の機械的証明が話題になりましたね。他にも四色問題などが定理証明系の上で証明されています。どちらも数学者の人力では証明の検証が難しい問題です。
それとは別に、ソフトウェアが満たすべき仕様を述語論理で記述して、プログラムを実装し、実装が仕様を満たすことを証明出来ます。ユニットテストなどのテストでは網羅的でなかったりなどの問題がありますがCoqを使えばそのような問題はありません。
では、そんな素晴らしいツールがなぜ世の中で広く使われていないのかというと...単純に証明を書くのは難しいからです。Coqで証明を書くにはCoqの技術を磨く必要があります。
そしてその機会が、今回のセミナーという訳です。

セミナーは、葉山のセミナーハウスにて合宿形式５日間コース（半日の鎌倉見物含む）で開催され、内容はCoqの開発元のINRIAから訪れた講師によるCoqチュートリアルでした。
朝から夕食の時間までCoqに関する授業あるいは課題による実習、その後も解けなかった問題を寝るまで解く、というハードな毎日でした。私自身はここんとこあまりCoqで何かを証明してなかったので、多少錆び付いていたCoqのスキルを取り戻す良い機会でした。

残念ながら講義資料は参加者以外に公開されていない様です（パスワードで保護）。ただ、Coq については名古屋のProofCafeや、東京だとSF読み進捗ダメです会議 #9 #readcoqart #Coq(こちらは私も参加しています)といった勉強会が定期開催されているので、興味があれば参加されるとCoqについて学べると思います。

[IVA] Chapter 2, Section 7, Exercise 7,13

Exercise 1.

計算問題故パス

Exersise 7.

monomial order を固定し、ideal $I$ のminimal Groebner base $G$, $\tilde{G}$ について、

a. LT($G$) = LT($\tilde{G}$) を示せ。

$G=\{g_1, \cdots, g_t\}$, $\tilde{G} = \{\tilde{g}_1, \cdots, \tilde{g}_{t'}\}$ とする。monomial order に従って、$g_1 \geq g_2 \geq \cdots$, $\tilde{g}_1 \geq \tilde{g}_2 \geq \cdots$ と仮定して良い。

$G$, $\tilde{G}$ はグレブナ基底だから $\langle \mathrm{LT}(G) \rangle = \langle \mathrm{LT}(\tilde{G}) \rangle = \langle \mathrm{LT}(I) rangle$.

$\mathrm{multideg}(\mathrm{LT}(g_1)) = \alpha_1$,  $\mathrm{multideg}(\mathrm{LT}(\tilde{g}_1)) = \tilde{\alpha}_1$ とする。

$$LT(\tilde{g}_1) = \sum_i f_i \mathrm{LT}(g_i)$$
と書けるから、$\tilde{\alpha}_1 \geq \alpha_1$ 逆も同様に言えるから $\alpha_1 \geq \tilde{\alpha}_1$ よって $\tilde{\alpha}_1 = \alpha_1$ である。LCは全て$1$ゆえ$\tilde{\mathrm{LT}(g_1)} = \mathrm{LT}(g1)$. $\mathrm{LT}(G)-\mathrm{LT}(g_1)$, $\mathrm{LT}(\tilde{G})-\mathrm{LT}(\tilde{g})_1$ について同様に議論でき、$\mathrm{LT}(G)=\mathrm{LT}(\tilde{G})$.

b. $G$ と $\tilde{G}$ が同じ数の要素を含む事を示せ。

a. より LT($G$) と LT($\tilde{G}$) は同じ数の元を持つ事が判る。仮に $| \tilde{G} | \;\gt \; | G |$  とすると、$\tilde{G}$ には LT が等しい事なる元が存在することになるが、それは minimal Groebner basis であることに矛盾する。よって$| \tilde{G} | = | G |$ .

Exercise 13.

$F$ がグレブナ基底で無い場合は、$F=(f_1, \cdots,f_s)$ を順序付きタプルと考える必要がある。
$\bar{f}^F = 0$ ならば $f = \sum_i h_i f_i$ と書ける。このとき、$F' = F \cup \tilde{f}$ とすると、$f = \sum_i h_i f_i + 0 \cdot \tilde{f}$ ゆえ $\bar{f}^{F'} = 0$.

[IVA] Chapter 2, Section 6, Exercise 1 and 7

Exercise 1

$I = \{0\}$ なら、$g=0$, $r=f$ として終わり。
$I \neq \{0\}$ とする。Section 5 Corollary 6 より$I$はグレブナー基底 $G=\{g_1, g_2, \cdots, g_t\}$ を持ち、グレブナー基底の定義より、$\langle \mathrm{LT}(g_1), \cdots, \mathrm{LT}(g_t) \rangle = \langle \mathrm{LT}(I) \rangle$.
すると Section 6 Proposition 1 の前提を見たいしているから成立。

Exercise 7

$$S(f,g) = \frac{x^\gamma}{\mathrm{LT}(f)}f -  \frac{x^\gamma}{\mathrm{LT}(g)}g $$

$$x_\gamma = \mathrm{LCM}(\mathrm{LM}(f), \mathrm{LM}(g))$$

$f = a_\alpha x^\alpha + \sum_{\alpha' < \alpha} a_{\alpha'} x^{\alpha'}$,
$g = a_\beta x^\beta + \sum_{\beta' < \beta} a_{\beta'} x^{\beta'}$ と書けるから

$$S(f,g) = \frac{x^\gamma}{a_\alpha x^\alpha}( a_\alpha x^\alpha + \sum_{\alpha' < \alpha} a_{\alpha'} x^{\alpha'}) - \frac{x^\gamma}{a_\beta x^\beta}( a_\beta x^\beta + \sum_{\beta' < \beta} a_{\beta'} x^{\beta'})$$

$$= \sum_{\alpha' < \alpha} \frac{a_{\alpha'}}{a_\alpha} x^{\gamma - \alpha + \alpha'} +  \sum_{\beta' < \beta}\frac{a_{\beta'}}{a_\beta} x^{\gamma - \beta + \beta'} = \sum_{\gamma' < \gamma}c_{\gamma'} x^{\gamma'}$$

よって $\mathrm{multideg}(f,g) < \gamma$.

[Math] Memo

twitter 上で出ていた問題を考えてみた。

赤黒のルーレットを100回行なったとき、５回連続で同じ色が出ない確率を求めよ、という問題。
$n$回行なったときの上記の確率を$p_n$とする。
初回の色をA、Aでない色をBとするとき、2回目以降のパターンが

• AAAA -> NGケース $\frac{1}{16} \times 0$
• AAAB -> $\frac{1}{16} p_{n-4} =$ AAAB というパターンが起きる確率 x B以降OKな確率
• AAB -> $\frac{1}{8} p_{n-3}$
• AB -> $\frac{1}{4}p_{n-2}$
• B -> $\frac{1}{2} p_{n-1}$ 

よって $p_n = \frac{1}{2}p_{n-1} + \frac{1}{4}p_{n-2} + \frac{1}{8}p_{n-3} + \frac{1}{16}p_{n-4}$
明らかに$p_1 = p_2 = p_3 = p_4 = 1$
あとは$p_5, \; p_6, \; \cdots$ と順次数値計算すると $p_{100}$ = 0.028310329886357316 となる。つまり97% ぐらいの確率で、５連続パターンはどこかで発生する。

[IVA] Chapter 2, Section 5, Exercise 1, 7, 13

Exercise 1

$g_1 = xy^2 - xz + y$, $\mathrm{LT}(g_1) = xy^2$
$g_2 = xy - z^2$, $\mathrm{LT}(g_2) = xy$

$g_3 = x-yz^4$, $\mathrm{LT}(g_3) = x$

lex 順序で考えるから$x$ の次数が $0$ であるような $g$ を作れば良い。
$g = -g_2 + y g_3 = -xy+z^2 + y(x-yz^4) = z^2 - y^2z^4$ とすると $\mathrm{LT}(g) = y^2z^4$.
$g \in I = \langle g_1, g_2, g_3 \rangle$ であるが $\mathrm{LT}(g) \notin  \langle \mathrm{LT}(g_1), \mathrm{LT}(g_2), \mathrm{LT}(g_3) \rangle$

Exersise 7

$g_1 = x^4y^2 - z^5$, $\mathrm{LT}(g_1) = x^4y^2$
$g_2 = x^3y^3 -1$, $\mathrm{LT}(g_2) = x^3y^3$

$g_3 = x^2y^4-2z$, $\mathrm{LT}(g_3) = x^2y^3$

$g = yg_2 - xg_3 = 2xz-y$ は $g \in I$ ゆえ $2xy \in \mathrm{LT}(I)$.

しかし $2xy \notin \langle x^4y^2, x^3y^3, x^2y^4 \rangle$ ゆえグレブナー基底ではない

Exercise 13

Exercise 1-4-14 の結果を用いると、$I(V_1) \subset I(V_2) \subset I(V_3) \subset \cdots$ に対して、$\exists N \geq 1, \; \mathrm{s.t.} \; I(V_N) = I(V_{N+1}) = \cdots$ が存在する事と同値。

これは定理7より明らか。

[IVA] Chapter 2, Section 4, Exercise 1, 7, 13

Exercise 1. $I \subset k[x_1, \cdots, x_n]$ がイデアルであり、$f \in \sum_{\alpha} c_{\alpha} x^{\alpha}$ に対して $\forall \alpha, \; x^{\alpha} \in I$ である。このとき $I$ が単項式イデアルであることを示せ。

$$A = \cup_{f \in I} \cup_{f=\sum_{\alpha}c_{\alpha}x^{\alpha}} \alpha$$

という集合をとる。
すると任意の $I$ の元 $f$ に対して、$f = \sum_{\alpha}c_{\alpha}x^{\alpha}$ と有限和で表す事が出来るがこの各$\alpha$ は$A$ の元であり、各$c_{\alpha}$ は$k[x_1, \cdots, x_n]$ の元であるから、$h_\alpha = c_\alpha$ ととれば任意の$I$の要素$f$ は$f = \sum_{\alpha \in A} h_\alpha x^\alpha$ と有限和で書ける。よって$I=\langle x^\alpha \; : \; \alpha \in A \rangle$ という単項式イデアルである。


Exercise 7.

$n$ についての数学的帰納法を用いる。

$n=1$ のとき、$A \subset \mathbb{Z}_{\geq 0}$ だが、$\geq$ の性質より $A$ には最小限 $\beta$ があり、$\forall \alpha \in A, \; \exists \gamma \in  \mathbb{Z}, \; \alpha = \beta + \gamma$ となるから $\alpha(1) = \beta$ とすればよい。

$n=k$ までなりたつとして$n=k+1$ とする。
記法の都合上、$\mathbb{Z}^{k+1}_{\geq 0}$  から、$\mathbb{Z}^k_{\geq 0}$, $\mathbb{Z}_{\geq 0}$ への射影 $\pi_1$, $\pi_2$ と、逆方向の埋め込み写像 $\iota_1$, $\iota_2$ を下記の様に定める。

$$\pi_1 \; : \; \mathbb{Z}^{k+1}_{\geq 0} \ni (\alpha_1, \cdots, \alpha_k, \alpha_{k+1}) \mapsto
 (\alpha_1, \cdots, \alpha_k) \in \mathbb{Z}^k_{\geq 0}$$
$$\pi_2 \; : \; \mathbb{Z}^{k+1}_{\geq 0} \ni (\alpha_1, \cdots, \alpha_k, \alpha_{k+1}) \mapsto  \alpha_{k+1} \in \mathbb{Z}_{\geq 0}$$

$$\iota_1 \; : \; \mathbb{Z}^k_{\geq 0} \ni (\alpha_1, \cdots, \alpha_k) \mapsto
 (\alpha_1, \cdots, \alpha_k, 0) \in \mathbb{Z}^{k+1}_{\geq 0}$$

$$\iota_2 \; : \; \mathbb{Z}_{\geq 0} \ni \alpha_{k+1} \mapsto
 (0, \cdots, 0, \alpha_{k+1}) \in \mathbb{Z}^{k+1}_{\geq 0}$$

$\mathbb{Z}^k_{\geq 0}$, $\mathbb{Z}_{\geq 0}$ における単項式順序は $\iota_1$, $\iota_2$ と$\mathbb{Z}^{k+1}_{\geq 0}$における$\geq$ を用いて定める。

$\pi_1(A) \subset \mathbb{Z}^k_{\geq 0}$ を考えると、帰納法の仮定より有限個の$\alpha(1), \cdots, \alpha(s) \in \mathbb{Z}^k_{\geq 0}$が存在して、

$$\forall \alpha \in A, \; 1 \leq \exists i \leq s, \; \gamma \in  \mathbb{Z}^k_{\geq 0}, \; \alpha = \alpha(i) + \gamma$$

各 $\alpha(1), \cdots, \alpha(s)$ に対して $\pi_2(\iota_1(\alpha(i)) \cap A)$ という集合を考えると、それぞれに最小限 $\beta(i) \in  \mathbb{Z}_{\geq 0}$ が存在する。添字を付け替えて $\beta(1) \leq \cdots \leq \beta(s)$ となるように並べ替えて良い。

ここで、任意の $\alpha \in A$ s.t. $\alpha_{k+1} \geq \beta(s)$ について、$\exists j, \; \pi_1(\alpha) = \pi_1(\alpha(j)) +   \mathbb{Z}^k_{\geq 0}$ であり、$\beta_j \leq \beta_s$ ゆえ、$\alpha = \alpha(j) +  \mathbb{Z}^{k+1}_{\geq 0}$ が言える。

残りは $\beta_1 \leq \alpha_{k+1} \leq \beta_s$ の場合である。

$j = \beta_1 , \cdots, \beta_s$ について、$A_j = \{\alpha \in A \; | \; \alpha_{k+1}=j \}$ というスライスを考える。各スライスについて帰納法の仮定より有限個の $\{\alpha_ji \in  \mathbb{Z}^{k+1}_{\geq 0} \}$ が存在するので、それらを集めれば良い。

無駄を減らすことを考えるなら、高さ($k+1$座標)$=j+1$ のスライスの $\alpha_{(j+1)i}$ の中で、$\alpha_{j' i} +  \mathbb{Z}^{k+1}_{\geq 0}$ と表せるものは除外出来る。

[IVA] Chapter 2, Section 3, Exercise 11

前回、ちゃんと解けなかったので。

c. 除算アルゴリズムによって $f=a_1 f_1 + \cdots + a_s f_s + r$ と得られたとする。

$f$ のLMを $x^{\beta}$ とするとき、$\beta \in \Delta_1 = \alpha(1) + \mathbb{Z}^n_{\geq 0}$ であるならば、ある$\gamma \in  \mathbb{Z}^n_{\geq 0}$ が存在して $x^{\beta} = x^{\alpha(1)} x^{\gamma}$ となるから、

$$a_1 \rightarrow a_1 + \frac{\mathrm{LT}(f)}{\mathrm{LT}(f_1)}, \; f \rightarrow f - \frac{\mathrm{LT}(f)}{\mathrm{LT}(f_1)}f_1$$

を繰り返す事で、$\mathrm{multideg}(f) \notin \Delta_1$ と出来る。

$f \leftarrow f - a_1 f_1$ とすると、上の議論より $\mathrm{multideg}(f) \notin \Delta_1$。

同様にして、もし $\mathrm{multideg}(f) \in \Delta_2$  ならば、

$$a_2 \rightarrow a_2 + \frac{\mathrm{LT}(f)}{\mathrm{LT}(f)}, \; f \rightarrow f_2 - \frac{\mathrm{LT}(f)}{\mathrm{LT}(f_2)}f_2$$

を繰り返す事で、$\mathrm{multideg}(f) \notin \Delta_2$ と出来る。

$\mathrm{multideg}(f)$ が $\Delta_1, \Delta_2, \cdots, \Delta_s$ のどれにも含まれない場合は、$r \rightarrow r + \mathrm{LT}(f), \; f \rightarrow f -  \mathrm{LT}(f)$ とするが、これは $\mathrm{multideg}(f) \in \bar{\Delta}$ である $\mathrm{LT}(f)$ を $r$ へと移動して、次の項について、$\Delta_1, \cdots, \Delta_s, \bar{\Delta}$ のどれに属すか探索を繰り返すことと等しい。

d. 唯一である事を示す。

$f = a_1 f_1 + \cdots a_s f_s + r = a_1' f_1 + \cdots a_s' f_s + r'$ と書けたとする。

仮定より $\mathrm{multideg}(f - a_1 f_1), \mathrm{multideg}(f - a_1' f_1),  \notin \Delta_1$ であるが、$a_1 \neq a_1'$  とすると $(a_1 - a_1')f_1 \in Delta_1$ であるから矛盾。よって $a_1 = a_1'$ 。

同様にして $a_2 = a_2', \; \cdots, a_s = a_s'$ であることを示す事が出来、その結果 $r=r'$。

  

[IVA] Chapter 2, Section 3, Exercise 1, 6, 11

Exercise 1

2変数版を暫定的にscalaで書きました
http://ideone.com/BUbIU8

grlex

f divMod List(f1,f2)
res7: (List[foo.Poly2], foo.Poly2) = (List(
1x^6+1x^2,
),
1x^7+1x^3+-1y+1)

f divMod List(f2,f1)                          
res8: (List[foo.Poly2], foo.Poly2) = (List(
, 
1x^6+1x^2),
1x^7+1x^3+-1y+1)

lex

f divMod List(f1,f2)                          
res7: (List[foo.Poly2], foo.Poly2) = (List(
1x^6+1x^5y+1x^4y^2+1x^4+1x^3y+1x^2y^2+2x^2+2xy+2y^2+2,
1x^6+1x^5y+1x^4+1x^3y+2x^2+2xy+2),
2y^3+-1y+1)


f divMod List(f2,f1)
res8: (List[foo.Poly2], foo.Poly2) = (List(
1x^6y^2+1x^5y^5+1x^4y^8+1x^3y^11+1x^2y^14+1x^2y^2+1xy^17+1xy^5+1y^20+1y^8,
),
1y^23+1y^11+-1y+1)


Exercise 6

$g = 2x(2xy^2-x) - 3y(3x^2y - y -1) = -3x^2 + 2y^2 + 2y \in \langle 2xy^2-x, \; 3x^2y - y -1 \rangle$
であることは明らかだが、grlex 順序の元では、LTを考えると
$g = 0 \dot (2xy^2-x) + 0 \dot ((3x^2y - y -1) + g$ と除算されるのは明らか。

Exercise 11

あんまり厳密に証明出来ませんでした。

a. 数学的帰納法で示す

$i=1$ の場合、
$\beta \in \Delta_1 = \alpha(1) +  \mathbb{Z}^n_{\geq 0}$ ゆえ、ある $\gamma \in \mathbb{Z}^n_{\geq 0}$ が存在して $\beta = \alpha(1) + \gamma$ よって割り切れる。
$j
$i=k$ まで成り立つとして$i=k+1$ の場合を考える。
$$\beta \in \Delta_{k+1} = (\alpha(k+1)+ \mathbb{Z}^n_{\geq 0}) - \cup_{i=1}^k \Delta_i$$
ある $1 \leq j \leq k$ が存在して $\beta \in \Delta_j$ と仮定すると、
$\beta \in  \cup_{i=1}^k \Delta_i$ ゆえ $\beta \notin \Delta_{k+1}$ となって矛盾。故にそのような $j$ は存在しない。すると$x^{\alpha(k+1)}$が$x^{\beta}$を割り切る事はあきらか。
また$j < i$のとき$\alpha(j) \in \Delta_j$ ゆえ$x^{\alpha(j)}$が$x^{\beta}$を割り切るなら、$\beta \in \Delta_j$ となるが同様に$\beta \notin \Delta_{k+1}$となる。

b. $s^{\alpha(i)}$ が $x^{\gamma}$を割り切るなら$\gamma \in \Delta_i$である。よって$\gamma \in \bar{\Delta}$ であるならばどの 
$x^{\alpha(i)}$ も$x^{\gamma}$を割り切らない。

c. $\beta + \alpha(i) \notin \Delta_i$ とする。するとa.より、$x^{\beta+\alpha(i)$ を $x^{\alpha(i)}$ が割り切らない、ある$j < i$ が存在して $x^{\beta+\alpha(i)}$ を $x^{\alpha(j)}$ が割り切るか、となるが、前者はありえないので後者。
すると$f=a_1f_1+\cdots+a_jf_j+\cdots$ という分解において、$a_j$ を $a_j + c x^{\beta+\alpha(i)-\alpha(j)}$ の様に修正する事で $i$ について考察する時の $f$ の $\beta+\alpha(i)$ の項を消せる。よって$\beta + \alpha(i) \in \Delta_i$ と出来る。

d. このセクションで作った除算アルゴリズムがそのアルゴリズム、なんだがどう示したものか。

[IVA] Chapter 2, Section 2, Exercise 1,7

Exercise 1.

a. $f(x,y,z) = 2x + 3y + z + x^2 - z^2 + x^3$

lex: $x^3 + x^2 + 2x + 3y - z^2   + z$, $\mathrm{LM}(f) = x^3$, $\mathrm{LT}(f) = x^3$, $\mathrm{multideg}(f) = (3,0,0)$
grlex: $x^3 + x^2 - z^2 + 2x + 3y + z$, $\mathrm{LM}(f) = x^3$, $\mathrm{LT}(f) = x^3$, $\mathrm{multideg}(f) = (3,0,0)$
grevlex: $x^3 - z^2 + x^2 + z + 3y + 2x$, $\mathrm{LM}(f) = x^3$, $\mathrm{LT}(f) = x^3$, $\mathrm{multideg}(f) = (3,0,0)$

b. $f(x,y,z) = 2x^2y^8 - 3x^5yz^4 + xyz^3 - xy^4$

lex : $-3x^5yz^4 + 2x^2y^8  - xy^4 + xyz^3$, $\mathrm{LM}(f) = x^5yz^4$, $\mathrm{LT}(f) = -3x^5yz^4$, $\mathrm{multideg}(f) = (5,1,4)$
grlex : $-3x^5yz^4 + 2x^2y^8 - xy^4 + xyz^3$, $\mathrm{LM}(f) = x^5yz^4$, $\mathrm{LT}(f) = -3x^5yz^4$, $\mathrm{multideg}(f) = (5,1,4)$
grevlex : $2x^2y^8 -3x^5yz^4 - xy^4 + xyz^3$, $\mathrm{LM}(f) = x^2y^8$, $\mathrm{LT}(f) = 2x^2y^8$, $\mathrm{multideg}(f) = (2,8,0)$

Exercise 7.

$>$ が monomial order であるとする。

a. $\alpha > 0$ for all $\alpha \in \mathbb{Z}_{\geq 0}^n$ を示せ。

ある $\beta = (\beta_1, \cdots, \beta_n) \in \mathbb{Z}_{\geq 0}^n$ が存在して $0 > \beta$ と仮定する。すると $0 + \beta > \beta + \beta$ となるから$\beta$を繰り返し加算する事で無限降下列 $\{\beta, 2\beta, 3\beta, \cdots\}$ を作れるがこれは$>$がwell-orderingであることと矛盾する。よって$\forall \beta, \; \beta \geq 0$ である。

b. $x^{\alpha}$ が $x^{\beta}$ を割り切るなら $\alpha \leq \beta$ を示せ。逆は成立するか？

 題意より単項式 $x^{\gamma}$ があって $x^{\beta} = x^{\alpha}x^{\gamma}$ と書けるが、$\beta = \alpha + \gamma$ であり、$\gamma \geq 0$ であるから$\beta \geq \alpha$.

成立しない。反例は例えば $x^{\alpha}=x, \; x^{\beta}=y^2$

c. $\alpha \in  \mathbb{Z}_{\geq 0}^n$ なら$\alpha$ が $\alpha + \mathbb{Z}_{\geq 0}^n$ の最小元である事を示せ。

任意の $\beta \in \mathbb{Z}_{\geq 0}^n$ に対して、$\beta \geq 0$ より $\alpha + \beta \geq \alpha$. よって $\alpha$ は最小元。

FLOPS2014報告

　FLOPS2014 に行ってきました、といっても発表しに行った訳でなく単に話を聞きに行っただけなんですが。

　FLOPS 2014 は二年に一回、日本で開催される関数型および論理型プログラミングに関する国際会議です。今年は6/4-6の日程で石川県金沢市で開催されました。
　弊社はアドテクの会社で開発言語もScalaだったりと、まぁほとんど会社の業務と関係無いのだけど、やはりせっかく日本で関数型言語の国際会議があるなら是非聞きに行かないとね、ということで聞きに行きました。

　以下、感想などです。各発表内容に関しては、プログラムのページから発表スライドを見る事ができるはず。

第１日目

★ "Liquid Types For Haskell" 招待講演
　今回のFLOPSで一番興味を持っていたのがこの話です。
　Liquid = Logically Qualified Data の略、のつもりらしく、liquid type というのは、{v: Int | v >= 0} の様に、論理式で修飾された型のことです。Coq などの依存型を用いた定理証明系でもこのような述語を伴った型を使ってプログラミングを出来るところは同じなのですが、liquid type は述語を決定可能なPresburger算術の範囲に限定し、SMTソルバーを用いて自動証明をさせようというところが大きく違います。まぁCoqの証明を書くのは大変だし、開発の現場で必要とされる検証課題はほぼPresburger算術で充分なのだとしたら、自動証明の方が普及までの敷居が低いのは自明。
　LiquidHaskell がどんなものか試したい人はオンラインでどんなものか試すことが出来ます。
liquid type の型定義は、{-@ type Even = {v:Int | v mod 2 = 0} @-} みたいにHaskell のコメントとして、実際のHaskellのコードに註釈します。すると double xs = [x + x | x <- code="" xs=""> のようなHaskellの実装について、{-@ double :: [Nat] -> [Even] @-} の様な仕様を満たすことを自動証明してくれる、というのを試せます。 個人的には Coq で証明を書くの好きなんだけど、やはり前の会社(SIer)や今の会社で仕事をしてみた印象としては、自動証明器も必要なのかなぁとも思います。ならば Why3 とか使って開発すれば良いかなとも思うけど、Haskell みたいに既にメジャーな言語でこの手のツールが使えるというのは、やはり強みなのかなぁと思います。

他の発表は簡単に（というか専門家じゃないから解説なんか出来ない）。詳しくは、proceedings読んで下さい。

★ "PrologCheck - property-based testing in Prolog"
　オブジェクト指向言語界隈では具体的なテストケースに対してユニットテストをすることが多い様ですが、関数型言語ではランダムにテストデータを生成して仕様（＝満たすべき性質）を満たすことを確認するようなproperty-baseのテストツールが標準的です。（ScalaでもScalaCheckというのが有りますが、開発現場ではあまり使われてないみたい。勿体ない話です。）
　で、Prolog版のを作った、という話（だと思う）。

★ "Generating Constrained Random Data with Uniform Distribution"
　で、その手の XXX Check系のテストツールには、「もし入力データが◯◯という性質を満たすなら△△」みたいなのをテスト出来るのですが、◯◯という条件を満たすランダム入力データを作るのはなかなか面倒だったりします。その辺を工夫したよ、という話（だと思う）。

★ "Guided Type Debugging"
　関数型言語のエラーメッセージは、（C++ほどではないと思ってはいますが）Javaとかに比べると判りにくいところがあります。その原因の一つの、型の不整合の時のエラーのデバッグを容易にしようとする工夫（だと思う）。

★ "Using big-step and small-step semantics in Maude to perform declarative debugging"
　Maude (という項書き換え系言語)の上に、何か言語の big-step あるいは small-step semantics を定義して実行とかデバッグとか出来るフレームワークを作った、という研究の様に思えた。確かに small-step semantics とか Maude の上に定義すると便利そうに思えますね。

★ "Faustine: a Vector Faust Interpreter Test Bed for Multimedia Signal Processing - System Description -"
　Faust というのは信号処理用のDSLらしいのですが、これを使ったギターアプリ(タブレット上で動くギター風に演奏出来るアプリ)の動画デモが。こんな研究してる人もいるんだなー、と思いました。

★ "The Design and Implementation of BER MetaOCaml: System Description"
★ "On Cross-Stage Persistence in Multi-Stage Programming"
　MetaOCaml というのは OCaml を拡張して型安全 eval を使える様にしたようなものなのですが、それに関する発表が２件。

第２日目

★ "Programming Language Methodologies for Systems Verification" 招待講演
　L4 microkernel を作ってる研究機関での形式手法仕様に関する報告。当初OS班と形式手法班がIsabelle/HOLを使おうとして失敗し、Haskellを両者の共通言語として選択したら成功して、両者の共通言語としてのHaskellからIsabellあるいはC++を作る様になった（しかしその後、各班がHaskellをメンテしなくなって云々）みたいな報告。
　この手の話聞くと、OS班とはいえ研究者の方々でも、やはり Isabelle などの形式手法（定理証明系）とかで仕様記述するの嫌なのか、と思ってしまいますね。。。IsabelleはZとかほど抽象的ではないと思うのだけれどなぁ。あと、線形型は勉強した方が良さそうだなと思った。

★ "Lightweight higher-kinded polymorphism"
　OCamlには無いhigher-kinded polymorphismをdefunctionalizationすることで実現したよ、という話。

★ "Generic Programming with Multiple Parameters"
　HaskellのGeneric programmingでパラメータを複数個使える様に、という話。うーむ、Haskellのgeneric programmingの話、ちゃんと復習しないとなー。

★ "Type-Based Amortized Resource Analysis with Integers and Arrays"
　計算量というリソースを型として表現するという話。こういうことも出来るのか、と。

★ "Linear Sized Types in the Calculus of Constructions"
　CoqのInductionの停止性、CoInductionのproductivityの判定の為に、それらを表現出来るような型を、という話。

★ "Dynamic Programming via Thinning and Incrementalization"
　ナップザック問題を例にとってDPの解法アルゴリズムを、融合変換とかアルゴリズム変換とかを使ってアルゴリズムを最適化する話。この手の話に興味がある人は、"semiring fusion" とか "第三準同型定理" とかのキーワードでググると良いと知人より教わりました。勉強すること多いなー。

★ "POSIX Regular Expression Parsing with Derivatives"
　微分を用いて正規表現を扱う話は知っていたのですが、POSIX準拠のはずの各種正規表現ライブラリが、どこで部分文字列をマッチすべきかについて正しく無い答えを返す、という話は知りませんでした。ちゃんとPOSIX仕様に基づいて、部分マッチ箇所を計算するアルゴリズムの話です。Proceedingsにはプレゼンでは端折ってあった箇所が書かれてて面白そうなので、あとでちゃんと復習しよう。

★ "Semantics for Prolog with Cut - Revisited"
　Cut有りのPrologのsemanticsをCoqでやってる、という話。すみません、Prolog良く解らないので、どの辺が重要なポイントなのか判りませんでした。

★ バンケット
　コース＋追加で寿司、天ぷら、日本酒という立派なバンケットでした。線形論理の話とか面白い話を聞けました。

第３日目

★ "Relating Computational Effects by TT-Lifting" 招待講演
　計算(computation)を扱う理論的枠組みとしてdenotational semanticsというのがあるのですが、圏論を使って色々統一的に議論出来るよという話で、最初は判る話だったんですが、後半はさすがに振り落とされました。が、こういう話聞くと、また圏論勉強しよう、という気分になりますね。

★  "A New Formalization of Subtyping to Match Subclasses to Subtypes"
　継承とジェネリクスと両方ある Java とか Scala みたいな言語だと、型宣言の際に共変反変の両方の制約を満たす為に(例えばScalaなら) sealed abstract class List[+A] extends ... { def ::[B >: A] (x: B): List[B] = ... } みたいなイディオムを使わざるを得ないとか色々不便なところもあるのですが、この論文は新しい subtyping の定式化をしてみたよという話。OO言語関係に近い話題はこの一件だけでした。Scala などに興味がある人は ECOOP とか聞きに行くべきなんですかね。。。

★ "Type Soundness and Race Freedom for Mezzo"
 Mezzo というのはML風の言語なんですが、線形型を用いることでマルチスレッドプログラミングでロック取得の必要性などをコンパイル時にチェック出来る様にした言語で、言語の正しさ(型検査が通ればデータ競合が起きない事)を Coq で証明した、という話。Java とか Scala とかだとプログラマが正しくロックを取ってる事を保証しなくてはいけないので、Mezzo のこういう機能は素晴らしいと思います。

★ "Proving Correctness of Compilers using Structured Graphs"
　木構造ではなく(非循環)グラフを用いてコンパイラを改善するみたいな話で、グラフを用いてコンパイル＆実行するのと、木も用いてとが等価だと言う証明の話（だと思う）。

★ "Constraint Logic Programming for Hedges: a Semantic Reconstruction"
　すみません、これは良く判りませんでした。semantics と solver のアルゴリズムについて話してたと思うのだが。

★ "How many numbers contains a lambda-term?"
　λ式でk-tupleとかを作った場合、λ式の型を決めると、そこに含む事の出来る自然数の個数には上限がある、という話（だと思う）。これも難しくて判りませんでした。

★ "AC-KBO Revisited"
　項書き換え系にはクヌース・ベンディックス完備化アルゴリズムという完備化アルゴリズムがありますが、結合則 x+(y+z) = (x+y)+z や交換則 x+y=y+x のような規則を満たす演算子に関する場合にどうするかという話。Steinbach という人の論文が間違っているという論文があったけど実はそれは正しくてみたいな話とか、順序付けがNP-hardなことはこうやってSATに変換してとか、（詳細は理解出来ない）門外漢にも楽しめる発表でした。

★ "Well-structured pushdown system: Case of Dense Timed Pushdown Automata"
　Timed Pushdown Automata の話でした。これも基礎知識が無くどういう話なのか良く判りませんでした。

終わりに

　社外勉強会の効能として、「今まで知らなかった話題に触れられる」「すごい人たちのやってるすごいことを知る」「もっと勉強しようというやる気を貰ってくる」といったことを主張する人は多いです。私もその意見に賛成します。
　だとしたら、学会とか国際会議に行けば、第一線の研究者がやっている最先端の話題を知る事が出来ます。
　そして、例えばHaskellとかOCamlなどは、言語の開発者がこういう学会で発表した事を言語の新機能として追加したりします。学会で話されている事は自分が使う機能と無関係な難しい話ばかり、という訳ではありません。
　
　勿論、聞いても分からない話も一杯有りますし、周りは見知らぬ研究者ばかりで話す相手も内容も無い、などなどというところはありますが、まぁその辺は我慢するとして。判らなかった内容とかは、各種勉強会とかに行って論文コピー片手に詳しそうな人に質問するとか方法はありますし。

　2016年のFLOPSは高知で春に開催だそうです。また PPL のような日本の学会とかなら敷居が低く感じるかと思います。

　社外勉強会に行く次のステップとして、学会とか国際会議を聞きに行くのを是非お勧めします。

[IVA] Chapter 1, Section 5, Exercise 1, 6, 13

Exercise 1.

$f \in \mathbb{C}[x]$ が $n = \mathrm{deg}f > 0$ なる多項式とすると定理1-1-7より$f(a_n)=0$ となる $a_n \in \mathbb{C}$ が存在する。
すると系1-5-3の議論と同様にして $f = q (x-a_n), \; q \in \mathbb{C}[x], \; \mathrm{deg} q = n-1$ となる。すると数学的帰納法より $f = q_0 (x-a_1) \cdots (x - a_n), \; \mathrm{deg} q_0 = 0$ となって$q_0$ は定数であるが、$f$ の最高次係数を $c$ とすると $q_0 = c$ となるのは明らか。

Exercise 7.

入力: $f_1, \cdots f_s$
 $f_1, \cdots f_s$ の中で最も次数の低いものを $f_i$ とする。(同じ次数のものが複数有る場合は添字$i$が最小のものを選択する。
$j = 1, \cdots s, \; i \neq j$ なる $j$ に対して $q_j = \mathrm{LT}(f_j) / \mathrm{LT}(f_i)$ から定まる$q_j$ を用いて$r_j = f_j  - q_j f_i$ として$f_j$ を $f_i$ で割った余りを求める。
$\{r_j \;|\; j=1,\cdots,s, j \neq i\}$ が全て$0$の場合、$\mathrm{GCD}=f_i$。
さもなければ $r_1, \cdots, r_{i-1}, f_i, r_{i+1}, \cdots, r_s$ の中で零多項式で無いもののみを選んで入力とする。

$\mathrm{deg} r_j < \mathrm{deg} f_i$ であるからループを回す毎に入力の次数は減少するため、アルゴリズムが停止する事が保証される。

Exercise 13.

$f = a_0 x^n + a_1 x^{n-1} + \cdots + a_{n-1}x + a_n $ とするとき、

$af = (a a_0) x^n + (a a_1) x^{n-1} + \cdots + (a a_n)$ ゆえ

$(af)' = n (a a_0) x^{n-1} + (n-1)(a a_1) x^{n-2} + \cdots + (a a_{n-1})$ ゆえ
$(af)' = a f'$

$n = \mathrm{max}(\mathrm{deg}f, \mathrm{deg}g)$ として$f,g$ を共に$n$次の$k[x]$と看做して、

$f = a_0 x^n + a_1 x^{n-1} + \cdots + a_{n-1}x + a_n $

$g = b_0 x^n + b_1 x^{n-1} + \cdots + b_{n-1}x + b_n $ とするとき、

$f+g = (a_0+b_0) x^n + (a_1+b_1) x^{n-1} + \cdots + (a_{n-1}+b_{n-1})x + (a_n+b_n) $

$(f+g)' = n(a_0+b_0) x^{n-1} +  \cdots + (a_{n-1}+b_{n-1}) = f' + g' $

上記より線形性が保証されるので、$f = x^n, \; g=x^m$ という単項式について考えれば充分である。
$(fg)' = (x^{n+m})' = (n+m)x^{n+m-1}$
$f'g + fg' = nx^{n-1}x^m + x^n mx^{m-1} = (n+m)x^{n+m-1}$
よって示せた。

[IVA] Chapter 1, Section 4, Exercise 1, 7, 13

Exercise 4-1
a)

$$ x^2 + y^2 -1 = 0 \;\;\; (1)$$
$$ xy -1 = 0 \;\;\; (2)$$

$$y = \frac{1}{x}$$ より$$ x^2 + \frac{1}{x^2} - 1 = 0$$
よって $ x^4 - x^2 + 1 = 0$

b)

$(1) \times x^2 - (2) \times (xy+1) = x^4+x^2y^2-x^2 - x^2y-2 + 1 = x^4 - x^2 + 1 = 0$

Exercise 4-7 任意の$n,m$ に対して $\mathbf{I}(\mathbf{V}(x^n, y^m)) = \langle x,y \rangle$ を示せ。

$$\mathbf{I}(\mathbf{V}(x^n, y^m)) = \left\{ f \in k[x,y] \;|\; f(a_1,a_2)=0 for \forall (a_1,a_2) \in \mathbf{V}(x^n, y^m) \right\}$$
$k$ は体であるから $a_1^n = 0, \; a_2^m = 0$ iff $a_1=a_2=0$
よって

$$\mathbf{I}(\mathbf{V}(x^n, y^m)) = \left\{ f \in k[x,y] \;|\; f(0, 0) = 0 \right\}$$

$\forall f \in \langle a,y \rangle$ を取る。$f(x,y) = h_1(x,y) x + h_2(x,y) y$ と書け $f(0,0) = 0$ となるから $f \in \mathbf{I}(\mathbf{V}(x^n, y^m))$ よって $ \mathbf{I}(\mathbf{V}(x^n, y^m)) \supset  \langle a,y \rangle$

逆に $\forall f \in \mathbf{I}(\mathbf{V}(x^n, y^m))$ を取る。$f(0,0)=0$ である。
$$f = \sum_{i,j=0}^{n_x,n_y} a_{ij} x^i y^j$$
と書くと、$f(0,0)=0$ より $a_{00} = 0$
すると
$$f = (\sum_{i>0}a_{ij} x^{i-1}y^j)x + (\sum_j a_{0j}y^{j-1})y$$
と書けるゆえ、$ f \in \langle x,y \rangle$ よって $ \mathbf{I}(\mathbf{V}(x^n, y^m)) \subset  \langle x,y \rangle$

故に　$ \mathbf{I}(\mathbf{V}(x^n, y^m)) =  \langle x,y \rangle$

Exercise 4-13
$I \subset \mathbb{F}_2[x,y]$ を $\mathbb{F}_2^2$ 上のすべての点で零となる多項式のイデアルとする。

a. $\langle x^2-x, y^2-y \rangle \subset I$ を示せ。

$\langle x^2-x, y^2-y \rangle$ がイデアルであることを示すのは省略。
$\forall f \in \langle x^2-x, y^2-y \rangle$ を取ると、
$f = h_1 (x^2-x) + h_2(y^2-y)$ となる $h_1, h_2 \in \mathbb{F}_2[x,y]$ が存在する。
任意の $\forall a = (a_1,a_2) \in \mathbb{F}_2^2$ に対して
$f(a) = h_1(a)(a_1^2-a_1) + h_2(a)(a_2^2-a_2) = 0$ より$f \in I$
よって $\langle x^2-x, y^2-y \rangle \subset I$

b.任意の$f \in \mathbb{F}_2[x,y]$ に対して $f = A(x^2-x) + B(y^2-y) + axy+bx+cy+d$ と書けることを示せ。

$\forall f \in \mathbb{F}_2[x,y]$ を取る。$y$ の次数で整理して
$$f = \sum_i p_i(x) y^i$$
と書ける。ここで $y^2=(y^2-y) + y$, $y^3=(y+1)(y^2-y) + y$ の様に書けるから
$f = B(y^2-y) + p(x)y + q(x)$ と変形出来る。
更に $p(x), q(x)$ にも同様の変形を行うと
$p(x)y = (A_p(x^2-x) + p_1 x + p_0)y$, $q(x) = A_q(x^2-x) + q_1x+q_0$ と書けるから整理すれば
$f = A(x^2-x) + B(y^2-y) + axy+bx+cy+d$ と書ける。

c. $axy + bx + cy + d \in I$ iff $a=b=c=d=0$ を示せ。

$x=y=0$ を代入して$d = 0$
$x=0, y=1$ を代入して $c=0$
$x=1, y=0$ を代入して $b=0$
$a=y=1$ を代入して $a=0$

d.  $\langle x^2-x, y^2-y \rangle \supset I$ を示せ。（a と合わせて  $\langle x^2-x, y^2-y \rangle = I$）

任意の $f \in \mathbb{F}_2[x,y]$ に対して b より $f = A(x^2-x) + B(y^2-y) + axy+bx+cy+d$ と書ける。そして $f \in I$ とすると c より$a=b=c=d=0$。
従って $f = A(x^2-x) + B(y^2-y)$ と書けるゆえ $f \in \langle x^2-x, y^2-y \rangle$
よって$I \subset \langle x^2-x, y^2-y \rangle$

e.

$x^2y+xy^2 = y(x^2-x) + x(y^2-y) + 2xy =  y(x^2-x) + x(y^2-y) \in  \langle x^2-x, y^2-y \rangle$

[IVA] Chaper 1, Section 3, Exercise 1, 7, 13

Exercise 1.
\begin{eqnarray}
x + 2y - 2z + w & = & -1 \\
x + y + z - w & = & 2
\end{eqnarray}
変形して
\begin{eqnarray}
x + 2y & = & -2z - w - 1 \\
x + y & = & -z + w + 2
\end{eqnarray}

解いて

\begin{eqnarray}
x & = & -4z + 3w + 5 \\
y & = & 3z - 2w - 3
\end{eqnarray}

Exercise 7.
$\mathbb{R}^n$ の$x_n$軸上の点 $(0, \cdots, 0, 1)$ から $x_1 \cdots x_{n-1}$ 超平面上の点 $(u_1, \cdots, u_{n-1}, 0)$ を通る様に伸ばした直線と、超球面 $x_1^2 + \cdots x_n^2 = 1$ との交点の座標を求めると、
\begin{eqnarray}
x_i &=& \frac{u_i}{u_1^2 + \cdots + u_{n-1}^2 + 1}t \;\; (1 \leq i \leq n-1) \\
x_n &=& \frac{-1}{u_1^2 + \cdots + u_{n-1}^2 + 1}t + 1
\end{eqnarray}
解いて $t=0, 2$ だが前者は自明な解であり、求めるものは後者。よって
\begin{eqnarray}
x_i &=& \frac{2 u_i}{u_1^2 + \cdots + u_{n-1}^2 + 1} \;\; (1 \leq i \leq n-1) \\
x_n &=& \frac{u_1^2 + \cdots + u_{n-1}^2 - 1}{u_1^2 + \cdots + u_{n-1}^2 + 1}
\end{eqnarray}

Exercise 13.

$$x = 1 + u - v$$

$$y = u + 2v$$

$$z = -1 -u + v$$

整頓して

$$(x,y,z) = (1,0,-1) + u(1,1,-1) + v(-1,2,1)$$

$$(1,1,-1) \times (-1,2,1)  = (3, 0, 3)$$

よって求める平面の法線ベクトルは $(3,0,3)$ に平行な $(1,0,1)$ と取れば良く、点$(1,0,-1)$ を通るため、求める方程式は $x-z=2$

[IVA] Chapter 1, Section 2

Exercise 3.

$\mathbf{V}(x^2+y^2-4) \cap \mathbf{V}(xy-1)$ を描け。

$x^2+y^2-4 = 0$ ゆえ $x^2 + y ^2 = 2^2$。よって前者は中心 $(0,0)$ 半径 $2$ の円。
$xy -1 = 0$ ゆえ $y = \frac{1}{x}$。よって後者は軸が $x=0, \; y=0$ である双曲線。
この交わりは有限個の点の集合。

交点の座標は $y = \frac{1}{x}$ を $x^2 + y^2 -4 = 0$ に代入して解けば良い。
$ x^2 - 4 + \frac{1}{x^2} = 0 $ より $x^2 = 2 \pm \sqrt{3}$。
対応する$y$ は $y^2 = \frac{1}{x^2} = 2 \mp \sqrt{3}$。
$$\sqrt{2\pm\sqrt{3}} = \frac{\sqrt{6}\pm\sqrt{2}}{2}$$
であるから、

$$\begin{eqnarray}
(x,y) &=& \left( \frac{\sqrt{6}+\sqrt{2}}{2},  \frac{\sqrt{6}-\sqrt{2}}{2}\right), \\
& & \left( \frac{\sqrt{6}-\sqrt{2}}{2},  \frac{\sqrt{6}+\sqrt{2}}{2}\right), \\
& & \left( -\frac{\sqrt{6}+\sqrt{2}}{2},  -\frac{\sqrt{6}-\sqrt{2}}{2}\right), \\
& & \left( -\frac{\sqrt{6}-\sqrt{2}}{2},  -\frac{\sqrt{6}+\sqrt{2}}{2}\right)
\end{eqnarray}$$

Exercise 9.

$R$ が $\mathbb{R}[x,y]$ の多項式 $f_1, \cdots, f_s$ を用いて $\mathbf{V}(f_1, \cdots, f_s)$ と書けたと仮定する。
任意の $a \in \mathbb{R}$ に対して $g(y) = f_1(a,y)$ とする。
$R$ は上半平面であるから $g(1) = g(2) = \cdots = 0$ と、$g(y)=0$ は無限個の$y$に対して$0$になるため $g=0$ でなくてはならないが、下半平面の点 $(a,-1) \notin R$ について考えると、$g(-1) \neq 0 $ となって矛盾。
よってそのような $f_1$ は存在しない。

Exersise 15.

a) $V_i ; (1 \leq i \leq n)$ をvariety とする。$n=1$ のとき、
$$ \bigcup_{i=1}^n V_i = \bigcap_{i=1}^n V_i = V_1$$
ゆえ、variety である。$n$ まで成立するとして $n+1$ の場合に対して、
$$\bigcup_{i=1}^{n+1}V_i  = \left( \bigcup_{i=1}^{n} \right) \cup V_{n+1},$$

$$\bigcap_{i=1}^{n+1} V_i = \left( \bigcap_{i=1}^{n} \right) \cap V_{n+1}$$
ゆえ、$n+1$ 個の variety の 結び、交わりは variety である。
よって数学的帰納法により成立。

b) $a \in \mathbb{R}$ に対して $V_a = \left\{(x,a) \; | \; x \in \mathbb{R} \right\} = \mathbb{V}(y-a)$ は variety。このとき
$$ V = \bigcup_{a>0}V_a$$
を考えると $V$ は Exercise 9. の上半平面 $R$ に等しいが $R$ は variety ではない。

c) $V = \mathbf{V}(x-y), \; W = \mathbf{V}( (x-1)^2 + (y-1)^2 )$ と定義すると
$V - W = \left\{(x,x) \;|\; x \in \mathbb{R}, \; x \neq 1\right\}$
これは Exercise 10 より variety ではない。

d) $f_1, \cdots, f_s \in k[x_1, \cdots, x_n]$ の各 $f_i$ は $f_i \in k[x_1, \cdots, x_n, y_1, \cdots, y_m]$ と看做す事が出来る。$g_1, \cdots, g_t \in k[y_1, \cdots, y_m]$ についても同様。
このとき、$\mathbf{V}(f_1, \cdots, f_s, g_1, \cdots, g_s)$ を考えると、

$$(x_1, \cdots, x_n, y_1, \cdots, y_m) \in \mathbf{V}(f_1, \cdots, f_s, g_1, \cdots, g_s)$$
if and only if
$$f_i(x_1, \cdots, x_n, y_1, \cdots, y_m) = g(x_1, \cdots, x_n, y_1, \cdots, y_m)) = 0$$

であるから、$V \times W = \mathbf{V}(f_1, \cdots, f_s, g_1, \cdots, g_s)$

[Coq][Math] From left unit and left inverse to right unit and inverse

群で左単位元と左逆元があれば、右単位元と右逆元があることの説明。

Coq 演習で、Coq 以外のところで行き詰まっていた人がいたので参考になればと。

逆元と単位元の導入/除去のとこだけ詳しく書きますが、結合則使って演算順序を変えるところは各自 rewrite とかで頑張ってください。

$x 1 = 1 x 1 = \{(x^{-1})^{-1} x^{-1}\} x (x^{-1}x) = (x^{-1})^{-1} (x^{-1}x) x^{-1}x $
$ = (x^{-1})^{-1} 1 x^{-1} x = (x^{-1})^{-1} x^{-1} x = \{ (x^{-1})^{-1} x^{-1}\} x = 1 x = x$

$x x^{-1} = 1 x x^{-1} = \{ (x^{-1})^{-1} x^{-1} \} x x^{-1} $
$= (x^{-1})^{-1} (x^{-1}x) x^{-1} = (x^{-1})^{-1}  1  x^{-1}$
$= (x^{-1})^{-1} (1 x^{-1}) = (x^{-1})^{-1} x^{-1} = 1 $

[IVA] Chapter 1, Section 1, Exercise 4

Ideals, Varieties, and Algorithms の演習問題。

Chapter1, Section 1, Exersise 4: Let $F$ be a finite field with $q$ elements.  Adapt the argument of Exersise 3 to prove that $x^q - x$ is a nonzero polynomial in $F\left[x\right]$ which vanishes at every point of $F$.  This shows that Proposition 5 fails for all finite fields.

解答：
$F$ は要素数 $q$ の有限体であるから、$F - \left\{0\right\}$ は要素数 $q - 1$ の有限群となることは、体の定義より明らか。
$F - \left\{0\right\}$ の任意の要素 $x$ に対して、$x$ の位数が $q - 1$ の約数であることはラグランジュの定理より明らか。
すると前問 3b より、$x \neq 0$ ならば $x^{q-1} = 1$ より $x^q - x = 0$.
同様に $x = 0$ なら $x^q - x = 0$.
よって全ての $x \in F$ に対して $f(x) = x^q - x \; \in \; F_p\left[x\right]$ は零となる。