定義するということ、そして読者の信念について。付録: 「関数は呼び出されるまで評価されない、というのは当然の性質だ」の検証

私はこのように言いました。

このように、遅延評価の意味合いは広がっていってしまう可能性があります。言葉を使う前に、いちいち自分の言う「遅延評価」とはこういう意味なんだぞ、と言っておかないと危ないと思います。

http://qiita.com/mandel59/items/8f9111143aea94e7b363#%E9%81%85%E5%BB%B6%E8%A9%95%E4%BE%A1%E3%81%AE%E7%94%A8%E4%BE%8B%E3%81%AE%E6%B7%B7%E4%B9%B1

ここで、「『遅延評価』とはこういう意味なんだぞ、と言っておく」というのは、「議論の前には『遅延評価』を定義せよ」ということです。

そして、kenokabeさんはこう言います。

やはりまず、「評価」の定義を教えていただけますか?

http://qiita.com/mandel59/items/8f9111143aea94e7b363#comment-c280f2286f40deb5a647

つまり「『評価』を定義せよ」ということです。

「定義する」とは、「新しい概念を説明するときに、既知の概念をもって説明する」ことです。

一方で、kenokabeさんは「最悪な説明」について説明しました。

こういう説明の仕方は最悪です。
新しい概念を説明するときに、
別の新しい概念をもって説明することをやってはいけません。
基礎も土台もなく、空中で家を組み立てるに等しい愚行です。

http://qiita.com/kenokabe/items/0dfe134428665d66d757

「最悪な説明をする」とは、「新しい概念を説明するときに、別の新しい概念をもって説明する」ことです。

この文章はいったい「誰」に向けて書いたのか?って思うだけ。

http://qiita.com/mandel59/items/8f9111143aea94e7b363#comment-247ff93d77b06e9e94d4

私はkenokabeさんのために文章を書くことはできません。それは不可能です。私は、いつでも自分自身のために文章を書きます。それは、自分自身で閉じています。たとえ文章がkenokabeさん宛に書かれたように見えても、それは「私の脳内のkenokabeさん」=「私論理上のkenokabeさん」あての文章でしかありません。

私は、kenokabeさんのことをよく知りませんから、脳内のkenokabeさんも不完全です。ですから、私は実体のkenokabeさんにとって、何が既知の概念であり、何が別の新しい概念であるかを判別することはできません。そういうわけで、私はkenokabeさんに向けて「定義」することはできず、いつでもkenokabeさんにとっては「最悪な説明」になってしまいます。

そして、これはkenokabeさんがする説明にも全くあてはまります。kenokabeさんは、自分では自分の言葉の使い方を明確に説明しているといいます。しかし、そこで行われた説明に使われた言葉は、表面上(発音、字面)は同じでも、私が使う言葉とはだいぶかけ離れた、未知のものであって、kenokabeさんの行った「定義」は、私にとっては「最悪な説明」です。例えば、kenokabeさんの先行評価、遅延評価の「定義」を見てみます。

関数、あるいは「クライスリ圏の射」、何でも良いですが、それは「論理」です。
「論理」はこの記事の文脈を踏襲すると「圏論」で論じられる単なる数学構造です。
「クライスリ圏の射」も当然数学構造です。
こういう「論理」はただそこにある。人間の世界、物質世界とは無関係な事象としてアプリオリに存在しています。
1+1を計算しようがしまいが、それが2と同値であるのはアプリオリな論理です。

1+1を計算するのは、端的にいえば、論理の物質化です。
コンピュータで計算すればメモリに展開したり、
暗算で計算すれば人間の脳の神経物質にマッピングされる。

「計算」とは人間の都合による「論理」の物質化であり、
「論理」と「計算」は別事象である。

先行評価戦略では基本的に「論理」=「計算」。
「論理」の宣言がそこにあれば即時に「計算」されてしまう。

遅延評価戦略(CallByNeed、必要呼び)では「論理」≠「計算」。
「論理」の宣言と「計算」のタイミングは一致しない、
(タイミングは過去に逆行しないので、原理的にそれは「遅延になる」)

http://qiita.com/mandel59/items/8f9111143aea94e7b363#comment-247ff93d77b06e9e94d4

先行評価や遅延評価の説明に、「論理」「宣言」「計算」「人間の世界」「物質世界」「論理の物質化」「即時」「タイミングの一致」などの、別の概念を持ってきて説明しています。もし、こういった言葉に対する認識が、私とkenokabeさんとで一致していれば、それは「定義」になるのですが、しかし、残念ながら大きな差異があると思います。つまり、私にとって未知の概念で説明されているわけです。そういうわけで、これは私にとっては「最悪な説明」です。

