日々の流転

λ. スパイ・ゲーム

スパイ・ゲームを見て来た。

• http://www.spygame.net
• http://spygame.eigafan.com

λ. 今年を振り返って

抱負は結局実現できてませんでした。「他人を犠牲にする」どころか他人に見捨てられてばかり。自分の欲求を追求すると言うよりも、自分を保護してくれる環境や人物に依存することによって一年を過ごしてしまってきた気がする。だんだんと自分の中で何か熱意のようなものが薄れてきている気もするし、この傾向はいい加減に解消しないとまずいよなぁ。

λ. 今年を振り返って (圏論)

ところで、1年前は圏論(Category Theory)の勉強会をやろうとしてましたが、結局参加者は集まらず一人で寂しく勉強してました。Categories for the Working Mathematician は、無責任に他人に勧めて置きながらまだ殆んど読めていないし、結局今年理解できたのは残念ながら圏論の初歩に過ぎなかったです。ただ、それにしても、圏論は「言語」として非常に優れていて、圏論を通して数学や計算機科学の色々な面を知ることが出来た事は、大きな収穫であったように思います。今年中にCPL(Categorical Programming Language)を再実装して、圏論の学習の一つの区切りにしようかと思っていましたが、これも残念ながら間に合いませんでした。

λ. 読書

『まぶらほ — メイドの巻』

築地 俊彦 [著]

「鋼鉄侍女(パンツァー・メートヒェン)」(Panzer Mädchen) なんて、すごいもの考えるよなぁ。しかし、なんにしてもメイドは良いものです。うんうん。……とか書いてみよう。

λ. Ruby-CPL (仮称)

R-NAT-Vの理解がいまいち進んでいないので、expressionのパーサも書いて、一応対話的に使えるようにした。

λ. 零戦ニ欠陥アリ

旧日本軍弱小列伝で紹介されていたので、ETV特集「零戦ニ欠陥アリ」の再放送をみた。

λ. コミケ

何やら不思議なパーティでコミケへ。

