評価と簡約(2)

　研究室の先輩にまたまた教えていただいた。なんかちょっとH研っぽいですよ。
　λ計算には大きくわけて2つの流派がある。ひとつはどこでも好きなところを簡約できるという流派で、もうひとつはいろいろ条件を付けることで簡約できるところを少なくしようとする流派。後者はなにがしたいのかというと、普通のλ式には簡約候補が複数存在するのが嫌（分岐が嫌というのは確かに感覚的に納得できる）なので、簡約候補をなるたけ減らしたい、という事らしい。いろいろ条件を付けるので、前者と後者では正規形の形も変わってくる。つまり、前者ではまだ正規形じゃないけど、後者では簡約できない（＝正規形になってる）という状態が存在する。また、前者は必然的に簡約の前後では式を式に簡約するという形を取るので、そもそも値という呼び方をしない。これ以上簡約できないものは正規形と呼ぶ。後者の場合はうにょーんと一気に正規形に持ってくる、という事をするので、それを値と呼ぶことがある。（前者では簡約候補が複数あるので、一気に正規形に飛ぶ、というような事はしない。）言葉の使い方の問題と言ってしまってもよいのかもしれない。
　ここからはちょっと話題が変わって副作用の話。前者で副作用を入れたいとして考えてみる。λ式M, Nと副作用Eを考えてみる。M -> N という関数に副作用をつけたいときにどうするか。M -> としてみる。つまり、Mを書き換えたらNができるんだけど、Eという副作用もあるので、それも結果として入れておきたいので、結果部分を拡張して、本来の結果と副作用の直積とする。これだと関数の合成とかも考えやすい。例えば…と思ったけれど、例を書くのはめんどくさいのでやっぱりやめる。で、こうすると、関数の合成を考える際にはから本来の結果のNのみを取り出して次の関数に渡す関数とか、Mを<,M>とくるんで次の関数に渡す関数とかを考えると、実際のプログラミングがしやすい、というのはかなり自明のことだと思う。それってbindとreturnじゃん！という事で、副作用を入れるためにはモナドがあると便利だね、という話につながる。