読み書き機械の指標とモデル

やっぱり読み書き機械だけでもいいのかもな。んんと、こういうことか。

集合Xと非負整数nが与えられると、指標Σ(X, n)が作れる。

• read(i):s→X (i = 0, ..., n-1)
• write(i, x):s→s (i = 0, ..., n-1、x∈X)

ここで自由なソート記号sに集合を対応させ、オペレータ記号に写像を対応させれば、指標Σ(X, n)のモデルとなる。セオリーとしては：

1. (true){write(i, x)}(read(i) == x}
2. (read(j) == y ∧i ≠ j){write(i, x)}(read(j) == y}

でいいと思う。このセオリーも一緒に考えるとして、そのモデル圏をRWM(X, n)とすればいいかな。

メモリー空間A = (A, E, X)があると、size(M) = size(E) = n として、対(X, n)が決まるから、RWM(M) = RWM(X, n) と定義できる。空のメモリ空間を許しても、RWM(M)は単元集合を状態空間として、（妥当な）観測子もアクションもまったくない機械になる。