• 入手したもの
  • 「くろいブラウスのあのこ」 (平均律)
  • 「東方文鳥録　〜Return Reanimateness〜」 (文鳥オンライン)
  • 「珍しい物を食べる会　珍味ミシュラン(山手線西側編)」「珍しい物を食べる会　珍味ミシュラン(山手線東側編)」 (mixi:「珍しい物を食べる会」)
  • 「青少年言説 WORKS - 後藤和智の仕事 2006〜2007」
  • 「暗黒団　計算機まとめノート　Linux上でのアセンブラ」「複素代数幾何初級検定・問題3とその解答」「最短距離のC言語」 (暗黒通信団)
  • 「Spファイル vol.5」 (Spファイル友の会)
  • 「THROW LINE」 (PASTA'S ESTAB)
• 入手できなかったもの
  • 全方位スクロール物量系アブストラクト系シューティング「exception」 (i-saintさん)
  • 「風 - KAZE -」 (SOUND HOILC)
  • 「コープスパーティブラッドカバー1」
  • 「うみねこのなく頃に episode 2」 (07th expansion)
  • 幺樂団の歴史4「東方夢時空　〜 Pantasmagria of Dim.Dream」, 幺樂団の歴史5「東方靈異伝　〜 Highly Responsive to Prayers」 (上海アリス幻樂団)
  • …

λ. 忘年会

λ. 「クリーニ代数入門」 by 古澤 仁 and 高井 利憲

• <URL:http://www.jstage.jst.go.jp/article/jssst/23/3/23_3_14/_article/-char/ja/>

二年前からの積読消化。 ちょっと前 に Topology via Logic の12章 Spectra of rings を読み返して、そこでquantaleに関係して「Conway [71] defines the notion of “standard Kleene algebra”, which is essentially the same as a quantale」と書かれていて、そういえばと思って読み始めたもの。 クリーニ代数に関しては「正規表現を公理化した代数らしい」というくらいの知識しか無かったんだけど、これは応用も沢山あり面白い。

ちょっとビックリしたのは、min-plus代数とトロピカル代数が同じもので、これがクリーニ代数の一例であること。 min-plus代数についてはPPL2008での発表 Modal μ-calculus on min-plus algebra N∞ で聞いていたし、トロピカル代数については檜山さんが時々日記に書いていた*1のを読んでいた。 どちらもちゃんと理解出来てはいない話だったのだけど、繋がってたのね……

min-plus代数を使って最短経路問題を解く話は面白かったので、自分でも試しに書いてみた。KleeneAlgebras.hs

また、自由代数に関しては、代数のクラスCが等式またはホーン節で定義される場合には集合からの自由生成が可能という話は、等式以外から自由生成することなんて考えたことが無かったので、「へぇ」と思った。

あと、KAT-MLという対話的定理証明器があるそうなので、遊んでみたい。

λ. コミケ

久しぶりにコミケに参加。購入物は以下のとおり。

• 『逆引きAcme大全 夢幻編』 by どんぞこ楽屋
• 『あふりかん大王』 by eoh (projectちゅちぇ) (twitter ID: @HEAT_PM, pixiv ID : magneton)
• 『SHANGRI-LA character filegraphy』 by 村田蓮爾＠PASTA'S ESTAB
• 『東方神籬』 by 紙切ればさみ
• 『K-theory入門』 by K-functor＠暗黒通信団
• 『Post card Book』 by 石渡尚子＠isismo
• 『最速クリア研究＠ドラゴンクエストI』 by 魔神ゲノム
• 『真・松来未祐　歌リスト本』 by 丹後研究員＠暗黒通信団

λ. 2013年振り返り

2014年を迎えるにあたって、2013年を簡単に振り返ってみる。

月毎の主なイベント

1月

Coursera での学習を開始。昨年末に買ったNexus7で初めてのAndroid経験＆初代iPadから乗り換え。

2月

スキーで転けて靭帯損傷。

3月

『型システム入門 プログラミング言語と型の理論』出版と出版記念トークイベント。Max-SAT Evaluation 2013 に参加。

4月

特になし

5月

Haskellで計算機代数勉強会を開催。Google Code Jam 2013 は去年に引き続いて今年も体調的に微妙で微妙。

6月

某自社の株主総会見てきた。

7月

スカイツリー昇った。ICSE'13勉強会でT芝チームとして発表。 奥歯抜歯。Coursera MeetUp Tokyo に参加。

8月

ICFP Contest 2013 に例によって Team Sampou で参加。引越しと一人暮らし開始。SPLC2013の併設ワークショップFMSPLE 2013で発表。

9月

ウサギと同居開始。

10月

結婚(といっても婚姻届を出しただけで、結婚式はまだ)

11月

電機連合第34回技術者フォーラムに参加。2013川崎国際多摩川マラソンに参加。

12月

川崎グランシティモール実証実験開始

Coursera

前から少し気になっていたCourseraを1月に試してみて、最終的に以下の9コースを履修。

1. Computing for Data Analysis by Roger D. Peng @ Johns Hopkins University
2. Data Analysis by Jeff Leek @ Johns Hopkins University
3. Linear and Discrete Optimization by Friedrich Eisenbrand @ École Polytechnique Fédérale de Lausanne
4. Machine Learning by Andrew Ng @ Stanford University
5. Developing Innovative Ideas for New Companies: The First Step in Entrepreneurship by James V. Green @ University of Maryland, College Park
6. Model Thinking by Scott E. Page @ University of Michigan
7. Maps and the Geospatial Revolution by Anthony C. Robinson @ The Pennsylvania State University
8. Introduction to Computational Finance and Financial Econometrics by Eric Zivot @ University of Washington
9. Introduction to Recommender Systems by Joseph A Konstan and Michael D Ekstrand @ University of Minnesota

自分のスキルのポートフォリオに追加したいと考えたものを中心に、それなりに戦略的に学習してみたつもり。上手くいった部分もあればそうでない部分もあるけれど。自分はデータ分析や統計に関しては大学1年のときに、ほぼ必修の位置づけだった「データ分析」の授業を途中で飽きて切ってしまってから、ほとんど学習しないままになってしまっていたので、その辺りを補完できたのは良かった。

そして、7月にCoursera MeetUp Tokyoに参加したところ、その縁で、メディアで取り上げらることになったのは、なかなか貴重な体験だった。

• 朝日新聞8月22日朝刊教育欄「東大、ネット講義で世界へ発信　秋から無料講座に参入」
• クローズアップ現代「あなたもハーバード大へ ～広がる無料オンライン講座～」(2013年9月17日（火）放送)
• 金成隆一: 広がるMOOC（ムーク）の活用と試行錯誤, 大学教育と情報, 2013年度 No.2 (通巻143号), pp. 2-11.
• 『ルポ MOOC革命――無料オンライン授業の衝撃』(金成 隆一)

新しいプログラミング言語、環境

「毎年少なくとも一つの言語を学習する」という話があるけれど、今年は Coursera のコースで割と色々な言語を学べた。 Computing for Data Analysis、Data Analysis、Introduction to Recommender Systems では R を、Linear and Discrete Optimization ではPython (とSymPy)を、Machine Learningでは MATLAB/Octave に触れることができた。その後、そのうちのRとPythonは仕事でもそれなりに使うようになったので、結構役立っている。

それから、言語というほどではないけれど、Model Thinking では NetLogo に、Maps and the Geospatial Revolution では ArcGIS Online に触った。 あと、Introduction to Recommender Systems で使った LensKit は、アノテーションなどを活用したJavaの今風なDIを使ってて、ちょっとおぉと思ったりなんかもした。

『型システム入門 プログラミング言語と型の理論』出版

Benjamin C. Pierce の Types and Programming Languages (TAPL) の訳書『型システム入門 プログラミング言語と型の理論』を出版。前回のAlloy本こと『抽象によるソフトウェア設計−Alloyではじめる形式手法』が終わり、2011年9月からTAPL翻訳が本格始動したのだけれど、それから1年半ほどかかって、ついに出版にこぎ着いたのがこの3月で、非常に感慨深かった。また、共訳者、監訳者、編集者、レビュワー、皆素晴らしい人達ばかりで一緒に仕事をできて光栄だった。出版記念トークイベントという珍しい体験もしてしまったし。

• TAPLの日本語訳出版します (ヒビルテ 2013-03-15)

靭帯損傷

2月にスキーで転けて靭帯損傷。内側側副靭帯損傷の2度で、MRIを初体験したり、しばらくギプス(正確にはギプスシーネ)と松葉杖で不便な生活をしたり、さらに結構な間リハビリをしたりとか。 ギブスしてると、立ってても座っててもバランスが悪くて、体中凝って仕方なかったのが辛かった。 後、しばらくギプスとサポーターをしてるだけで、関節って本当に曲がらなくなるんだなぁ。リハビリしてだんだん動くようになって、人間の関節や筋肉って本当によくできてるなぁと思った。 大変な体験だったけれど、周囲からは非常によくしてくれたし、結構学ぶことのあった体験だったと思う。

ランニング

ランニングは500kmの目標を立てていたけど、途中怪我で数ヶ月走れなかったこともあって、320kmほどに留まった。でも、我ながらよく続いたなぁと思うし、自分を誉めてあげたい。 また、大会に参加するという目標は2013川崎国際多摩川マラソンに参加するという形で達成。 目標がハーフマラソンだったのに対して8kmになってしまったので、ハーフマラソンを走るのは2014年の目標に持ち越し。

あと、昨年末にちゃんとしたランニングシューズを買ったけれど、今年は心拍計 Wahoo Blue HR とか、活動量計 Misfit Shine とか、ランニング用のスポーツタイツのCW-Xとか色々と買ってしまった。

お仕事

Courseraで学んだデータ分析・機械学習系の知識を活かして、これまでとちょっと違った方面の仕事に挑戦してみた1年で、川崎グランシティモール実証実験 なんかにも関われて、まだまだこれからだけれど、面白い仕事ができた。

• <URL:https://plus.google.com/+MasahiroSakai/posts/hdEteHHBGxr>
• <URL:https://plus.google.com/+MasahiroSakai/posts/V9atG4FFHTX>

その他にはFMSPLEで発表したりとか。

• Masahiro Sakai, Takeo Imai, Mikito Iwamasa, Takeshi Nagaoka and Mari Inoki, A Decision Table Analyzer for Detecting Variability in Source Code, Fourth Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE 2013), August 27, 2013. (presentation only)

