2009年3月21日土曜日

技術者/プログラマのためのラムダ計算、論理、圏 第3回に行ってきた

実は第2回にも行っていたんだけど内容をまったく咀嚼できず、そのうちやろうと思っているうちに第3回が開催されてしまった ^^;

第2回 ラムダ計算と停止性問題
第2回は、主にラムダ計算について。前回の復習からはじまって、回路図のような絵を交えながらラムダ抽象化につなげていき、最後はJavaScriptのようなCのような疑似コードを使って、チューリングマシンの停止性問題を背理法で証明して終わった(と思う)。詳しくは、檜山さんのBlogに書いてあるので、そちらを見た方が良いと思う。

セミナー資料
紙芝居:ラムダ抽象
セミナー非参加者にもわかるリアルワールド向けラムダ計算
なぜ停止性について話したのか?

第3回 自然演繹と型付きラムダ計算、カリー/ハワード対応
第3回は、カリー・ハワード対応についての感覚的な理解がゴール。第2回とはうってかわって論理を中心に話をすすめていき、論理でやっていることが最終的にラムダ計算に対応することを感覚的に理解することで、カリー・ハワード対応を感じるのが目的、という感じ。こちらも、檜山さんのところに、他の参加者さんのまとめへのリンクを含めてきちんと色々書いてあるのでまとめは書きません、というか書けません!

セミナ資料
カリー/ハワード(Curry-Howard)の対応を知らない子供達および大人達へ
演繹系の話題と演習

もともと、「素数の音楽」「暗号解読」「論理学入門」あたりの書籍や、TM(T字形ER)のセミナでの疑問(数理論理学まわり)解消のためにちょこちょこ調べていたこともあって、今回の話の大半は馴染みがあった。とはいえ、雰囲気つかむことを重視してたので、導入規則や除去規則についてあまりよくわかっていなかったのだが、今回具体例をもとに理解できたのはとても良かった。
セミナの内容の本筋としては「計算と論理は以下のように対応する」

論理算術
演繹系 算術回路キット
推論 基本演算
証明図 計算図
演繹系の証明図 算術回路キットの計算図
証明可能 計算可能
derived rule 計算のマクロ
公理 最初から使える定数
定理 計算済み定数

でFAな感じなんですが、話の中でちらちら出てくる用語や、自分が既に知っていることとの関係がよくわからなくてもやもやしている。というか、聞けば聞くほど疑問が増えるという状態...
  • 檜山さん的アプローチでのラムダとは少しは仲良くなった気がするが、一般的(形式的というか記号的というか)なラムダ計算についてイマイチわかっていない感
  • カリー/ハワード対応が何を意味しているのか(この理解が何につながっていくのか)
  • 自然演繹以外の演繹系と、型付ラムダ計算以外の計算も対応するのか?
  • フォーマルメソッドや自動証明との関係は?
  • プロセス論理との関係は?
  • 型推論との関係は?
  • 結局、絵算というのは何がエキサイティングなんでしょう?
檜山さんのエントリによると、話題同士の関係についてこれからいくつかエントリをあげつつ説明してくださるようなので、それらのエントリをながめつつ、自分なりに理解を深める過程を書いていこうと思う。ううむ...文系は土台からしてしょぼいからつらいなぁ...。

何か関係ありそうなリンク
型=命題、プログラム=証明
 Haskellを例に、型推論との関係について説明してくれそう。
Curry-Howard対応を知らないこども達
 サーセン(笑)
Curry-Howard Isomorphism
 ざっと読んだけど、概要を把握するにはとても良さそう。
CiteSeer : Curry-Howard Isomorphism
 カリー/ハワード同型対応についてきちんと書いてあるらしい論文。
自然演繹-Wikipedia
 型理論や線形論理との関係も書いてある。
ラムダ計算-Wikipedia
 ここに書いてあることが「そりゃそうだよねぇ」と言えるくらいにはなりたい。

2009年3月18日水曜日

自分のブランディングを考える inspired by 「抜擢される人の人脈力」

同僚に貸してもらって「抜擢される人の人脈力」という本を読んだ。これは、人脈をつちかっていくことで自分自身も成長し、トータルでの仕事の能力も上げ、最終的には代替不可能な人材になって自由な働き方を手に入れよう、てな本。目指すところには非常に共感した。

人脈を広げるための5ステップ
この本では、人脈を広げるためのステップを、以下の5段階で定義している。
  1. 自分にタグをつける
  2. コンテンツを作る
  3. 仲間を広げる
  4. 自分情報を流通させる
  5. チャンスを積極的に取りにいく
2番目以降は考えるだけではダメなのでおいおいやっていくとして、まずは自分にタグをつけるとしたらどうなるのかを現時点で整理して、ブログの紹介文にでもいれとこうかと思う。

