02 January, 2015

[Python] python環境構築

›
機械学習用のpython環境構築 MacでPythonの機械学習環境構築(2014年5月版) を参考にしました $ sudo brew update $ sudo brew install pyenv ~/.bash_profile に export PATH=...
06 December, 2014

[Coq] TPPmark2014 : Theorem Prover Advent Calendar

›
　 TPP (Theorem proving and provers for reliable theory and implementations) 2014 という定理証明系に関するワークショップがあり、毎年秋〜冬に日本で開催されています。  　TPPでは毎年TPPmar...
25 September, 2014

[IVA] Chapter 2, Section 9, Exercise 13

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

[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) = \s...
08 September, 2014

ProofSummit 2014 & JSSST Coq Tutorial

›
名古屋で開催された ProofSummit 2014  と、同じく名古屋大学で開催されている日本ソフトウェア科学会の チュートリアル：定理証明支援系Coq入門  に参加しました。 ProofSummit は各種の定理証明系(今年は Coq, Agda, Mizarの話がありま...

[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-...
01 September, 2014

NII Shonan School on Coq 参加報告

›
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{...
18 August, 2014

[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\}$ を持ち、グ...
11 July, 2014

[Math] Memo

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

[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)...
27 June, 2014

[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$ ...
1 comment:

[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...
23 June, 2014

[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...
16 June, 2014

[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...
10 June, 2014

FLOPS2014報告

›
　 FLOPS2014  に行ってきました、といっても発表しに行った訳でなく単に話を聞きに行っただけなんですが。 　FLOPS 2014 は二年に一回、日本で開催される関数型および論理型プログラミングに関する国際会議です。今年は6/4-6の日程で石川県金沢市で開催されました。...
02 June, 2014

[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の議論と...
26 May, 2014

[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$$ よって...
19 May, 2014

[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...
12 May, 2014

[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...
2 comments:
28 April, 2014

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

›
群で左単位元と左逆元があれば、右単位元と右逆元があることの説明。 Coq 演習で、Coq 以外のところで行き詰まっていた人がいたので参考になればと。 逆元と単位元の導入/除去のとこだけ詳しく書きますが、結合則使って演算順序を変えるところは各自 rewrite とかで頑張っ...
22 April, 2014

[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...
27 April, 2012

[Coq] Group on Setoid

›
@cocoatomo さんの blog に Python で群論 をという記事があったので、同じことを Coq でやってみました。 証明を含む実際のコードは  https://github.com/tmiya/coq/blob/master/group/setoid_grou...
31 March, 2012

[Coq] Specification of rev

›
そもそもの動機は（普通に再帰で書かれた） rev 関数の正しさを保証する最小の Unit Test ケースは何だろうみたいな話で、リストを逆転する rev 関数についての性質を話していて。 A:Type とし、 f : list A -> list A な関数とする...
27 March, 2012

[Coq] Epistemic Logic

›
先日のFormal Methods Forum勉強会で話した話。 Epistemic Logicというのは「誰々は◯◯を知っている」「誰々は◯◯を知っていることは常識である」みたいな知識に関する事柄を扱う論理です。通常の命題 $P$ に対して、「$\alpha$は$P$を知っ...
25 March, 2012

[Coq][Alloy] Proof of Alloy Example

›
本日の Formal Methods Forum で扱った Alloy の問題で、 assert union { all s:set univ, p,q : univ -> univ | s.(p + q) = s.p + s.q } check union...
25 February, 2012

[Coq] Even + Odd = Odd

›
日本数学会の 「大学生数学基本調査」に基づく数学教育への提言 によると、『「偶数と奇数の和が奇数になる」証明を明快に記述できる学生は稀』という調査結果が得られたそうです。 さて Coq で実際証明してみると判りますが、ちょっとした工夫をしないと、 Theorem plus_...
13 February, 2012

[Coq][Alloy] Properties of Relation

›
先日のFormal Methods Forum勉強会にて、Alloy本の演習問題を皆で解いた。Alloyとしての課題は、関係 r について各種性質（推移律とか単射とか）を Alloy の関係演算記法で書かれたものについて検討した後に、述語論理っぽく同等の性質を書き下し、同等性を ...
01 February, 2012

[Coq] Scala PartialFunction is Monoid

›
「Scala の PartialFunction が orElse の演算に関して monoid になっているのでは？」という stackoverflow の議論 Scala PartialFunction can be Monoid? について twitter 上で目にしたの...
19 January, 2012

[Coq] Coq Tutorial on 1/12, 2/2, 2/9, and 2/16

›
イベントレポート：「Coqチュートリアル#1」 @ InfoQ 今回、豆蔵様より会場を提供していただけることになって、前々から計画していた平日夜の複数回開催のCoqチュートリアルを 1/12, 2/2, 2/9, 2/16 という予定で開催します。 参加申し込みについては上...
05 January, 2012

[Coq] itoa in Coq

›
https://github.com/tmiya/coq/blob/master/Radix/Radix.v 自然数$n$を$p \ge 2$で割って余りを求め、商をまた割って、と繰り返すことで$n$の$p$進表示を得られますが、そのencode/decodeをCoqで書きま...
31 December, 2011

[Misc] 2011 Summary

›
2011年を振り返ってですが、 今年も Formal Methods Forum が続けられた。@kencoba さん他皆様のお陰だと思います。来年も継続して行きたい。 RegExpライブラリ が書けたのは嬉しかった。2012年も上半期に何か纏まった成果を出したいなぁ。 ...
30 December, 2011

[Coq] Group defined by one operation

›
通常、群$G$を定義するときは、演算 $\cdot : (G \times G) \rightarrow G$, と単位元 $e:G$, 逆元 $(\cdot)^{-1}:G \rightarrow G$ から定義しますが、$x/y := xy^{-1}$ を基本的な定義として群...