評価と簡約
ボスの人に聞いてみた。一番大きな違いは、
- 簡約は式を書き換えて式を作る。
- 評価は式に対して値を返す。
というところであるそうな。簡約は定義域も値域も式。評価は定義域は式で値域は値。
例えば、(1+2)+(3+4)という式を考える。簡約する場合は3+(3+4)もしくは(1+2)+7と書き換えられて、さらに書き換えると10に合流する(チャーチ・ロッサー性という奴ですね)。この場合の10は簡約化できない、つまり正規形の式。評価の場合は評価戦略によってどこから評価するかはわからんけど、とにかく途中で3+(3+4)という式は出てこない。(1+2)+(3+4)を評価すると10という値が返ってくる。
「簡約は式の書き換えであって、副作用という概念の入り込む余地が無さそうだが、評価は副作用という概念を入れる余地がある様に見える。この印象は正しいか、間違っているか?」という質問には間違ってはいないだろうという評価が得られた。
さらに先輩にも聞いてみた。small stepが簡約で、big stepが評価、という答えが帰ってきた。簡約が、式の簡約可能な部分をひとつ書き換える操作である、という点に関しては、おそらく異論はないであろうが、評価に関しては人それぞれの定義があるかもしれない、とのこと。
big stepという単語で検索をかけると、d:id:sumii:20060520:1148128716がみつかった。(というか、この記事は見覚えあるな…orz)これも要約するとsmall stepが簡約でbig stepが評価と書いてある。
ボスの意見もこれらの記述とは特に矛盾しなさそうだ。(計算としてλ計算を想定するなら、評価の場合にも明らかに定義域、値域ともに関数になるけども、まぁ細かいところは気にしない。)というわけで、かしこそうな3人の意見を総合すると、簡約はsmall step reductionで評価はbig step reductionである、という事は間違い無さそうに見える。
簡約において副作用という概念の入り込む余地があるか、ないか、という問題に関しては、この「簡約→small step, 評価→big step」という考えの元ではあまりなにも言えないというか、簡約においても評価においても副作用の扱いは同様に難しいね、という感じな気がする。