プログラムの意味付けから始める計算効果（computational effects）入門

はじめに

自分の理解の整理も込めてまとめてみました。
ほとんど計算機科学に数学的関数を導入するくだりの話で力尽きました。
間違いや事実誤認があればご指摘いただければありがたいです。

参考にしたもの

ちゃんと理解できたとは全く言ってない。

• 淵一博+黒川利明 編著(1986) 新世代プログラミング 主に95頁（133頁も）の図
• E.Moggi(1989) An Abstract View of Programming Languages 第三章 モナドとしての計算概念
• E.Moggi(1989) Computational lambda-calculus and monads 冒頭だけ
• E.Moggi(1991) Notions of computation and monads 冒頭だけ
• S.マックレーン 数学-その形式と機能 pp.163-167

プログラムとは？８０年代的状況

２つ異なるプログラムが与えられたとき、性質も含めてその２つのプログラムが同一のものか否かを厳密に答える理論が欲しい、としよう。
プログラムの記述が全く同じだったら同一言語処理系で実行する分にはその性質も含めて同じ結果を返すので同一であることはわかる。でもプログラムは記述をちょっと変えるだけでも大きく動作が変わってしまうことになるので、プログラムの構文の世界で同一だいや違うということを言っていても筋が悪い。
こういうときはプログラムを、それ自体が比較可能な直観的なものにマッピングしてしまってから比較すればいい。

つまり、構文上は似ても似つかないプログラム１とプログラム２があるとき、その比較を行うにあたっては、

• プログラム１　＝＞　なにか意味するものA
• プログラム２　＝＞　なにか意味するものB

というように割り当てしてから、A＝BかA！＝Bかを検討すればいいわけである。

だとすると、プログラムをなにか意味するものに割り当てる方法が必要になってくるわけだが、どういう方法が適切だろうか。

80年代に刊行（1986）された新世代プログラミング（淵一博、黒川利明編著）という本によれば、スローガン的に以下の頁の下図のように分類できる（そうしても怒られることはないよう）である。

この分類によれば、プログラムというものへのアプローチの方法としては、

• 関数的なアプローチ（操作的意味論、表示的意味論）
• 論理的なアプローチ（公理的意味論など）

の２つに大別できるそうである。

ただ、論理的なアプローチについては、プログラミング言語依存であったり、どういう手法をとるかということを決定した上でそのルールに従ってやらないと意味をなさない要素が多く、一般的なプログラミングにおけるプログラムの意味付けとは両立しないようなので今回考えない。

というわけで、「プログラムとは関数である」という、プログラムと数学の関数を対比させるというある意味おなじみの説明となる。だが、ここで、そもそも数学における関数とはなんだろうか。

数学における「関数」の概念

S.マックレーン著「数学－その形式と機能」によると以下である。

pp.163-164の抜粋

ある意味なじみ深い上記の関数定義はすべて現代数学では用いられない曖昧な定義ということである。というわけで、数学における関数の正式な定義としては以下になるという形でつながる。167頁。

この数学的関数概念は、どちらかというとプログラミング言語では関数・手続き（procedure）よりも連想配列（associative array）の方が近い。

これを踏まえて「プログラムとは何か？」のスローガンの図に戻ると、なんかちょっと表現が不自然である。操作的意味論と表示的意味論の違いをニュアンスで出すために表現を変えているともとれるが、数学的関数概念は一つだけなのに２つ関数概念があるように読めてしまうのはなんだか変である¹。

もしかしたら、80年代においては計算機科学者の間で数学的関数概念の共通認識を得ることができていなかったのではないか、という疑いを持つのはこれを根拠にして突飛な考えではない言えると思う²。

別にどうでもいいじゃないか。という声もあるかもしれないが、プログラムの意味付けに数学的関数を使っていないとなると、

• なにかプログラムの理論があるとして、その理論的根拠として数学の盤石な土台を利用できない
• 「関数」とは名ばかりのあいまいな関数概念で構成されていると、関数の一般理論（a general theory of functions）である圏論を適用できない（しても数学側からは認められない）³。

というデメリットがある。理論家であればあるほど、計算機科学の理論における関数概念は数学的関数概念で統一したいだろうというのは想像に難くない。

数学的関数もといλ項（βη簡約の系）とプログラムを同一視すること

このような状況の80年代の末に出てきたのがEugenio Moggiである。Moggiは「プログラムとは何か？」のスローガンでいうところの問いを以下のように組み立てて、「プログラムとは数学的関数である」というスローガンを導入した。

• プログラムはλ項に同一視できるので、λ計算はプログラミング言語の研究において有用な数学的道具である
• でも、βη簡約の理論を適用するとすると、プログラムとはvalueからvalueへの全域関数 ということになっちゃうよ
• ＝＞（全域関数（total function）とは数学的関数のことなので）プログラムとは数学的関数である というスローガンが形を変えて導入されることになる。

計算効果（computational effects）

長々と「プログラムとは数学的関数である」というプログラム観をどう導入するかの説明をしてきたが、これは正直いうと現実のプログラムをちゃんと反映しているプログラム観ではない。数学的関数が連想配列に近いということを思い出してほしいが、「プログラムは数学的関数である」というスローガンは、プログラムをする目的である「計算する」という行為を全く表現できていないのである。
Moggiは論文"Notions of computation and monads"で以下のように表現した。

我々は、プログラムの等価性を証明するための出発点として、βη簡約の理論は採用しない、これは、A→B型のプログラム（手続き）の表示的意味を、AからBへの全域関数と同一視するものである、なぜなら、この同一視は、非停止性、非決定性、副作用など、実際のプログラムが示しうる振る舞いを完全に排除してしまうからである。

さんざん数学的関数について語っておきながら、この結果である。数学的関数では非停止性とか非決定性、副作用といった効果を表現できないのである。

ただ、悪いことばかりではない、数学的関数を用いたことによって、処理して値を返すという機構の部分と、計算するというプロセスの結果得られる副次的な効果という部分を切り分けすることができるようになるのである。

この切り分けされた、現実のプログラムの数学的関数では表現しきれない効果でMoggiの理論の枠組みに従うもののことを、計算効果（computational effect） と呼ぶのである。

長くなったので続く（かも）。

1. 念のため「新世代プログラミング」において関数が変換操作であったりグラフであるということについて説明している箇所を示しておきます。少なくともこれをどうとらえるかについては幅があるといえるのではないでしょうか。
   「新世代プログラミング」93頁。
   ↩

2. これは決してScottやPlotkinが数学的関数の概念を知らずに理論を組み立てたとかそういうことを言っているわけではないです。理論として専門家から認められたけれど、その専門家の間でも関数概念の認識には統一性がとれていなかったのではないか？という話です。 ↩

3. 文献を読んでいく限り、個人の印象として、当時は結構この圏論を適用するニーズはでかかったように思います。 ↩