- 693 名前：デフォルトの名無しさん mailto:sage [2017/06/14(水) 00:24:00.03 ID:VydZF3sS.net]
- ["aa","bb",f["cc","dd"]]=["aa","bb","cc","dd"]なるfが存在しないことは、
チャーチ・ロッサー性で説明できる。
チャーチ・ロッサー性は、簡単に言うと、計算の順番を変えても
最終的な計算結果が変わることが無いという性質。
もし上記のようなfがあるとすると、以下の2つの式の計算結果が同じでなければならない。
なぜなら、これら2つの式は、一番内側のfを先に計算するかどうかの違いしかないから。
null(tail(tail(tail ["aa","bb",f["cc","dd"]])))
null(tail(tail(tail ["aa","bb","cc","dd"])))
しかし、計算すればわかるが、上はtrueで下はfalseになるので矛盾する。
よってfは存在し得ない。
本当は、型なしラムダ計算に落としこんでからやる必要があるけど、
(型なしラムダ計算にチャーチ・ロッサー性があることは証明済み)
骨子としてはこんな感じ。
|
 |