計算機代数

代数的実数や量化子除去に関して勉強したり簡単な実装をしたりしていたので、思いきって Haskellで計算機代数勉強会という勉強会をゴールデンウィークに開催。結構マニアックなトピックにも関わらず参加者20人以上も集まり、なかなか楽しかった。 その後も、Berlekamp-Zassenhaus アルゴリズムを理解して実装したりとちょっとは進めた。あと、これまでなんとなくしか理解できていなかった sugar flavor とか syzygy とかについて、計算機代数勉強会での@mr_konnさんの発表で理解できて、自分でも実装してみようと思っていたけれど、これは実装しないままになってしまったなぁ……

Max-SAT Evaluation 2013

昨年は Pseudo Boolean Competition 2012 に参加したが、今年は開催されなかったので、代わりに Max-SAT Evaluation 2013 に参加。 今回は自分のtoysatに加えて、GLPK と SCIP に簡単なフロントエンドを付けたもので参加。

自作のtoysatの方は、昨年の Pseudo-Boolean Competition 2012 ではそれなりに健闘した(と思ってる)けれど、今回はあまり振るわなかったねぇ。 まあ、色々とやりたいことはあったけれど、結局、目的関数値の線形探索ベースの単純なアルゴリズムのやつで投稿してしまったからなぁ……