自分へのタグづけ
さて、タグをつけるには、以下の3つの観点から考えると良い、とアドバイスされている。
  1. 将来、どんな仕事をしたいか(Will)
  2. 自分にできることは、何か(Skill)
  3. 相手にどんなメリットをもたらすか(Value)
はい、では1から。

Will/将来、どんな仕事をしたいか
第二の就職活動のような内省が必要になる部分だろうと思うが、自分は日常の会話やふとした反応から、自分にいくつかの指向があるのを感じていた。まず、最も根底にあるのは...
すばらしい仲間と最高のシステムを作る
ということ。ここでの「すばらしい」が意味するのは、必ずしもすばらしいスキルを既にもっている、ということではない。それは、志を同じくしていて、そのシステムをより良いものにするのに真剣に心を砕き、全力を注いでくれる、という意味だ。そして、そんなシステムを作るために、日頃から鍛錬を惜しまない、という意味でもある。だから、結果として高い能力はついてきているはずだ、という期待もある。もちろん、自分がその仲間になるのであれば、自分も同じようにあらねばならないのは当然のことだ。...できてるかどうかあやしいけど...。

簡潔にタグにするとすると、どうなるんだろう?「目指せドリームチーム入り」?チームメディカルドラゴンみたいな感じでしょうか。

さらにもう1つ、それは...
アカデミックな研究成果で現場を進歩させる
ということ。自分はもともと経済学部でミクロ経済学を専門にしていたんだけど、色んな仮説をたてて市場をモデル化し、現実の経済を分析しようとしても、そのモデルがどの程度現実を反映しているのかを知ることは非常に困難であり、現実世界に寄与する方法があまり具体的にイメージできなかった。この現実世界との乖離度合いに我慢ならなかったために、企業に入社したようなものだ。

元々自分はアカデミックな研究成果(というより、先人が払ってきた膨大な労力)に対して敬意を持っているのだが、往々にして現場はアカデミックな研究成果を現実的でないと馬鹿にしていたり、そもそも理解するどころか、どのような成果があるのかを確認すらしていないことが多い。
彼ら(我ら)が我流で考えだす改善策やソリューションにも一定の意味があることは多いが、たいていは研究成果の出来の悪い焼き直しであったり、よくわからない局所最適解であることが多い。今は昔とは逆に、アカデミックな研究成果を現場に取り入れることの難しさにもがいているわけだが、大学から現場に口を出すよりも、現場から成果をひっぱってくる方が遥かに簡単だと感じている。自分は研究と現場をうまくつなぐような役割を果たしたい。
こういうの、なんていうんだろう?「現場の学者」のようになりたいのだ。

最後にもう1つ、それは...
才能を持った人材が比較的自由に仲間や仕事を選べる、職人ギルドのような組織を作り、個人の力を最大限に解放できるようにする
なんか長いな。これはもう、そのまま。特に動機になっているのは、企業内では才能を持った開発者が自己の能力を最大限生かして働くことが非常に難しい、ということ。さらに、生かせたとしても、それに対してあまり高い報酬をもらっていないケースをよく見る。逆に、大した寄与がない人間が非常に高額の報酬をもらっているのもよく見る。自由もなく報酬も少なく、評価もあまりされない。仮に自分を成長させられたとしても、居場所がなさそうな世界なんてぶっつぶしてやりたくもなるよね?これを実現するには、周囲が才能や能力を認知できる状態にしなくてはならないので、みんな一定の能力が求められることになるんだけど。
タグづけすると...「才能を縛らない現場を作る」かな。

Willはこんなものかな。次、2。

Skill/自分にできることは何か
自分にできること...
「小規模から超大規模まで、10近くの様々な規模の業務システムでソフトウェアアーキテクチャ設計に携わっている。そのうちの2つの中規模システムは主たる設計者として参加している。」
「業務アプリケーションから基盤ソフトウェア、開発支援ツール類までの設計・実装をしている。」
「業務システム開発の技術リスク監査ができる。」
「業務モデリングもある程度できる。」
「Domain-Driven Designをわりとよく理解している。」
かなぁ。

Value/相手にどんなメリットをもたらすか
ううむ、難しくなってくるな...
「どんな規模のシステムでも、ソフトウェアアーキテクチャ設計できますよ」
「インフラだけでなく業務もある程度わかるので、ソフトウェア全体の最適化の役に立てますよ」
「業務モデリングによる業務最適化も考慮したシステム開発ができますよ」
「DDDアプローチによる、柔軟性の高いシステム構築に対応できますよ」
こんな感じだろうか。

最後に、コンテンツを考えるうえでのヒントをメモって終わりにする。
  • 能力
  • 実績
  • 意欲
以上の3つを把握する。実績を積むためには...
  • 脳に汗をかくくらい頭を使う
  • ビジネス上の修羅場を経験する
  • 自分の名前で仕事をする
以上を心がける。さって、がんばるぞー。とりあえず明日、檜山さんの主催する、「技術者/プログラマのためのラムダ計算、論理、圏」最終回にいってきまっす!