[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}$
よって示せた。