SCIPの方は、SCIP本体のバグが見つかって、SCIP開発者に報告・修正してもらったものを再投稿させてもらったりと、意外と大変だったけれど、その甲斐もあって Partial Max-SAT 部門の Crafted ベンチマークで2位に入賞して嬉しかった。(別にフロントエンドを書いただけの自分がすごい訳ではないのだけれど)

• <URL:https://plus.google.com/100215187201873478127/posts/M1AHKWtyaRz>

英語

英語は今年はあんまり頑張れなかった。 Courseraでは英語を使って学習してはいたし、日本開催の国際会議SPLC2013の併設ワークショップFMSPLE 2013で発表はしたものの、海外には一回も行かなかったし。それに、レアジョブも後半は殆どやらなくなってしまったしなぁ。2014年はその辺りもっと頑張りたいところ。

関連エントリ

• 2011年振り返り

λ. 2015年振り返り

2015年を振り返ると、色々と翻弄された年だったな、というのが正直なところ。 だけれども、こうして振り返ってみると、それでも割と色々とやっていて、捨てたものでもないかもという気にもなってくる。

お仕事

お仕事的には、某プロジェクトの打ち切りから始まり、その後色々なプロジェクトに参加したりしたけれど、色々となかなか思うように進められず、また色々と思い悩むことも多かった１年だった。 発表としてはコンピュータソフトウェア誌への「SAT問題と他の制約問題との相互発展」の掲載(G+の投稿)と、FIT 2015 (第14回情報科学技術フォーラム) での「地域活性化のためのスマートフォンアプリを用いた実店舗および商品の推薦 」という簡単な発表。 その他には例年通り ICSE 2015 勉強会 で論文紹介をしたりとか。 あと、海外の顧客に対して技術のプレゼンテーションしたりとか、ちょっと面白い経験もできた。

英語とか海外とか

今年は Rarejob も iKnow もほとんど出来ず。 せっかくおカネを払ってるのだからもっとやらないと勿体ないのだけれど…… ただ、久しぶりに受けたTOEIC(IP)では905点をとれ、前回2008年の885点からは上がってたので、多少なりとも進んでいるのが実感できたのは良かった。

それから、フランスに行ってメドックへのワインを飲んできたり、サルラを観光したりと、遊んできた。 鉄道のストとか、おみやげのフォアグラを空港で急遽消費したりと色々あったが、いい経験と思い出になった。 海外にはずっと苦手意識があったけれど、ようやく慣れてきたかも。

Coursera / MOOC

今年も前半幾つかコースを取れたけれど、後半はそれどころではなかった感じ。

最初に受けたのは Gamificationのコース。 あまり受けたことのないタイプのものだったので、面白かったが、得られた知識はまだあまり活用できてはおらず。

