2002-12-12
λ. ローレンス・レッシグ＠ネットワーク社会論
話は面白かったし、生レッシグも見れたし、大満足。
だけど、終わってみればSOIに後で上がるというじゃありませんかー!! SOIに上がると知っていたら、わざわざ予算編成論をサボってまで聴かなかったっすよ。僕はCODEも読んでないので質問したい事も特に無かったし。ぎゃー、ぎゃー、ぎゃー。
要約か何かをここに書こうかとも思ったけど、どうせSOIに上がるんならいーや。あ、そうそう。creativecommons.orgというのを紹介してました。
ところで、コミケくるってマジですか? 質問すれば良かったかなぁ。(笑)
λ. 予算編成論
こっちは財務省財務総合政策研究所研究部総括主任研究官の田中秀明氏の講演。 レッシグの講演が終わってから覗いてみたら、外債保有量が云々といった話をしていた。聞くところによると、スウェーデンとニュージーランドの財政の話とかがあったそうだ。それから、財務大臣の権限の大きさと財政赤字の量には相関があるという話が面白かったとか。くぅぅ
λ. From Direct Style to Monadic Style through CPS
LtUより。内容は簡単なのだけど、型を考えようとしたら頭が混乱してしまった。S式は型を想像しにくい気がする。
2005-12-12
λ. 今日の「情報教育論」
大岩先生曰く「日本語が情報処理に一番適した言語」「数式 = 英語の省略形」
- g(x) = d/dx f(x)
![\xymatrix{& & {/} \ar@{-}[dl]\ar@{-}[dr] \\ & {+} \ar@{-}[dl]\ar@{-}[dr] & & C \\ A & & B }](tex/8f771b146b236bc863f40c0d30aafb78.png "\xymatrix{& & {/} \ar@{-}[dl]\ar@{-}[dr] \\ & {+} \ar@{-}[dl]\ar@{-}[dr] & & C \\ A & & B }")
- 英語 : prefix : / + A B C
- 日本語 : postfix : A B + C /
- 数式 : infix : (A + B) / C
括弧を導入してまでinfixを選ぶメリットは何か?
- 構造が一覧できる?
- ……
コンピュータが逐次にしか処理できないことを、postfixの理由として挙げるのは変。
欧米人が postfix notation の言語を開発したのは事実だが、infix notation / prefix notation の言語も多く開発しているわけだから、それをもって postfix notation が優れていることの傍証として用いるのは変。
2006-12-12
λ. 今日のIT-system
- GTEdit(Gesture-based Tree Editor)
- GTEDIT: A GESTURE-BASED VISUAL PROGRAMMING ENVIRONMENT FOR TEACHING LISP (GTEdit:ジェスチャを用いた視覚的なLisp教育環境)
- PlanetLab
- Walrus - Graph Visualization Tool
- Skip Graph
λ. スンニ派とシーア派の違い
生徒の作文で宗教対立を扱っていたところから、スンニ派とシーア派の違いの話に。調べてみると、こんな違いがあったのね。へぇ、へぇ、へぇ。
イスラームという宗教が生まれて間もない初期のころ（正統カリフ時代）に、預言者の後継者（ハリーファ（カリフ））を誰にするかという問題において、ムハンマドの従兄弟かつ娘婿であるアリーとその子孫のみがイマームとして後継者の権利を持つと主張したシーア・アリー（「アリーの党派」の意。後に略されて「シーア」、すなわちシーア派となる）に対し、アブー＝バクル・ウマル・ウスマーンのアリーに先立つ三人のカリフをも正統カリフとして認めた大多数のムスリム(イスラーム教徒)がスンナ派の起源である。
2007-12-12
λ. 「Coqで“無限オブ無限”」のyoshihiroさんによる証明
先日のCoqで“無限オブ無限”で書いたCoqのコードが題意を満たすことを、にわとり小屋でのプログラミング日記のyoshihiro503さんが証明してくれました。ありがとうございます。
⇒ Coqで”無限オブ無限”(証明部分)
これは圧巻。面倒そうだとは思っていたものの、なんと500行もの証明に。 ……自分でやらなくて正解だったかも(苦笑
Coqを知らない人はこれを見て何が何だか分からないと思うけど、CoqIDEに読み込ませてステップ実行*1させていくと、ゴールがどう変形されていくかが分かって、何をやってるかが分るはず。といっても、僕もまだ全部はとても理解できていないけど。
*1 Coqは手続き型言語です;-)