kenokabeさんが、自分の表現が「定義」になっていることを期待して

ここまではよろしいですね?

http://qiita.com/mandel59/items/8f9111143aea94e7b363#comment-556a6523109653beb687

と書いた時、実際にはぜんぜん「よろしい」=「既知の概念で説明されている」ということになっていないのです。

このような、「定義する」という行為自体が不可能となっている状況を指して、私は「ワード間の関係に互換性ない」という表現を行いました。

この状況では、定義の基礎となる、両者に共通に認識される言葉が欠落しているので、定義の無限後退を引き起こしてしまいます。

「ワード間の関係に互換性がない」というのは、相対的な表現で、どちらが悪い・悪くないということは含意していません。

よって、この「コミュニケーションロス」を生じさせているのは、私ではなく、この記事を書いた本人です。

http://qiita.com/mandel59/items/8f9111143aea94e7b363#comment-247ff93d77b06e9e94d4

とありますが、私はもとから、「kenokabeさんがコミュニケーションロスを生じさせている」というような意味では使っていないのです。

一方で、「典型的」「非典型的」という表現は相対的でない表現です。実際、これは「kenokabeさんの行っているコミュニケーションは多くの人間に対してコミュニケーションにロスがある」という私の主観的観測からの表現なのです。なので、kenokabeさんが「私は多くの人間に理解できるよう説明できている。もし理解できない人間がいれば、それはその人間が非典型だからだ」あるいは「多くの人間に理解できるかどうかはどうでもいい。Ryuseiが理解できるかどうかが問題なのだ」と主張するのであれば、私はこの表現を使うのをやめます。

ともあれ、

というツイートは、「kenokabeさんの行っている説明は多くの人にとって『最悪な説明』である」ということを表しています。

一見、「最悪な説明」には価値がないように思えます。実際、「最悪な説明」はほとんどの場合無価値と見なされます。「最悪な説明」を長々と続けても、そもそも読んでさえもらえないでしょう。しかし、もし読む人が「他人が考えていること」に興味を持っているなら話は別です。「一体全体、この人はなんでこんなわけのわからないことを書くのだろう」と思って、わからないなりに読むのです。基礎も土台もなく、しかしそれでも価値があると信じて読むのです。

私は、kenokabeさんの言葉は、kenokabeさんの言葉の使い方の範囲で、kenokabeさんにとって真であるのだろうと思います。そして、そのことについて異議を差し挟むつもりはありません。私は、kenokabeさんはいい加減に言葉を使っているのではなく、ただ他の人の言葉の使い方とは互換性がないのだ、と解釈します。

しかし、私は私で、私の言葉の使い方の範囲で、私の言葉で「モナドの挙動は遅延評価ではない」といいます。それは私の中なりに、いい加減でない言葉遣いで主張しているのです。私はkenokabeさんの納得のいくやり方で言葉を定義することはできません。それでも、私の言葉は私の中で一貫して使われているのです。

Ryuseiの言葉の使い方はいい加減で、無価値であると思うなら、読まないくていいです。文章に価値があるかどうかは、読んだ人間が自分で決めることだと思っています。しかし、もし、私の言葉が一貫して使われていると信じ、わけのわからないなりに読むつもりがあるのであれば、私の文章を読んでください。そして、私の言葉の使い方は、kenokabeさんの言葉ではどのように説明がつくのかをぜひ書いて下さい。

付録: 「関数は呼び出されるまで評価されない、というのは当然の性質だ」の検証

一応、私の中での「関数は呼び出されるまで評価されない、というのは当然の性質だ」という部分の検証を書いておきます。(これからの説明では項書換えの考え方に則って説明しますが、分かりやすさの都合で用語は変えています。)

式、簡約、値、評価、評価戦略の定義

式を、同値でより簡単な形に変形することを、簡約ということにします。例えば、

(2 × 3) + (5 × 7)

という四則演算を使った式があるとします。2 × 3 = 6なので、この関係を使って式を簡約をすることで

6 + (5 × 7)

という式に変形できます。さらに簡約を繰り返すと、

6 + (5 × 7)
6 + 35
41

