参照の透明性

分析哲学とコンピュータサイエンスでは、参照の透明性と参照の不透明性は言語構造の特性であり、^[1]言語の拡張である。言語構造は、そこから構築された任意の式について、部分式を同じ値を表す別の部分式に置き換えても^[2]式の値が変わらない場合、参照透明であると呼ばれる。^[3]^[4]それ以外の場合、参照不透明であると呼ばれる。参照不透明な言語構造から構築された各式は部分式について何かを述べているのに対し、参照透明な言語構造から構築された各式は部分式について何も述べていない。つまり、部分式は式に対して「透明」であり、単に他の何かへの「参照」として機能する。^[5]例えば、「_は賢かった」という言語構造は指示的には透明である（例えば、ソクラテスは賢かったは西洋哲学の創始者は賢かったと同義である）が、「_は_と言った」は指示的には不透明である（例えば、クセノポンは「ソクラテスは賢かった」と言ったはクセノポンは「西洋哲学の創始者は賢かった」と言ったとは同義ではない）。

プログラミング言語における参照の透明性は、式の表示間の意味的等価性、または式自体の文脈的等価性に依存します。つまり、参照の透明性は言語のセマンティクスに依存します。したがって、宣言型言語と命令型言語はどちらも、与えられたセマンティクスに応じて、参照が透明な位置、参照が不透明な位置、または (通常は) その両方を持つことができます。

参照透過的な位置の重要性は、プログラマーとコンパイラーがそれらの位置での書き換えシステムとしてプログラムの動作を推論できることです。これは、正しさの証明、アルゴリズムの簡素化、コードを壊さずに変更することの支援、メモ化、共通部分式の削除、遅延評価、並列化によるコードの最適化に役立ちます。

歴史

この概念はアルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルの『プリンキピア』（1910-1913）に由来している。^[5]

真実か虚偽かを伝える手段としての命題は特定の出来事ですが、事実として考えられる命題は類似の出来事の集合です。「A はp を信じている」や「p はAに関するものである」などの文に現れるのは、事実として考えられる命題です。
もちろん、「ソクラテスはギリシャ人である」という特定の事実について述べることは可能です。長さが何センチか、黒いか、などと言うことはできます。しかし、これらは哲学者や論理学者が言いたくなるような発言ではありません。
主張が行われるとき、それは特定の事実によってなされ、その事実は主張された命題のインスタンスです。しかし、この特定の事実は、いわば「透明」です。つまり、それについては何も言われていませんが、それを通して何か他のことについて何かが言われています。この「透明」な性質こそが、真理関数に現れる命題に属するものです。これは、pが主張されるときにはpに属しますが、「 pは真である」と言うときには属しません。

これはウィラード・ヴァン・オーマン・クワインの『言葉と対象』（1960年）で分析哲学に採用された。 ^[3]

単数名詞が文中で純粋にその目的語を指定するために使用され、その文がその目的語について真である場合、同じ目的語を指定する他の単数名詞に置き換えてもその文は確実に真のままである。ここに、純粋に指示的な位置と呼べるものの基準がある。つまり、その位置は同一性の代替性に従わなければならない。
[…]
参照透明性は構文（§ 11）に関係しており、より具体的には、単数名詞または単数文における単数名詞または単数文の包含モードに関係している。単数名詞 $t$ の出現が用語または文 $ψ$ $($ $t$ $)$ 内で純粋に参照的である場合、包含用語または文 $φ$ $($ $ψ$ $($ $t$ $))でも純粋に参照的である場合、包含モード$ $φ を$ 参照透過的と呼ぶ。

この用語は、クリストファー・ストラチーの有名な講義ノート『プログラミング言語の基本概念』（1967年）におけるプログラミング言語の変数に関する議論の中で、当時のコンピュータサイエンスの用法で登場した。 ^[4]

式の最も有用な特性の 1 つは、Quine [4] が参照透明性と呼ぶものです。本質的には、部分式を含む式の値を求める場合、部分式について知っておく必要があるのは、その値だけです。部分式のその他の特徴、たとえば内部構造、構成要素の数と性質、評価される順序、書き込まれたインクの色などは、主式の値とは無関係です。

正式な定義

形式言語における代替性に関する基本的な性質は、参照透明性、明確性、展開可能性の3つである。^[6]

構文上の等価性を ≡ で表し、意味上の等価性を = で表します。

参照の透明性

位置は自然数のシーケンスによって定義されます。空のシーケンスは ε で示され、シーケンスコンストラクタは '.' で示されます。

例:式 $(+ (* e 1 e 1) (* e 2 e 2))の位置 2.1 は、$ $e 2$ が最初に出現する場所です。

式 $e'が$ 位置 $p$ に挿入された式 $e$ は $e$ $[$ $e'$ $/$ $p$ $]$ で表され、次のように定義されます。

