もともとのマイヒル／ネロードの定理は、形式言語理論のなかに位置付けられるものです。しかし僕は、プログラム意味論のなかでマイヒル／ネロードの定理を捉えています。一般化されたマイヒル／ネロードの定理は、プログラムの構文と意味に関して様々なことを教えてくれます。そのこと（の一部）は次の記事に書きました。
リアルな問題に対して、マイヒル／ネロードの定理は具体的に応えて（答えて）くれます。しかし、この「リアルさ」「具体性」がなかなか伝わらない。どうしてでしょう？ 大きな障害は文化的なギャップだろうと思います。
リアルな問題に共感してくれる人が相手であっても、圏論を使った議論をすると、往々にしてアブストラクト・ナンセンス（抽象的空論）と敬遠されてしまいます。一方、圏論を理解している人でも、リアルな問題に馴染みがなければ動機が分からず、「なんのためにソレやってんの？」となります。
このギャップはなんとかしたいのですが、難しい問題ですね。せめて、言葉の翻訳規則くらいは提供しましょう。異なる文化で使われている言葉はまるで違っていて、翻訳なしには理解不能ですから。
引き続く節で、「一般化されたマイヒル／ネロードの定理 1：準備と事例」で導入した圏論／グラフ理論／形式言語理論などの言葉が、プログラム／ソフトウェアでは何に対応するのかを説明していきます。
内容：
- プログラムのモデルとしての一般化オートマトン
- 指標グラフに関する言葉
- 指標圏に関する言葉
- 関手に関する言葉
プログラムのモデルとしての一般化オートマトン
「一般化されたマイヒル／ネロードの定理 1：準備と事例」において僕がセットアップしたのは、プログラムの構文論と意味論のための枠組です。これは、形式言語理論／オートマトン理論の枠組を一般化しています。しかし、プログラム意味論としては極めて限定的でプアなものです。
プログラムに制御構造はなくて、出来ることは順次実行だけです。if文（条件分岐）もwhile文（繰り返し）もなく、再帰も出来ません。プアですよね。非決定性分岐は簡単に入れられますが、今回はそれも入れてません。
プログラムの基本構成素である関数や手続きは1引数だけです。引数なしはユニット型（シングルトン型）の1引数で表せます。多引数を単一タプル引数でシミュレートすれば、それほど大きな制限ではないかも知れません。でも、引数を持つ状態遷移コマンドなどのモデル化は苦しくて、小細工が必要です。小細工の例は「整数スタックの例」のpush(n)を参照してください。
そういう事情で、一般化オートマトンはプログラムのモデルとしては不十分ですが、その分、取り扱いやすい面が多々あります。簡単なモデルからも有用な情報・知見を得ることが出来るのです。
指標グラフに関する言葉
言葉の対訳表を示します。簡単な説明は表内にありますが、補足的な説明は表の後に書きます。
| モノ | グラフ理論 | 形式的プログラム構文論 | 説明 |
|---|---|---|---|
| Φ | （有向）グラフ | 構文構成素の集合 | インターフェイス定義 |
| |Φ|の要素 | 頂点 | ソート記号 | 型の名前 |
| Φ(x, y)の要素 | 辺 | オペレーション記号 | 手続きの名前 |
指標グラフΦは、プログラムの構文を決めるものです。構文は、使える型の名前と手続きの名前を提示すれば決まります。「手続き」という言葉は、「関数、メソッド、命令（インストラクション）、サブルーチン、アクション」などと呼ばれている概念を総称的に表すために使います。
次の表のなかで、Φの隠蔽頂点の集合をHidとします。Hid = |Φ|＼(S∪D) です。
| モノ | グラフ理論 | 隠蔽代数の理論など | 説明 |
|---|---|---|---|
| S∪D の要素 | 可視頂点 | 可視ソート記号 | 組み込みの値型の名前 |
| Hid の要素 | 隠蔽頂点 | 隠蔽ソート記号 | ユーザー定義オブジェクト型の名前 |
| x, y∈(S∪D) として Φ(x, y)の要素 | 可視辺 | 可視オペレーション記号 | 組み込み関数の名前 |
組み込みの値型（value type）とは、整数型や真偽値型のことです。文字列型も、イミュータブルなら値型と考えていいでしょう。ユーザー定義せずとも始めから使える型／手続きの名前が可視ソート記号／可視オペレーション記号で、グラフ上では可視頂点／可視辺と呼ぶのです。
次の表を理解するには、メイヤー先生の「Command-Query分離の原則」が必要です。「メイヤー先生の偉大さとCommand-Query分離」を参照してください。
| モノ | 説明 |
|---|---|
| s∈S, x∈Hid として Φ(s, x)の要素 | コンストラクタの名前 |
| Sの要素 | コンストラクタの引数となる型の名前 |
| d∈D, x∈Hid として Φ(x, d)の要素 | クエリーの名前 |
| Dの要素 | クエリーの値となる型の名前 |
| x, y∈Hid として Φ(x, y)の要素 | コマンドの名前 |
| x∈Hid として Φ(x, x)の要素 | 遷移コマンドの名前 |
| x, y∈Hid, x≠y として Φ(x, y)の要素 | 変容コマンドの名前 |
S, Dなどの頂点の部分集合を導入するのは、コマンドとクエリーを区別する手段としてです。他に、伝統的オートマトンの始状態と終状態を真似るため、という動機もあります。
コマンド（の名前）は、さらに遷移コマンド（transition command）と変容コマンド（mutation command）に分けています。遷移コマンドは同一の状態空間内の移動で、異なる状態空間に飛び移るのが変容コマンドです。遷移コマンドは、圏では自己射（endomorphism）になります。
指標圏に関する言葉
以下、C = FreeCat(Φ) であると仮定して、Cは指標圏（signature category）と呼びます。
| モノ | グラフ理論 | 圏論 | 説明 |
|---|---|---|---|
| Φ | グラフ | 自由圏の生成系 | インターフェイス定義 |
| C | 全てのパスの集合 | 自由圏 | 全てのプログラムコードの集合 |
| |Φ| = |C| の要素 | 頂点 | 対象 | 型の名前 |
| C(x, y) の要素 | パス | 射 | プログラムコード |
| f;g | パスの連接 | 射の結合（合成） | プログラムコードの順次結合 |
指標グラフΦにより、型と基本手続き（primitive procedure）の名前が提示されます。頂点が型の名前、辺が基本手続きの名前でした。Φから作られた自由圏Cは、基本手続きをもとに作られた全てのプログラムコードを表現します。基本手続きを複合する方法は順次結合（sequential composition）だけです。
指標Φが次のような形をしているとき、それは伝統的オートマトンの指標です。
この特殊な状況では、次の言葉を使います。
| モノ | ラベル付き遷移系 | オートマトン | 説明 |
|---|---|---|---|
| Γ = Φ(1, 1) | ラベル集合 | アルファベット | 遷移コマンド名の集合 |
| Φ(1, 1) の要素 | ラベル | 字（letter）、語 | 遷移コマンド名 |
| C(1, 1) の要素 | ラベル列 | 語、文 | プログラムコード |
| id1 | 空列 | 空語、空文 | 空プログラムコード |
隠蔽頂点（隠蔽ソート）がただ1つしかない場合がラベル付き遷移系や伝統的オートマトンです。プログラムにおけるクラスのインターフェイスでは、唯一の隠蔽ソート（図では頂点1）がthisやselfとなります。[追記]thisやselfは型の名前そのものというより、変数のように使われるので、正確には「thisやselfが走る領域に付ける名前・番号」とか言うべきでした。[/追記]
関手に関する言葉
指標グラフΦと指標圏Cは、プログラムの構文を定義します。プログラムの意味を定義するのが関手 F:C→ Set です。プログラムの意味は実装（implementation）と呼んでもいいでしょう。
| モノ | 説明 |
|---|---|
| F:Φ→Set | インターフェイスΦの実装 |
| K:Φvis→Set | 組み込み部分の事前実装 |
| x∈(S∪D) として F(x) | 型xの値空間 |
| y∈Hid として F(y) | 型yの状態空間 |
| a∈Φvis(x, y) として K(a) = F(a) | 組み込み関数aの表示的意味 |
| b∈Φ(x, y) として F(b) | 基本手続きbの表示的意味 |
| f∈C として F(f) | プログラムfの表示的意味 |
x∈|Φ| は型の名前で、F(x)∈|Set| が実際の型（データ領域）となる集合です。ここでは、「型の意味は集合（Sets-as-Types）」という素朴な立場をとっています。x∈Hid とは、名前xがオブジェクトの型（クラス）を表すことです。そのときのF(x)は、オブジェクト状態の集合なので状態空間（state space）と呼ぶのです。一方、組み込み型の値の集合は値空間（value space）です。
f:x→y in C は、単なるプログラムコードであり、構文的な存在です。x, y も単なる名前と考えます。それに対して、F(f):F(x)→F(y) は集合のあいだの写像です。集合と写像に対して、プログラム的なニュアンスを付けるために次のような呼び名で区別するのです。
- 値空間
- 状態空間
- 値空間のあいだの組み込み関数
- ユーザー定義のコンストラクタ
- ユーザー定義のクエリー・メソッド
- ユーザー定義のコマンド・メソッド（遷移と変容）
集合と写像は何の色も付いてない味気ないものです。無味無臭の集合／写像に、プログラミング上の役割を（間接的に）付与する手段が、開始頂点族Sと識別頂点族Dだったのです。
上記の対訳表により、関手オートマトンを構成している Φ, S, D, K, F の現実的な対応物が了解できると思います。この対応（翻訳）を適用すれば、抽象的な構成や言明から、現実的な意味を汲み取ることができるでしょう。
実は、ここに書かなかった“論理との対応”もあります。クエリー名が述語記号に対応し、引数なしコンストラクタ名は定数記号に対応します。関手Fは、個体項や論理式の意味論（＝モデル）です。論理もまた異なる文化圏なので、まったく違った言葉が使用されます。同じ内実に対して、言葉だけがどうしてこうも大量にあるのか!? と溜め息が出ますが、まー、言ってもしょうがない。
- 関連する愚痴： 感動か効率性か
