Referential Transparencyの代わりに使える概念案

Referential Transparencyという概念が指すものは漠然としているので、もっと意味が明瞭で使いやすい用語を定義し、色々な言語の性質を記述してみる。

前提として

  • 式は原子式か複合式である。
  • 複合式は関手(functor)と項(argument)から構成される。
〈純粋性〉
「式の意味」と「式の値」は同義である。
〈原子確定性〉
原子式の意味は原子式自身とその原子式の文脈から決定される。
〈構成性〉
複合式の意味は関手および項の意味から決定される。
〈弱構成性〉
複合式の意味は関手、項の意味および式の文脈から決定される。
〈文脈構成性〉
複合式の項の文脈は、その複合式の文脈と関手から決定される。
〈文脈弱構成性〉
複合式の項の文脈は、その複合式の文脈、関手および他の項の意味から決定される。
〈確定性〉
式と式の文脈から部分式の意味が決定される。
〈文脈確定性〉
式と式の文脈から部分式の文脈が決定される。
〈文脈同一性〉
部分式は式全体と同じ文脈を持つ。
〈同値置換可能性〉
部分式を、その式と同値の別の部分式に置き換えても、式全体は同じ意味を持つ。
  • 関手がすべて全関数である数式は〈原子確定性〉〈構成性〉〈文脈同一性〉を持つので、〈確定性〉がある。たとえば、 \{ a \mapsto 2, b \mapsto 3 \}という文脈において、式 a + bは確定した値 5を持つ。また、同じ変数は、ひとつの式の中では常に同じ値を指す。
  • C言語においては普通「式の値」でなく、副作用を含めた「式の動作」が「式の意味」だと考えるので、C言語は〈純粋性〉を持たないと言える。
  • Haskellにおいては普通「式の値」が「式の意味」だと考えるので、Haskellは〈純粋性〉を持つと言える。
  • 関手がすべて全関数である数式に非再帰的なlet式を加えても〈原子確定性〉〈弱構成性〉〈文脈弱構成性〉〈確定性〉は保たれる。

(〈弱構成性〉は、レカナティの「語用論的構成性」と同様の概念か。 http://www.wakate-forum.org/data/tankyu/42/42_09_takaya.pdf