2002-07-05
λ. 自然言語論
最終レポートの課題が出た。どれを選ぼうか。
λ. なぜ日銀は介入するのか？
tsさんが勧めているので、5日付日経新聞の「経済教室」欄を読んだ。うーむ。
λ. ホームレス育成ゲーム
あとは、課題で作ってる「ホームレス育成ゲーム」っていうのを近日中にＵＰ する予定です。 もう凄く中途半端な作品に仕上がっており、煮え切らない感 想を知り合いから聞くのが今から楽しみです。
その知り合いの中には僕は入っていないだろうけど、楽しみ。
2005-07-05
λ. 安全保障論 (12)
今日の安全保障論は大塚海夫・一等海佐の講演だった。面白かった。
慶應が、「学問の府で現役自衛官を招くのは不適切」という訳の分からない理由で佐藤正久・一等陸佐の講演を中止した早稲田のような大学でなくて本当に良かった。
2007-07-05
λ. CLEAR FILE
「CLEAR FILE」と書かれているのを見て、代数的仕様記述言語CLEARのファイル形式か何かだと一瞬思ってしまった。疲れてるな。
ちなみに、CLEARは以下のような感じの言語。
constant Triv =
theory
sort element
endth
procedure Prod(A:Triv,B:Triv) =
theory
data sort prod
opns pair: element of A,element of B -> prod
pi1 : prod -> element of A
pi2 : prod -> element of B
eqns all a:element of A,b:element of B,
pi1(pair(a,b)) = a
all a:element of A,b:element of B,
pi2(pair(a,b)) = b
endth
この例はCPLの論文からとってきた例で、ここでは直積型の仕様を記述している。
詳しくはこの辺りの論文でもどうぞ。私は読んだことないけどね。
- Burstall, R. M. and Goguen, J. A. (1980): The Semantics of Clear: A Specification Language. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh.
- Burstall, R. M. and Goguen, J.A. (1982): Algebras, Theories and Freeness: an Introduction for Computer Scientists. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh.
2008-07-05
λ. Morph Endo!: Report on the Tenth Interstellar Contest on Fuun Programming
“Morph Endo!: Report on the Tenth Interstellar Contest on Fuun Programming” by Eelco Dolstra, Jur Hage, Bastiaan Heeren, Stefan Holdermans, Johan Jeuring, Andres Löh, Arie Middelkoop, Alexey Rodriguez, John van Schie, Clara Löh
を読んだ。今年の ICFP Programming Contest ももうすぐだけど、これは昨年の ICFP Programming Contest 2007 (c.f. 参加記録)の出題者らによるテクニカルレポート。 昨年参加したときには丁度入り口付近に辿りついたところで終了という感じで悔しかったのだけど、この先にはこんなに作りこまれた世界が広がっていたのね。 改めて凄いと思った。
去年悔しい思いをした人は、このレポートをガイドにして再挑戦してみるのも楽しいかも。DON'T PANIC!
2009-07-05
λ. “Referential transparency, definiteness and unfoldability” by Harald Søndergaard and Peter Sestoft
Chatonのhaskell-jpルームで2009-07-03と2009-07-04にあった、参照透明性と副作用の定義に関わる話で出てきた論文。積読論文の中にあったので読んでみた。
参照透明性(referential transparency)はQuineによって考えられた概念で、LandinとStracheyによってプログラミング言語の性質として使われるようになった。が、その定義・使われ方は変化しており、それらは同値ではないという話。
それらを、この論文での呼び方で呼ぶと以下のような感じ。
- 確定性 (definiteness)
- 変数がそのスコープの中で単一の値を持つこと。xを変数とすると、x-xは常に0になる。
- 副作用がないこと (absence of side-effects)
- 副作用がないこと。この論文では取り上げていない。
- 決定性 (determinacy)
- 関数の値が引数の値だけから決まること。この論文では取り上げていない。
- 展開可能性 (unfoldability)
- (λx. e1) e2 = e1[e2/x] が成り立つこと。
- 外延性 (extensionality)
- “means that if we wish to find the value of an expression which contains a sub-expression, the only thing we need to know about the sub-expression it its value” [18, page 16] この論文では取り上げていない。 「フレーゲの原理(Frege's Principle)」とか、Principle of compositionality とか言ったほうが馴染み深い人も多いかも。
- ライプニッツ則の適用可能性 (applicability of Leibniz's law)
- “any subexpression can be replaced by any other equal in value” この論文では取り上げていない。
- 参照透明性 (referential transparency)
- 式eの位置pが参照透明なのは ∀e1,e2. e1=e2 ⇒ e[e1/p]=e[e2/p] が成り立つとき。すべての位置が参照透明なとき、その言語は参照透明という。外延性とライプニッツ則の適用可能性に相当。
これらを非決定的な作用的評価順序の言語からはじめて、セマンティクスを変えながら比較している。
- 最初の言語Q0は、非決定的かつ作用的評価順序で、かつ部分式の値ではなく部分式の形によって値が決まる演算子を持つ。Q0は definiteness, unfoldability, 参照透明性のすべてを満たさない。
- Q0を参照透明になるよう少し変更したQ1は、参照透明だが、definiteness, unfoldabilityは満たさない。
- Q1の評価順序を正規順序風にしたQ2は、unfoldabilityは満たすが、definitenessは相変わらず満たさない。
- Q2をdefinitenessを満たすように変更したQ3は、definitenessは満たすが、unfoldabilityは満たさない。
- 非決定性を諦めたQ4はすべてを満たす。
非決定的な言語ではunfoldabilityとdefinitenessが両立出来ないというのには気付いておらず、なるほどと思った。
ψ タナカコウイチロウ [どうも。遅い書き込みです。 参照透明性は、やっぱり、最初はQuineが考えていたんですね。私は、「言語哲学大全 ３」..]
ψ さかい [参照透明性の話は「論理的観点から : 論理と哲学をめぐる九章」 Quine著, 飯田隆訳 なんかにも書いてあって、昔..]
ψ タナカコウイチロウ [どうも。相当遅い書き込みです。 こちらには記憶が無いんですが… 参照透明性とQuineにこだわっていたのは、以前青木..]
ψ さかい [ありゃりゃ。 じゃ、たぶん私の記憶違いだと思います。 (タナカさんには本を色々紹介していただいているので、他の何かと..]
ψ metaphusika [さすがにプログラミング言語の文脈で外延性を参照透過性と同一視するのは計算可能性の観点から不自然ですね。]
