2007-02-05 [長年日記]
λ. 大人の常識力トレーニングDS
これまで少しばかり非常識な存在だったので、常識を身につけようと購入してみた。社会人にもなることだし。
最初の診断の結果は7問正解*1で常識力指数59。なんだ、わりと常識的じゃん、俺。でも、苦手ジャンルは「礼儀」で、これは予想通り。
λ. [tom] 研究会最終発表
せっかくDSを持っていったのに、ピクトチャットするのを忘れてた。 しょぼーん。
打ち上げ
- コスプレはするもんじゃない、させるものだ
- 藪をつついたら萩野先生が
- 大学教授は社会人なのか?
*1 一問暗算が間に合わなくて落した問題があるのが悔しい
2007-02-03 [長年日記]
λ. Functional Logic Languages: Basic Concepts and Operational Semantics by Michael Hanus
を読んだ。<URL:http://d.hatena.ne.jp/m-a-o/20070128#p4>より。
関数論理型言語の実行モデルってこんなに興味深い話だったのね。
2007-02-02 [長年日記]
λ. 秋学期修士最終試験
中高の入試と被っていたので朝バスは凄い状態になっているのではないかと思ったが、8:40〜9:00ごろには空いていた。受験生はもっと早い時間だったのかな。
発表ではPowerpointの発表者ツールが使えずに焦ったが、発表時間の調整は発表練習の時よりもうまく行っていた。不思議だ。そして、質疑応答もそれなりにうまくこなせた。人事は尽くしたし、あとは天命を待つだけ。
発表を終え、会場を後にする修士たちの姿(まだ未発表の人もM2じゃない人もいるけど)。赤松さんによる写真。
λ. [haskell] Haskellと高階論理の土台は異なるか?
宮本の日記（仮）のGHCは気色悪いという話に関して。コメントとして書こうと思ったのだけど、色々と書き足しそうなので、こっちに書く。
∀x. (a → b → x) → x が a ∧ b と同型になることは通常パラメトリシティを用いて示されるが、Haskellのような言語ではパラメトリシティは完全には成り立たない。また、高階論理であってもパラメトリックでないモデルを考えれば両者は同型にはならないのではないかと思う。
次に ∀a,b. a → b という型を持つ閉項が存在するという話について。全ての型に対して不動点演算子 fix が存在する言語では、全ての型が閉項 fix(λx. x) を持ち、論理体系としては矛盾した体系になる。それゆえ、不動点演算子はパラドキシカル演算子と呼ばれることもある。
Haskellのように再帰的定義が自由に行える言語では fix f = f (fix f) によって不動点演算子を定義でき、論理体系として解釈すると矛盾した体系になっている。通常の論理では無矛盾であることが基本なのに対して、通常のプログラミング言語は論理体系としては矛盾していることが前提なため、ある意味「土台」が異なっていると言えると思う。
その点に関して、A note on inconsistencies caused by fixpoints in a cartesian closed category (20061110#p01参照) では「The results indicate the different nature of domain theory and set=topos theory or, in other words, that programming requires other foundations than even a constructive set theory.」と述べられていたりする。
また、この話については「自己言及の論理と計算」 (20030629#p03参照) は非常に面白く書けていると思う。
この辺りの話は結構面白く、幾らでも書けそうな気がするけど、とりあえずこの辺りで。
(2/5 追記) seqとパラメトリシティ
seqとパラメトリシティの話は知ってはいました(20050315#p03)が、面倒だったので触れていませんでした(それにseqが存在しなくともパラメトリックでないモデルを作ることは出来るはずだし)。そしたら早速指摘が。
- sumiiさんのseqとパラメトリシティ
- KeisukeNakanoさんのパラメトリシティとseq
今回の話の個人的な収穫は以下の点。Pittsのアプローチには詳しくないため、TT-closedness は admissibility と同じようなものだと思っていたが、KeisukeNakanoさんによれば「TT-closed は admissibility より強すぎる」とのこと。うーむ……
ψ ささだ [あれ，なにやってん？]
ψ さかい [いわゆる最終口頭試験(?)として修士論文の発表してました。 そういうのって普通ありますよね?]
ψ ささだ [ああ，なるほど．私の知っているところでは修論審査・諮問などと聞くな．気が変わって，なんか次へ進むのかと思った＞試験 ..]
ψ とくえ [おつかれ。 昨日は、あの後は残留して準備してました。発表は楽しかったです。]
ψ さかい [あれから残留したのかー。おつかれー 僕も発表は楽しかったです。 結構緊張はしたけど (^^;]
ψ 宮本 [Haskellの型についての補足をありがとうございました。さかいさんのエントリーを参考に、当方でもこの件について記事..]
ψ KeisukeNakano [はじめまして．「TT-closedはadmissibleより強い条件」ということについては，M. Abadiの「TT..]
ψ さかい [参考文献をありがとうございます。 近いうちに読んでみようと思います。]
2007-01-31 [長年日記]
λ. 今日も発表練習
15:00から始めて、終わったのは19:30過ぎ。本番では持ち時間30分(発表20分、質疑応答10分)なので、4人分で2時間ちょいくらいで終わると思っていたのになぁ。
それと、配布資料も作らんとなぁ……。
λ. [haskell] Haskellでパーサを書く時に面倒な点
先日のPTQ実装のパーサをいじって、名詞の性や動詞の変化を扱うようにしようとしていたのだけど、Haskellでこれを実現するのはちと面倒くさいという事に気付く。Prologみたいに論理変数と単一化があれば、何が入力で何が出力かを決めることなく、素性が一致するという制約だけを書けるのになぁ。もちろん、使っているパーサーコンビネータを拡張して論理変数と単一化を実現すれば良いだけの話なのだが、それも大げさすぎる気がする。大体、PTQの場合は名詞の性と動詞の変化くらいにしか使うところはないわけで。
それはそうと、文法フォーマリズムで単一化文法が主流になっている理由の一端が理解できたする。
λ. [時事] 「女性は産む機械、装置」柳沢厚労相が大失言
なんかえらい騒ぎになっているが、「産む機械、装置の数は決まっているから、あとは一人頭で頑張ってもらうしかない」というのが女性差別発言という感覚が良くわからない。そもそも、「生産要素投入が増えないのであれば、生産性を上げなきゃ生産量は増えない」というごく当たり前の事実を少子化問題に適用し、比喩を用いて説明しただけなんだよね?
例えば、我々は人間や生物も一種のオートマトン(＝機械)として抽象化して物事を考えることがある。これは人間性を無視したことなんだろうか? そんなことはない。ある面に着目して物事を抽象化・単純化することは、元のものにあった他の全ての側面を切り捨てることであり、そりゃ人間性だとかは切り捨てられる。けど、それは対象となる議論にとって本質的でないから注目しないだけであり、その他の側面が存在しないなんて誰も考えちゃいない。そんなのはあえて説明するまでも無い、当たり前の前提だ。この発言に対する過剰な反応は、私には抽象的に物事を考えること自体を否定しているように感じられて、ちょっと薄ら寒いものを感じる。
柳沢厚労相の発言は不用意だったとは思うが、辞任しなくてはならないような問題とはとても思えない。しかし、安倍内閣は阿呆らしいスキャンダルが多いね……
(2/3追記) 発言要旨
どういう文脈での発言かイマイチよくわかってなかったのだけど、YouTubeにあがっていた スーパーモーニング 2007/02/02 で1月27日の講演での発言要旨が紹介されていたので以下に引用する。
では、人口の状況はどうか。平成17年の国勢調査を受けて、18年に年金の人口推計をやるわけです。(中略) 特に、2030年に例えば30歳になる人を考えると、今、7、8歳になってなきゃいけない。生まれちゃってるんですよ、もう。あとは「産む機械」って言っちゃなんだけど、装置の数が決まっちゃったことになると、機械って言っちゃ申し訳ないんだけど、機械って言ってごめんなさいね。あとは産む役目の人が、一人頭でがんばってもらうしかない。2030年はもう勝負は決まっているとよく役人に言われる。
これを読む限りでは、単に「2030年時点で出産可能な女性の人数は既に決まってしまっていて増えようがないのだから、少子化を解決するにはあとは女性一人あたりの出産数を増やすしかない」という事実を述べているだけに思えます(「機械」は数が既に決まっていて増やせない生産要素であることの喩え)。
ψ takot [この件については，切り捨てた部分が > それは対象となる議論にとって本質的でないから 「本質的ではない」..]
ψ ささだ [まぁこうなることくらい想像できてしかるべきではなかろうか，という気はする．]
ψ さかい [それが安倍内閣クオリティ…… orz]
ψ uenoB [抽象化それ事態は自明なマッピングでまあ悪くないと思うんですが，その次のモデルの検証と問題への適用に関する考察がごっそ..]
ψ たけを [重さのレベルが違うし、片やフィクションなんですけど… 『ザ・ホワイトハウス』って米国の政治ドラマで、厚生大臣相当（..]
ψ たけを [ごめん、↑のヘロインは多分マリファナか何か、僕の間違いです。ヘロインて中毒性ありまくりだよねｗ]
ψ とおる。 [いや、少し前までは日本でも「女は子供を産んで育てる装置」という認識があったんですよ。（だから教育なんか必要ないし、政..]
ψ さかい [そういった人たちが「冗談じゃない!」と思ってしまうのは、無理からぬことだと思いますし、それを責めるつもりはないです。..]
2007-01-27 [長年日記]
2007-01-21 [長年日記]
λ. [圏論] 第二十五回圏論勉強会
今回で一応最後まで到達。まだ勉強会自体は終わらないと思うけど一つの区切りか。25回を振り返ると、一人で読んだときには自明と思って読み飛ばしてしまった問題とかも、真面目に解こうとすると結構難しかったりして、結構勉強になったなぁ。
なお、次回からは『量子ファイナンス工学入門』に対抗して、『圏論ファイナンス工学入門』を皆で執筆する予定だそうです(嘘
λ. 六耳獼猴と五仙五類
毎日新聞朝刊で連載されている西遊記を読んでいたら、六耳獼猴(ろくじびこう)というのが出てきた。五仙五類に属さない、四猴混世(しこうこんせ)の一種らしい。五仙五類というのは<URL:http://members.at.infoseek.co.jp/hongkong_movies/saiyuuki.htm>によると、五仙が天・地・神・人・鬼で、五類が人類・魚介類・獣類・鳥類・虫類ということか。分類が少し面白いと思った。
2007-01-20 [長年日記]
λ. [haskell] 関数従属性の落とし穴
以下のようなコードが型エラーになることに驚いた。
class Assoc a b | a -> b instance Assoc Int Int f :: Assoc Int b => Int -> b f x = x
fの型チェック時には個々のインスタンス宣言を参照したりしないから、考えてみれば当たり前なのだが。しかし、関数従属性(Functional Dependencies)やGADTを使うと依存型っぽいことが一部実現できるが、ちょっとでも複雑なことをしようとするとすぐに落とし穴にはまる気がする。本物の依存型が欲しい……
λ. [ruby] YARVへの感慨
そういえば、YARVに末尾再帰用の命令を追加して遊んでいた(20040120#p01)のがもう3年前か。そのYARVもついに本体にmergeされたんだよなぁ……