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

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

前提として

• 式は原子式か複合式である。
• 複合式は関手（functor）と項（argument）から構成される。

〈純粋性〉

「式の意味」と「式の値」は同義である。

〈原子確定性〉

原子式の意味は原子式自身とその原子式の文脈から決定される。

〈構成性〉

複合式の意味は関手および項の意味から決定される。

〈弱構成性〉

複合式の意味は関手、項の意味および式の文脈から決定される。

〈文脈構成性〉

複合式の項の文脈は、その複合式の文脈と関手から決定される。

〈文脈弱構成性〉

複合式の項の文脈は、その複合式の文脈、関手および他の項の意味から決定される。

〈確定性〉

式と式の文脈から部分式の意味が決定される。

〈文脈確定性〉

式と式の文脈から部分式の文脈が決定される。

〈文脈同一性〉

部分式は式全体と同じ文脈を持つ。

〈同値置換可能性〉

部分式を、その式と同値の別の部分式に置き換えても、式全体は同じ意味を持つ。

• 関手がすべて全関数である数式は〈原子確定性〉〈構成性〉〈文脈同一性〉を持つので、〈確定性〉がある。たとえば、という文脈において、式は確定した値を持つ。また、同じ変数は、ひとつの式の中では常に同じ値を指す。
• C言語においては普通「式の値」でなく、副作用を含めた「式の動作」が「式の意味」だと考えるので、C言語は〈純粋性〉を持たないと言える。
• Haskellにおいては普通「式の値」が「式の意味」だと考えるので、Haskellは〈純粋性〉を持つと言える。
• 関手がすべて全関数である数式に非再帰的なlet式を加えても〈原子確定性〉〈弱構成性〉〈文脈弱構成性〉〈確定性〉は保たれる。

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