最近、メイヤー代数／メイヤーオートマトンの話をしました。（メイヤーオートマトンとメイヤー加群は同義語です。）
メイヤー代数／メイヤーオートマトンの概念は最近考えたわけではないのですが、概念に呼び名がなかったので語りようがない状況でした。
メイヤー先生が提唱する「Command-Query分離された状態遷移系」の代数的な定式化はだいぶ以前から考えていたのですが、なんと呼べばいいかウジウジと悩んでいました。思い切って（勝手ながら）メイヤー代数と呼ぶことにしました（「メイヤー代数、メイヤー指標、メイヤーオートマトン」）。これで話がしやすくなりました。名前がないモノについて語るのは困難（ときに不可能）ですからね。
2010年に「ストレージの線形代数： 泥臭いデータ操作の洗練された定式化」は書いてますが、これは更新操作、つまりCommandだけを扱いQueryは入ってません。CommandとQueryの両方を扱うと、メイヤー代数やメイヤーオートマトン（メイヤー加群）になります。
メイヤーオートマトンの大きなメリット・魅力は、マイヒル／ネロード（Myhill-Nerode）の定理が成立することです。この定理の記述と証明は難しくないですが、先に、どんなありがたみがあるかを宣伝しておきます。
マイヒル／ネロードの定理とはどんなもの？
メイヤーオートマトンは、特定のインターフェース（あるいはプロトコル）を持った操作可能オブジェクトのモデルです。インターフェースは、Command記号の集まりとQuery記号の集まりに分離されています -- これがミソ! メイヤーの原則です。
特定のインターフェースを持つメイヤーオートマトンの全体を考えて、「アプリケーションプログラムから見て区別が付かない」という同値関係で分類します。この同値関係は、ある種のリスコフ置換可能性（Liskov substitutability）です。あるメイヤーオートマトンを、それと同値な別のメイヤーオートマトンと入れ替えてもアプリケーションプログラマはそれに気づくことができず、また、何の不都合も起きません。
マイヒル／ネロードの定理は、この「区別がつかない」という同値関係の各同値類に対して、唯一つの標準的なメイヤーオートマトンを構成可能であることを主張します。具体的な構成法も与えます。標準的なメイヤーオートマトンは最小（minimum）な正規形（normal form）なので、MN（エムエヌ）オートマトンと言っていいでしょう。具合がいいことに、MNはMyhill-Nerodeの頭文字と一致します :-)
おそらくこれは、余代数の圏の終対象に関する定理なのでしょうが、そこまで言わなくても十分に一般性があり守備範囲は広く、具体的でハッキリとした構成法を持ちます。
正規言語に関するマイヒル／ネロードの定理との関係
マイヒル／ネロードの定理は、もともと正規言語を特徴付ける定理です。ある正規言語を受理するオートマトンのなかで、状態数が最小のものが（標準的に）存在することがわかります。メイヤーオートマトンに関するマイヒル／ネロードの定理は、正規言語に関するそれの直接的な拡張です。
有限オートマトンよりはるかに広いクラスのオートマトン（ラベル付き状態遷移系）に適用でき、オリジナルのマイヒル／ネロードの定理を特殊なケースとして含みます。一般化されているにも関わらず、定式化や証明の過程は、オリジナルより具体的で分かりやすいと思います。
なぜ「具体的で分かりやすい」かと言うと、メイヤーオートマトンに関するマイヒル／ネロードの定理は、インターフェースと実装とテストの関係について述べていると解釈できるからです。メイヤーオートマトンは、Command-Query分離されたインターフェース（メイヤー指標）の実装ですが、「アプリケーションプログラムから見て区別が付かない」とは、どんなに頑張ってテストしても挙動の食い違いを発見できない、ことです。
どんなに頑張ってテストしても挙動の食い違いを発見できないなら、それは異なる実装と考える必要はなくて、（事実はどうあれ）「同じ実装」とみなして差し支えありません。この「同じ」という概念がリスコフ置換可能性としての同値関係です。頑張って作ったテストの集合は、究極的には（同値関係の意味で）単一の実装を完全に特徴付けてしまうはずです。これが、メイヤーオートマトンに関するマイヒル／ネロードの定理の主張です。
マイヒル／ネロードの定理のご利益は
メイヤーオートマトンに関するマイヒル／ネロードの定理は、仕様記述、モジュール／クラス設計、リファクタリング、テストなどに色々と知見と示唆を与えてくれます。
例えば、仕様記述には、メイヤーの契約とかホーアトリプルとホーア論理などを用いるでしょうが、単純な等式的論理も有用なことがわかります。仕様記述とテストは区別すべきではない、と僕は考えていますが、その立場でエクスペクテーションベースのテストを眺めると、テストにより等式的論理の原子基礎論理式を積み重ねていることがわかります。このような見方・考え方は、テスト容易性／テスト困難性が何に起因するかを教えてくれます。テストが困難な状況を緩和するにはどうすべきかの方針も与えてくれます。
また、次のような問や疑問にある程度は答えることが可能となります。
- 「仕様は実装です」って主張に意味があるのか？ 合理化できるのか？
- 仕様に対する参照実装って役に立つのか？
- テストは多いほど良いのか？
- 仕様の詳細化ってなに？
- 仕様の互換性、実装の互換性に正確で実証可能な定義を与えられるのか？
- 仕様とテストにより*1、実装の挙動を完全に制約できるか？
*1:「仕様記述とテストは区別すべきではない」なら、この言い回しは冗長ですけどね。