e [e' /ε] \equiv e'

すべての演算子Ω

と式

e 1 、\dots、 e n について、

e

[

e'

/

i

.

p

]

\equiv <Ω

e

1

\dots

e

i

[

e'

/

p

] \dots

e

n

>

e \equiv <Ω

e

1

\dots

e

i

\dots

e

n

>

の

場合

、それ

以外

の場合は未定義

です

。

例。 — $e \equiv (+ (* e 1 e 1) (* e 2 e 2))$ の場合、 $e [e 3 /2.1] \equiv (+ (* e 1 e 1) (* e 3 e 2))$ 。

位置 $pは$ 式 $eにおいて$ 純粋に参照的なものであり、次のように定義される。

e 1 = e 2

は、すべての式

e

1

、

e

2に対して、

e [e 1 / p] = e [e 2 / p]

を意味します。

言い換えれば、位置は、等号の置換性の対象となる場合にのみ、式内で純粋に参照的です。ε $は$ すべての式で純粋に参照的です。

演算子 $Ωは$ $i番目$ の場所で参照透過的であり、次のように定義される。

p は

e i

implies

i

において純粋に参照的です

。p

は

、すべての位置p

と式

e

1

, \dots,

e

n

について、

e \equiv <Ω e 1 \dots e i \dots e n >

において純粋に参照的です。

それ以外の場合、 $Ω は$ $i$ 番地では参照的に不透明です。

演算子が参照透過的であるとは、すべての場所で参照透過的であることによって定義されます。それ以外の場合は、参照不透明です。

形式言語が参照透過的であることは、そのすべての演算子が参照透過的であることによって定義されます。そうでない場合は、参照不透明です。

例: '_ lives in _' 演算子は参照透過的です:

彼女はロンドンに住んでいます。

実際、2 番目の位置は、主張において純粋に参照的です。なぜなら、ロンドンを英国の首都に置き換えても、主張の値は変わらないからです。最初の位置も、同じ代替性の理由により、純粋に参照的です。

例: '_ contains _' および引用符演算子は参照的に不透明です。

「ロンドン」には6文字が含まれます。

実際、最初の位置はステートメント内で純粋に参照的ではありません。ロンドンを英国の首都に置き換えると、ステートメントと引用符の値が変わるからです。したがって、最初の位置では、「_ は _ を含む」演算子と引用符演算子によって、式とそれが示す値の関係が破壊されます。

例: '_ refers to _' 演算子は、引用演算子の参照不透明度にもかかわらず、参照透過的です。

「ロンドン」はイギリス最大の都市を指します。

実際、最初の位置は引用文ではありませんが、文の中では純粋に参照的です。これは、ロンドンを英国の首都に置き換えても文の値は変わらないためです。したがって、最初の位置では、「_ refers to _」演算子によって、式とそれが示す値の関係が復元されます。2 番目の位置も、同じ置換性の理由により純粋に参照的です。

明確さ

形式言語は、そのスコープ内での変数のすべての出現が同じ値を表すことによって定義されます。

例:数学は明確です:

3 x 2 + 2 x + 17

。

実際、2 回の $x$ の出現は同じ値を表します。

展開性

形式言語が展開可能であることは、すべての式がβ 還元可能であることによって定義されます。

例:ラムダ計算は展開可能です:

((λ x . x + 1) 3)

.

実際、 $((λ x . x + 1) 3) = (x + 1)[3/ x]$ です。

プロパティ間の関係

参照透過性、明確性、展開可能性はそれぞれ独立しています。明確性は決定論的言語に対してのみ展開可能性を意味します。非決定論的言語は明確性と展開可能性を同時に持つことはできません。

参照

参考文献

^ 言語構造（包含モード、文脈、演算子とも呼ばれる）は、穴のある表現です。
^ ここで、値とは式の表示内容 (意味、オブジェクト、または参照先とも呼ばれる) であり、評価プロセスの結果ではありません。
^ ab クワイン、ウィラード・ヴァン・オーマン（1960年）。『言葉と対象』（第1版）。マサチューセッツ州ケンブリッジ：MIT出版。144ページ。ISBN 978-0-262-17001-7。
^ ab Strachey, Christopher (1967).プログラミング言語の基本概念(技術レポート). コペンハーゲンで開催された国際コンピュータプログラミングサマースクールの講義ノート。また、Strachey, Christopher (2000)「プログラミング言語の基本概念」高階および記号計算。13 (1–2): 11–49。doi : 10.1023 /A : 1010000313106。S2CID 14124601 。
^ ab ホワイトヘッド、アルフレッド・ノース;ラッセル、バートランド(1927)。プリンキピア・マセマティカ。第 1 巻 (第 2 版)。ケンブリッジ: ケンブリッジ大学出版局。p. 665。ISBN 978-0-521-06791-1。
^ Søndergaard, Harald; Sestoft, Peter (1990). 「参照の透明性、明確性、展開可能性」(PDF) . Acta Informatica . 27 (6): 505–517. doi :10.1007/bf00277387.

外部リンク

http://userpage.fu-berlin.de/~ram/pub/pub_jf47ht81Ht/referential_transparency
https://stackoverflow.com/a/9859966/655289、Uday Reddy 教授 (バーミンガム大学)
http://okmij.org/ftp/Computation/PrincipiaMathematica.txt

[1] 言語構造（包含モード、文脈、演算子とも呼ばれる）は、穴のある表現です。

[2] ここで、値とは式の表示内容 (意味、オブジェクト、または参照先とも呼ばれる) であり、評価プロセスの結果ではありません。

[quine1960-3] クワイン、ウィラード・ヴァン・オーマン（1960年）。『言葉と対象』（第1版）。マサチューセッツ州ケンブリッジ：MIT出版。144ページ。ISBN 978-0-262-17001-7。

[strachey1967-4] Strachey, Christopher (1967).プログラミング言語の基本概念(技術レポート). コペンハーゲンで開催された国際コンピュータプログラミングサマースクールの講義ノート。また、Strachey, Christopher (2000)「プログラミング言語の基本概念」高階および記号計算。13 (1–2): 11–49。doi : 10.1023 /A : 1010000313106。S2CID 14124601 。

[whitehead1927-5] ホワイトヘッド、アルフレッド・ノース;ラッセル、バートランド(1927)。プリンキピア・マセマティカ。第 1 巻 (第 2 版)。ケンブリッジ: ケンブリッジ大学出版局。p. 665。ISBN 978-0-521-06791-1。

[sondergaard1990-6] Søndergaard, Harald; Sestoft, Peter (1990). 「参照の透明性、明確性、展開可能性」(PDF) . Acta Informatica . 27 (6): 505–517. doi :10.1007/bf00277387.