分析哲学とコンピュータ科学では、参照の透明性と参照の不透明性は言語構造の特性であり、[ a ]ひいては言語の特性です。言語構造は、そこから構築された任意の式について、部分式を同じ値を表す別の部分式に置き換えても式の値が変化しない場合に、参照的に透明であると呼ばれます。[ b ] [ 1 ] [ 2 ] それ以外の場合は、参照的に不透明であると呼ばれます。参照的に不透明な言語構造から構築された各式は、部分式について何かを述べていますが、参照的に透明な言語構造から構築された各式は、部分式についてではない何かを述べています。つまり、部分式は式に対して「透明」であり、単に他の何かへの「参照」として機能します。[ 3 ]例えば、言語構造「_は賢かった」は指示が透明である(例:ソクラテスは賢かったは西洋哲学の創始者は賢かったと同義である)が、「_は言った」は指示が不透明である(例:クセノフォンは「ソクラテスは賢かった」と言ったは、クセノフォンは「西洋哲学の創始者は賢かった」と言ったとは同義ではない)。
プログラミング言語における参照の透明性は、式の指示対象間の意味的等価性、あるいは式自体の文脈的等価性に依存します。つまり、参照の透明性は言語の意味論に依存します。したがって、宣言型言語と命令型言語の両方とも、与えられた意味論に応じて、参照的に透明な位置、参照的に不透明な位置、あるいは(通常は)その両方を持つことができます。
参照透過性を持つ位置の重要性は、プログラマとコンパイラがそれらの位置における書き換えシステムとしてプログラムの動作を推論できる点にあります。これは、正当性の証明、アルゴリズムの簡略化、コードを壊さずに変更する際の支援、メモ化、共通部分式の削除、遅延評価、定数畳み込み、並列化などによるコードの最適化に役立ちます。
この概念は、アルフレッド・ノース・ホワイトヘッドとバートランド・ラッセルの『プリンキピア・マテマティカ』(1910~1913年)に端を発している。[ 3 ]
真偽を伝える手段としての命題は特定の出来事であるのに対し、事実として考察される命題は類似した出来事の集合である。「Aはpを信じている」や「pはAに関するものである」といった文に現れるのは、事実として考察される命題である。
もちろん、「ソクラテスはギリシャ人である」という特定の事実について述べることは可能です。例えば、その長さが何センチメートルか、黒いなどと言うこともできます。しかし、これらは哲学者や論理学者が述べようとするような発言ではありません。
主張が行われるとき、それは主張される命題の具体例である特定の事実によってなされます。しかし、この特定の事実は、いわば「透明」です。つまり、その事実自体については何も語られず、その事実を通して何か別のことが語られるのです。真理関数の中で現れる命題に備わっているのは、まさにこの「透明」な性質です。これは、pが主張されるときにはpに備わっていますが、「 pは真である」と言うときには備わっていません。
分析哲学では、ウィラード・ヴァン・オーマン・クワインの『言葉と対象』(1960年)で採用された。 [ 1 ]
文中で単数形の語が純粋にその目的語を指定するために用いられ、かつその文がその目的語に関して真である場合、同じ目的語を指定する他の単数形の語を代入しても、その文は必ず真のままとなる。ここに、純粋に指示的な位置と呼べるものの基準がある。すなわち、その位置は同一性の置換可能性に従わなければならない。
[…]
参照的透明性は構文(§ 11)に関係しており、より具体的には、単数語または単数文が単数語または単数文に含まれる様式に関係しています。単数語tの出現が語または文ψ ( t )の中で純粋に参照的である場合、包含語または文φ ( ψ ( t ))の中でも純粋に参照的である場合、包含様式 φ は参照的に透明であると私は言います。
この用語は、クリストファー・ストラッチーの画期的な講義ノート「プログラミング言語の基本概念」(1967年)におけるプログラミング言語の変数に関する議論の中で、現代のコンピュータ科学での使用法として登場しました。 [ 2 ]
式の最も有用な特性の1つは、クワイン[4]が参照的透明性と呼んだものです。これは本質的に、部分式を含む式の値を求めたい場合、部分式について知る必要があるのは値だけであることを意味します。部分式の内部構造、構成要素の数と性質、評価の順序、または記述に使用したインクの色など、部分式のその他の特徴は、主式の値とは無関係です。
形式言語における置換性には、参照の透明性、明確性、展開可能性という3つの基本的な特性がある。[ 4 ]
構文上の等価性を≡で、意味上の等価性を=で表すことにしよう。
位置は自然数の列によって定義されます。空の列はεで表され、列構成子は「.」で表されます。
例。—式(+ ( ∗ e 1 e 1 ) ( ∗ e 2 e 2 ))の 2.1 位は、 e 2が最初に出現する位置です。
位置pに式e′を挿入した式eは、e [ e′ / p ]と表記され、次のように定義される。
例。 — e ≡ (+ ( ∗ e 1 e 1 ) ( ∗ e 2 e 2 ))の場合、e [ e 3 /2.1] ≡ (+ ( ∗ e 1 e 1 ) ( ∗ e 3 e 2 ))となります。
式eにおける位置pは純粋に参照的であり、次のように定義される。
言い換えれば、式における位置が純粋に指示的であるのは、それが等号の置換の対象となる場合に限る。εはすべての式において純粋に指示的である。
演算子Ωは参照透過性であり、iは次のように定義される。
それ以外の場合、 Ωは位置iにおいて参照的に不透明である。
演算子が参照的に透明であるとは、すべての場所で参照的に透明であることを意味します。そうでない場合は、参照的に不透明です。
形式言語が参照透過的であるとは、そのすべての演算子が参照透過的であることによって定義される。そうでない場合は、参照不透明である。
例: — '_ lives in _' 演算子は参照透過性があります。
実際、第二の位置は主張において純粋に指示的な意味合いしか持たない。なぜなら、「ロンドン」を「英国の首都」に置き換えても、主張の妥当性は変わらないからである。第一の位置も、同様の置き換えの理由から、純粋に指示的な意味合いしか持たない。
例: — '_ には _ が含まれます' および引用符演算子は参照的に不透明です。
実際、文の最初の位置は純粋に指示的なものではありません。なぜなら、 「ロンドン」を「英国の首都」に置き換えると、文と引用符の値が変わってしまうからです。したがって、最初の位置では、「_ には _ が含まれる」という記号と引用符演算子によって、式とそれが示す値との間の関係が破壊されます。
例:引用符演算子の参照不透明性にもかかわらず、「_ は _ を参照する」演算子は参照透過性を持つ。
実際、文中の最初の位置は純粋に参照的ですが、引用文中ではそうではありません。なぜなら、「ロンドン」を「英国の首都」に置き換えても文の値は変わらないからです。したがって、最初の位置では、「_ は _ を参照する」演算子によって、式とそれが示す値との関係が回復されます。2番目の位置も、同じ置換の理由で純粋に参照的です。
形式言語は明確であり、そのスコープ内の変数のすべての出現箇所が同じ値を表すことによって定義されます。
例:数学は明確である。
実際、2回出現するxは同じ値を表しています。
形式言語が展開可能であるとは、すべての式がβ還元可能であることによって定義される。
例:ラムダ計算は展開不可能である。
実際、((λ x . x + 1) 3) = ( x + 1)[3/ x ]。
参照の透明性、明確性、展開可能性はそれぞれ独立している。明確性は、決定論的言語においてのみ展開可能性を意味する。非決定論的言語は、明確性と展開可能性を同時に持つことはできない。
{{cite book}}ISBN /日付の不一致(ヘルプ){{cite book}}ISBN /日付の不一致(ヘルプ)