トップ «前の日記(2009-07-04) 最新 次の日記(2009-07-07)» 月表示 編集

日々の流転


2009-07-05 [長年日記]

λ.Referential transparency, definiteness and unfoldability” by Harald Søndergaard and Peter Sestoft

Chatonのhaskell-jpルームで2009-07-032009-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が両立出来ないというのには気付いておらず、なるほどと思った。

Tags: 論文
本日のツッコミ(全5件) [ツッコミを入れる]
ψ タナカコウイチロウ (2009-07-21 07:28)

どうも。遅い書き込みです。<br>参照透明性は、やっぱり、最初はQuineが考えていたんですね。私は、「言語哲学大全 3」(飯田著)から邪推していました。また、プログラミング言語論(?)への導入と、意味の変遷があり、そのようなことを書いてある論文があるのを知りました。

ψ さかい (2009-07-23 00:43)

参照透明性の話は「論理的観点から : 論理と哲学をめぐる九章」 Quine著, 飯田隆訳 なんかにも書いてあって、昔誰かに勧められて参照したような記憶があるのですが、あれはタナカさんではなかったのかなぁ……

ψ タナカコウイチロウ (2009-09-04 12:27)

どうも。相当遅い書き込みです。<br>こちらには記憶が無いんですが…<br>参照透明性とQuineにこだわっていたのは、以前青木さんの日記にコメントで、”そうだとおもうんですけど…”(具体的証拠がない)て感じで書いていて、ちょっとイイスギかなと思ってたもので。という訳です。

ψ さかい (2009-09-04 23:23)

ありゃりゃ。<br>じゃ、たぶん私の記憶違いだと思います。<br>(タナカさんには本を色々紹介していただいているので、他の何かと勘違い手してそう……)<br><br>青木さんの日記のコメントというのは http://i.loveruby.net/d/20060714.html#c01 ですね。

ψ metaphusika (2012-05-27 23:59)

さすがにプログラミング言語の文脈で外延性を参照透過性と同一視するのは計算可能性の観点から不自然ですね。