マイヒル／ネロードの定理
箇条書きでザッと。
- マイヒル／ネロード（Myhill/Nerode）の定理は、Constructor-Command-Query分離した指標に対するモデルの構造定理である。
- Xを状態空間、適当な圏のホムセットを考えて、コンストラクタ（の意味）は Hom(1, X)、コマンドの意味は Hom(X, X)、クエリーの意味は Hom(X, V) となる。1はシングルトンセットでVはクエリーの値の集合。
- 可達かつ可識なモデルを考える。
- 可達性は、状態を事前に調整可能であることを意味する。ゴミの状態がない。
- 可識性は、状態を実験と観測で同定できることを意味する。異なるが識別できない二状態がない。
- 可達かつ可識なモデルは、無駄がないモデル。
- 可達かつ可識なモデルは、構文的に再構成可能である。これがマイヒル／ネロードの定理。
- さらに、構文的で標準的なモデルの具体的構成法を与える。
- 構文的で標準的なモデルは、リンデンバウム、エルブラン、タルスキーの伝統。
- 与えられた指標に関して、可達かつ可識なモデルの圏において、構文的標準モデルは稠密な部分圏となる。よって、構造的には、構文的標準モデルを調べれば十分である。
- すでにあるモデル（実装）と構文的標準モデルを比べるとリファクタリングができるかも。ゴミ＝無駄を特定できるので。
ネロード同値とは、不可識（indistinguishable、distinguishableの否定）な2つの状態を同値とする同値関係である。ネロード同値関係で商を作ることはある種の正規化になる。ネロード同値が最初から等値になっているなら、それは正規なモデルである。ネロードの正規化は、状態空間を最小化するので、ネロード最小化とも呼ぶ。これは関手性を持つので、ネロード最小化（正規化）関手が存在する。
ネロード同値とネロード最小化の発想は、ライプニッツの不可識別者同一（不可弁別即同一）の原理（principle of the identity of indiscernibles）と同じ。可達性も同じようなもので、次のようにまとめられる。
- 観測できないものは存在しない。
- 区別できないものは同じ。
圏をモデルにするような指標を圏指標と呼ぶ。圏指標のモデルは当然に圏だが、圏に可達性と可識性を定義する。
- Iに入る射がidIしかないとき、スターティング対象（またはソース、ルート）と呼ぶ。
- Vから出る射がidVしかないとき、エンディング対象（またはシンク、リーフ）と呼ぶ。
- スターティング対象Iから出る射をポイントと呼ぶ。
- エンディング対象Vに入る射をクエリーと呼ぶ。
圏の指標Σがあって、
- 任意のポイントがΣの項で表現可能なら、そのΣモデルは可達。
- 任意の射の同一性が、Σのクエリー項に対する等式で表現可能なら、そのΣモデルは可識。
これが意味を持つには、おそらく次が前提だろう。
- 任意の射f, gの同一性が、ポイントpに対する p;f = p;g で判断可能。
この状況で、指標Σの可達可識なモデルに関するマイヒル／ネロードの定理が成立するはず。
