3月に入っても寒い、よって、体調わろし。あー、イヤだ。
ソフトウェアの設計や実装の際に、計算モデルを持たないと何か不安だし、方針も立ちにくいですね。それで、計算モデルを考えるのですが、単一の計算デルではなく、何種類かを使い分けることがあります。「何種類か」とは言っても、まー2種類あればだいたい足りるかな。でも、1つだけでは不足な感じがします。
2つの計算モデルを考える場合、1つは比較的に概念的で、もう1つは実装に近いものです。これらを、概念モデルと実装モデルとか言いたくなるのですが、そう言ってしまうとチョット違う。なーんか違う。事実を歪めたり誤解を招く気がしていたのです。最近、これを「大域計算モデル」と「局所計算モデル」と呼べばいいのじゃないか、と思いました。
2つの計算モデルが出てくる典型的な例はラムダ計算です。ラムダ計算の圏論的モデルはデカルト閉圏です。しかし、いつでも圏論を使うかというとそうではありません。適用構造とかラムダ代数とかの構造を使うこともあります。スコットが作ったラムダ計算の記念碑的なモデルは、自然数のベキ集合Pωのなかでゴニョゴニョします。
Pωのようなモデルは具体的でいいのですが、なにゆえにPωがラムダ計算のモデルになっているかはハッキリしません。具体物を目の前に出されて、「これはラムダ計算のモデルでしょ」と言われれば確かにそうなんですが、「なぜそれを出したの？」「他のモデルはないの？」「どうしてそれなの？」という疑問は残ります。
ラムダ代数は、ラムダ計算のモデルが満たすべき構造を公理化したものです*1。Pωがラムダ計算のモデルであることは、Pωがラムダ代数になっている（あるいはラムダ代数を作れる）ことで説明できます。
ここでデカルト閉圏に目を向けて： デカルト閉圏Cの対象Xが、XX⊆X とみなせるとき反射的対象と呼びます。記号「⊆」の部分は、圏論の言葉だけで書き下す必要がありますが、雰囲気的には「自分自身のベキを自分に埋め込める領域」がXです。このようなXをもとにしてラムダ代数が作れます。
デカルト閉圏Cの対象が、任意の対象を埋め込めるとき、それは万能対象（universal object）と呼びます。Uが万能（普遍的）なら、UU→U と埋め込めるので反射的になります。UはCのスノーグローブ対象だとも言えます。外の圏Cの構造を対象Uのなかでソックリ再現できます。つまり、外の圏Cと中の対象Uの関係はメタ巡回的となっています。
「ラムダ計算、デカルト閉圏、ラムダ代数」の場合は、メタ巡回構造がハッキリとしているのですが、ここまでうまくいかないまでも、なんとなくメタ巡回的なことはあります。スノーグローブが外の世界と少しズレている、歪んでいる、くもっている、という感じです。
最近僕がよく使っているモデルはデカルト半環圏です。デカルト半環圏は、デカルト閉圏のように閉構造（指数、ベキ）を持たないので、きれいなスノーグローブ（メタ巡回構造）は作れません。それでも、ある程度の構造を備えた対象を探すと、その対象のなかに外の圏をだいたいは写し込むことができます。
冒頭で言った2つのモデル -- 大域計算モデルと局所計算モデル -- とは、外の圏と中の対象のことです。広くて自由な世界、マクロコスモスとして外の圏＝大域計算モデルがあります。大域計算モデルの内部のデータ領域で、ある程度豊かな構造を持つものは、世界全体のミニチュアとなるミクロコスモスを形成します。これが局所計算モデルです。
大域計算モデルのほうが制約が少なく見通しがいいのですが、設計や実装の考察には局所計算モデルのほうが向いています。つまり、どちらか一方では不足で両方を使ったほうがいいというわけです。
*1:ラムダ代数とよく似たラムダモデルという構造もあります。微妙に違うようですが、その違いを僕はよく知りません。
