「大域計算モデルと局所計算モデル」で、計算モデルを少なくとも二種類（それが、大域計算モデルと局所計算モデル）は使ったほうが良さそうだ、と書きました。大域計算モデルは圏論ベースのモデルで、局所計算モデルはその圏のなかの対象を台として構成されます。外の世界である圏が、中のモノである対象に写り込むので、スノーグローブ現象が起きている状況だとも言えます。
ラムダ計算の大域計算モデル、つまり圏論的なモデルというとデカルト閉圏でほぼ決まりなのですが、局所計算モデルはなんだかイッパイ種類があるようです。ラムダ代数（lambda algebra）、ラムダ構造（lambda structure）、組み合わせ代数（combinatory algebra）、適用構造（applicative structure）、型フレーム（type frame）とか。
大域と局所の区別以外に、不純と純粋という分類も意味があるでしょう。僕は「不純な計算」のほうに親しみを感じるのですが、その辺のことは、「操作的意味論と、不純な表示的意味論」とかに書いてあります。不純な計算を扱う基本的な道具は非交替的な積を持つ圏だろうと思っています。特に積がデカルト積（の拡張）である事例としてデカルト作用圏があります。
デカルト作用圏は、モナドのクライスリ圏として構成されることが多いのですが、モナドを考えるよりは、直接的にデカルト作用圏や類似の構造を考えたほうが扱いやすいようです。背後にモナドがいるにしても、いちいちモナドに言及せずに特定の構造を持つ圏として調べたほうが楽な感じですね。特に、たくさんのモナド類似物を一度に扱うときは、インデックス付きフレイド圏が良さそうです。
不純な計算モデルに何を採用するにしても、その部分圏（あるいは係数圏）として“きれいな”モノイド圏が含まれます。このモノイド圏が純粋な計算に対応します。
さて、大域と局所、不純と純粋という分類を考えたとき、どのような組み合わせがよいのでしょうか？ もちろん目的・用途によりけりですが、僕の当面の目的では、次を使おうと思っています。
| ＼ | 大域 | 局所 |
|---|---|---|
| 不純 | デカルト半環作用圏 | Command-Query分離された状態遷移系 |
| 純粋 | デカルト半環圏 | コゥゼンの集合代数 |
デカルト半環作用圏は、デカルト作用圏に直和で足し算を入れたものです。デカルト半環圏は、直積と直和を持つ圏ですが、up-to-isoな計算法則がちゃんと定義されているものです。デカルト半環圏／デカルト半環作用圏はインデックス付きフレイド圏と一緒に使えそうです（たぶん）。
Command-Query分離は、「メイヤー先生の偉大さとCommand-Query分離」で説明しています。Command-Query分離された状態遷移系は、たいへんに扱いやすい状態遷移系（オートマトン）ですね。
コゥゼン（Dexter Kozen）の集合代数は、コゥゼンがtermset algebraと呼んでいるもので、エルブランモデルの作り方を代数構造にしたようなものです。“具体的に構成できる項の集合”の集合の上にいくつかの演算を載せています。少し変形すると、けっこう色々な場面で使えます。
局所計算モデルにラムダ計算のモデルが出てこないのは、大域計算モデルにデカルト閉構造を要求してないからです。デカルト閉構造があればメチャクチャ強力になりますが、強力すぎて扱いにくい面もあります。部分閉構造が妥当かな、と思っています。
デカルト半環圏（純粋部分）とデカルト半環作用圏（不純部分）を一緒に考えることは、可換半環を係数とした非可換半環（半多元環）に関する議論とちょっと似ています。非可換半環上の加群（半加群）は、ファイルシステムやデータベースのようなストレージに相当します（「ストレージの線形代数： 泥臭いデータ操作の洗練された定式化」を参照）。
以上の枠組みは、アマタある計算モデルのなかから適当そうなモノをみつくろって作った1つのレシピです。これは一例に過ぎないので、状況によっては不適切で役立たずかもしれません。僕自身は、けっこうな時間をかけて選んだ組み合わせなので、使いやすいと感じてます。足りてない部分がまだ残ってはいますが*1。
*1:なにが足りてないって、僕の勉強が不足ってのが一番の問題。ちゃんと使いこなせてない。
