日々の流転

λ. 『下流志向 ― 学ばない子どもたち 働かない若者たち』 by 内田 樹

読了。

最初に出てくる「若い人たちにとっては、世界そのものが意味の穴だらけ」になっていて、「『意味のわからないもの』が彼ら世界で意味を失ってしまった」というのは表現が面白いなと思った。

「教育からの逃避」に関して、家庭内労働が消滅してしまったため、現代の子供達は社会関係に入っていくときに、労働からではなく消費から入ることになり、消費主体として教育サービスを値踏みし、経済合理性故に教育から逃避している、という指摘は興味深かった。 また、「労働からの逃避」についても同じく経済合理性から説明していて、なるほどと思った。

ただ、これらは仮説・解釈としては面白いけど、「本当かな?」というのが、正直なところ。 と思うのは、(著者は社会学者でないせいか)そもそも検証に興味を持っていないように思えるのと、どうも経済・ビジネス・リスクといったものについてあまりに素朴な見方が元になっていて、その辺りが疑わしく思えてしまうため。

λ. PLDIr #6

PLDIの論文を読む PLDIr の第六回に参加。 今回はPLDI2002の論文が対象で、私は以下の2本の論文を紹介した。

• Adoption and focus: practical linear types for imperative programming (著者版)
• MaJIC: compiling MATLAB for speed and responsiveness (著者版)

Adoption and focus: practical linear types for imperative programming は、型で状態をトラッキングする Type state のようなシステムに関するもの。 状態をトラッキングする型システムはエイリアシングと相性が悪い。 例えば、close(a); read(b) は a と b が同じものを指していたら不正となる。 そのため、エイリアシングを禁止して線形型的な取り扱いをするのだけど、線形型をフィールドに持つような型も線形型にしなくてはいけなくて、現実的ではなくなってしまう。 この問題を解決するために、adoption と focus という演算を持つ型システムを考えている。この型システムは面白かった。

MaJIC: Compiling MATLAB for Speed and Responsivenes は、MATLABのためのJITコンパイラとAOTコンパイラのシステム。MATLABは型なしの言語なので、型推論するのだけど、JITの場合と違ってAOTの場合には型を投機的に予想してコンパイルするというのが面白かった。

スライド(PDF):

前回

λ. Formal Methods Forum

昨日の PLDIrで紹介されたので登録してみた。

tmiyaさんのCoqとWhyについての発表資料「Coq and Why : Formal Verification Tools」が面白い。

• Coq_20100208a.pdf
• <URL:http://www.slideshare.net/tmiya/coq-20100208a>

Whyは 計算機言語で定理証明 (Proof Party.JP) のときにちょっと使ってみた Jahob と同じようなツール。

λ. Javascript クイズ

Javascript というか ECMA262-3 に関するクイズ。

var f = function(){ if (true) {function g() { return 1; }; }
               else {function g() { return 2;};}
               var g = function() { return 3;}
               return g();
               function g(){ return 4;}}
var result = f();

このコードの実行後に result の値はどうなるべきか?

これを知って、Javascript難しいと思った。

元ネタ: A Structural Operational Semantics for JavaScript の18ページ目