X-オートマトン

昨日、読み書き機械という概念を導入したが、集合（つうか圏の対象）Xに対してX-オートマトンという概念／用語のほうがいいと思い直した。

(S, X, O, A)がX-オートマトン（背景の圏はSet）だとは、

1. Sは状態の集合
2. Xは観測値の集合
3. Oは観測子（属性）の集合、f∈O なら、f:S→X
4. Aはアクション（遷移）の集合、a∈A なら、a:S→S

メイヤーが言うクエリ＆コマンド方式の、クエリの値をXに限定したもの。背景の圏を変えると、部分性や非決定性も表せる。

一般には、圏Cと、X∈|C|を含む指標Σに対して、Autom(C, Σ)が定義できる。指標Σ内のソート記号xが前もってXにバインドされている状況。Autom(C, Σ(X)) = Autom_Σ(C, X) のようにも書ける。Σが自明ならAutom(C, X)、さらにCも暗黙に固定（例えばSet）するならAutom(X)。

メモリ空間M = (A, E, X)があると、Σ(M) = (O(M), A(M))を次のように定義できる。

• O(M) = {read(i):s→X | 0 ≦ i ＜ size(M)}
• A(M) = {write(i, x):s→s | 0 ≦ i ＜ size(M), x∈X}

このΣ(M)とState(M)があれば、Autom(M)が構成できる。

背景となる圏を（例えばSetに）固定して、X-Automの圏とY-Automの圏の関手を定義すべきだし、X-Autom = Autom[X] としてindexed categoryにすべき。うーむ、やっぱりそういうことになるのか。