モナドによる計算の抽象化の発案であるEugenio Moggiの論文

モナド云々が画期的だということでよく紹介される

主張としては、プログラム同士の同値性を考える際に従来の方法では正確性に欠けるので、より正確に扱える手法として圏論のモナドを使おうぜ！というもの

1988年

新規性

従来ではプログラムの意味論といえばラムダ計算だったが、これはβ簡約などによって同じラムダ抽象でも異なる形に表現できてしまうので、ある意味情報を損なうことになる。そこで、この意味論文やに圏論を用いた新しい計算モデルを提案。

大まかな流れ

Introduction

プログラムの等価性には3つのアプローチがあった

論理的観点からのアプローチ

βη簡約を使うと、細かい振る舞いが消えてしまう

なので、たとえ同じ式に簡約されたとしても、それらのプログラムの等価性を正確に同じだとは言えない

例えば副作用とかは表示されない

そこで圏論のトポス上のモナドを用いてこれを表現する

直積型が計算とどう結びつくのか、とか

A categorical semantics of computations

ここからが本質だが未読

『圏論の歩き方』と一緒に読むと良さそう

Extending the language

The λc-calculus

Untyped λc-models

Reduction

Conclusions and further research

圏論をプログラム意味論のフレームワークとして使用できる

計算を改善するために、

圏論的観点で操作的意味論を扱い、

プログラム同士の同値性を正確に導く、

という手法が使える

Acknowledgements

References

面白そうな関連論文

この論文の親にあたるもの

多分この論文のリファレンスには載っていないが、この論文の話をしてる人が挙げてた

気になった英単語・英語表現

参考

『圏論の歩き方』 p.82~