ホーア4つ組の定式化

ホーア4つ組の定義らしきもの。やっと、しかし、まだ詰めが甘い。

Sは状態空間、Aが入力記号の集合で、指標Σのミューテータ記号で与えられる。Bは出力記号の集合で、指標Γのミューテータ記号で与えられる。A*（Aの列）をコマンド、B*（Bの列）をイベントと呼ぶこともある。

A*×S → Pow(S×B*) を遷移とする。α∈A*に対してS→Pow(S×B*)が決まる。これを、【α】とかく。p, qなどはS上の述語だとする。EがBの正規表現だとして、組(q, E)は、【q】×【E】∈Pow(S×B*)という解釈をする。【q】⊆S、【E】⊆B*（正規言語）である。

4つ組 p→[α]q, E の意味は、【p】⊆【α】^-1(【q】×【E】) だとする。【α】^-1は、ブール代数Pow(S×B*)からPow(S)への様相オペレータとなっている。4つ組の解釈はPow(S)内で行える。

α∈A* と x∈Sが与えられたとき、「x∈【p】ならば【α】(s)∈【q】×【E】」のとき、ホーア4つ組'p→[α]q, E'を満たしている。

A*×S → Pow(S×B*) はCirc-Kleisli構成を一般化して、とある圏のA→Bという射と考えることができるだろう。またこれは、S|→[A*, Pow(S×B*)]という関手の余代数にもなっている。