それから、昨年、受講したけど途中で断念した　Discrete Optimization を再受講して、最後はギリギリだったけれど、なんとか修了証をゲットするまでできた。 列生成法(Column Generation)とか分枝価格法(Branch and Price)とか気になっていたのが理解できたのは良かった。 以前に受講した Linear and Discrete Optimization と合わせて、これで私も一応は最適化の専門家を名乗っても良いだろうか(^^ まあ、実際には非線形の連続凸最適化とか、カバーできていない領域はまだ色々とあるけれど。

その続きとして、Modeling Discrete Optimization も受講したかったけれど、忙しくなってしまってこっちは結局断念してしまった。

もう一つは、Process Mining: Data science in Action の受講で、こっちはペトリネットやワークフローといった比較的馴染み深い話と、データ分析、エンドトゥエンドでのプロセス改善みたいな話がつながってきて、なかなか面白い領域だった。

あと、Coursera’s Global Translator Community (GTC) は参加はしてみたけれど、結局ちょっと翻訳してみただけで、その後の活動が続かなかった。

プログラミングコンテスト系

今年も Google Code Jam はラウンド1を突破できず残念。 また、 ICFP Programming Contest 2015 の方 は結局上位位にはいけなかったけど、色々新しいことを試せたのは良かった。 せっかく最近機械学習とか勉強しているのにDQNを試せなかったのは心残りではあるけれど。

それから、今年も toysolver / toysat を Max-SAT Evalution や Pseudo Boolean Evaluation には出したけれど、アルゴリズム的な改良も特には出来ていたわけでもなく、これも結果は振るわず。一方で、新しいチャレンジとして、MINLPLIB2を変換したものでしかないけれど、問題を投稿するということができたのは良かったと思う。

あと、Proof Summit 2015 で「SAT/SMTソルバの仕組み」というトークをして、それをキッカケに放置気味だった*1実装を再開して、簡単なSMTソルバの実装ができたのは進捗っぽい。 まだ、SMT-LIB2の仕様を満たせていないのでリリースしていないけれど、満たせたらリリースしたい*2。そして、来年はSMTソルバのコンペであるSMT-COMPに参加してみたいねぇ。 もっとも現段階では本当に最小限の動作をするだけで、性能を云々するところまでいけていないし、これから頑張っても、第一線のソルバと性能を競うところまでは行けそうにないけれど。

それから、以前から気になっていたセキュリティの技術を競うCTF(Capture the Flags)に参加してみれたのは良かった。 CTF for ビギナーズ 2015 東京 に参加して 103人中6位になった後も、Trend Micro CTF Asia Pacific & Japan 2015 Online Qualifier と SECCON 2015 Online CTF にチームで参加し、それぞれ881チーム中46位と、1251位中43位という成績に。 セキュリティ方面の問題には専門家が多かったので、餅は餅屋ということでお任せして、自分は割とプログラミング系の問題を解いていただけだけれど、後からセキュリティ系の問題も復習したりして結構勉強になった。

• <URL:https://plus.google.com/+MasahiroSakai/posts/SAmMNXMBZgy>
• <URL:https://plus.google.com/+MasahiroSakai/posts/GXikC8acbh5>
• <URL:https://plus.google.com/+MasahiroSakai/posts/9JaHiNJUBSJ>
• <URL:https://plus.google.com/+MasahiroSakai/posts/Ag82UPytnMc>
• <URL:https://plus.google.com/+MasahiroSakai/posts/bfPxxooKwh2>

コミュニティとか技術トレンドとか

ここ数年引きこもり気味で技術的なトレンドとかをあまり追えていなかったけれど、Proof Summit 2015、Haskellもくもく会、Tokyo Haskell Meetup に参加して他の人と交流したりと、少しはリハビリできたかな。

新しい言語としては、Goを触ってみたけれど、結局ちょっと試しただけで、それ以上使っていけなかったのは残念な感じ。

余談としては、「flatten=平滑化」事件 とか。

ランニング

3/8の「かつしかふれあいRUNフェスタ」でハーフマラソンの2回目を走った。 その後、今度は今年中にはフルマラソンを一回と思っていたけれど、以前に靭帯を痛めた方の膝の調子が一時期イマイチだったこともあって、結局割とマイペースに走っていた。 年末の恒例の皇居ランではちゃんと2周10km走れて良かった。 合計回数と距離は、Nike+によると今年は104回のランで338.89kmほど走っていたようだ。来年こそはフルマラソンに挑戦したいねぇ。

Ingress

Ingressは 啓示の夜のパワーキューブを観に第18回文化庁メディア芸術祭の受賞作品展示に行ったり、#‎IngressYokosuka‬ のミッションデイ に参加 した以外は、特にイベントにも参加せず、まったりやっていた感じ。 一応レベル15にはなった。