日々の流転

λ. “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が両立出来ないというのには気付いておらず、なるほどと思った。