となり、ここで式は一番簡単な形になり、これ以上簡約できなくなります。これ以上簡約できない式のことを、値と呼ぶことにします。(項書換えの用語で言えば、正規形のことです。)このとき、与えられた式から値を求めることを、評価と呼ぶことにします。

先ほどの式は、別の順番で簡約することもできます。

(2 × 3) + (5 × 7)
(2 × 3) + 35
6 + 35
41

式のどの部分から簡約を行うのかを決めたルールを、評価戦略*1といいます。二項演算子の左側の式から簡約したり、右側の式から簡約したり、デタラメな順番で簡約したりできますね。しかし、数とその四則演算だけを含む式では、どのような評価戦略であっても必ず値が得られ、しかも評価戦略によらず同じ値が得られます。

λ計算の場合

今の場合は数に対する四則演算で説明しましたが、λ計算の場合は話が複雑になります。λ計算では、式が必ず値を持つとは限らないからです。たとえば、次のλ式を簡約してみてください。

(λx. x x) (λx. x x)

関数の適用の (λV. E) E′ = E[V := E′] という関係を使って簡約(β簡約)すると、

(λx. x x) (λx. x x)

という、最初の式と全く同じ式になります。つまり、この式は簡約が無限にできてしまい、値を持たないということです。

weak equivalence

λ計算では値を持たない式もあるのですが、β簡約は合流性という性質を持つことが知られていますから、任意のλ計算の式eについて、もしeを評価した時に評価戦略1でも評価戦略2でも値を持つならば、評価戦略1で得られた値と評価戦略2で得られた値は等しいということが言えます。この性質は、What is a purely functional language?でいうところのweak equivalenceです。

正格評価

正格評価は、関数の適用 f x を評価する時に、適用される部分の式xを評価してから続きの簡約を行うことを言います。(評価戦略 - Wikipedia)

λ計算では、次の式は正格評価では値を持ちません。

(λx. (λ y. y) 42) ((λx. x x) (λx. x x))

正格評価の定義から、この式を評価するために、いつかは (λx. x x) (λx. x x) の部分を評価しなければいけませんが、それは不可能です。よって、式全体が評価できません。それは、先に (λ y. y) 42 の部分を簡約しても同じことです。

(λx. (λ y. y) 42) ((λx. x x) (λx. x x))
(λx. 42) ((λx. x x) (λx. x x))

しかし、評価戦略が正格でなければ、この式も値を持ちます。先に、一番外側の関数適用の部分から評価すると、

(λx. (λ y. y) 42) ((λx. x x) (λx. x x))
(λ y. y) 42
42

別の順番で簡約してもいいですけれども、

(λx. (λ y. y) 42) ((λx. x x) (λx. x x))
(λx. 42) ((λx. x x) (λx. x x))
42

どちらにしろ、これらは正格評価ではありません。

「関数は呼び出されるまで評価されない、というのは当然の性質だ」について

正格評価の定義では、「正格評価は、関数の適用 f x を評価する時に、適用される部分の式xを評価してから続きの簡約を行う」と言っていました。ここでは、fの部分の簡約をいつ行うのかについては何も言っていません。つまり、(λx. (λ y. y) 42) → (λx. 42) という簡約を行うのか、行わないのかについては、何も言っていないのです。

多くのプログラミング言語で採用されている評価戦略では、λ項の内側の式については簡約・評価を行いません。私が言った「関数は呼び出されるまで評価されない、というのは当然の性質だ」というのは、その性質を指しています。「正格でない評価を行う」ということと「λ項の内側の式については簡約・評価を行わない」ということは別の性質です。

もちろん、プログラムの最適化で行われるインライン展開は、コンパイル時にλ項の内側の式について先に簡約を行う例になっています。その点では、「λ項の内側の式について簡約を行わない」という命題は、偽になるでしょう。しかし、インライン展開は、「λ項の内側の式について簡約を行わない」場合と実行時の結果を変えない範囲で部分的に簡約が行われるのであって、λ項の内側の式を完全に評価することはありません。λ項の内側の式を予め完全に評価するコンパイラーというのも考えられますが、そのコンパイラーはコンパイル時に無限ループになってしまう可能性があります。

以上のことをふまえて、「関数(の内部の式)は呼び出されるまで評価されない、というのは(普通のプログラミング言語では)当然の性質だ」と言えます。そして、この性質は、遅延評価とは別の性質です。

*1:Wikipediaの定義だと「通常決定的な」とありますけど、ここではそのような制約は付けないことにします。非決定なルールでもok。