観測可能論理と隠蔽論理

ゴグエン／マルコルム／ケンプ（Joseph Goguen, Grant Malcolm, Tom Kemp）の"A Hidden Herbrand Theorem"(1998)とビドォイト／ヘンニッカー／カーツ（Bidoit/Hennicker/Kurz）の"On Observability and Reachability "を読み比べてみた。

Observational Logic Inst.	Hidden Logic Inst.
S : all sorts	S : all sorts
SObs : observable sorts	V : visible sorts
SNonObs : non observable sorts	H : hidden sorts
SNonObs = S＼SObs	H = S＼V
-	Ψ : visible operators
-	ΨはVによる誘導部分指標
-	op:s1, ..., sn→sで、si∈Hとなるiは高々1つ
observer (op, i)	-
s1, ..., sn→s、si∈SNonObs	s1, ..., sn→s、si∈H
s1, ..., sn→s、si∈SNonObs	s1, ..., sn→s、si∈H
s∈SObsなら direct observer	s∈V ならばattribute
s∈SNonObsなら indirect observer	s∈H ならばmethod
モデルはobservational algebras	モデルはhidden algebras

hiddenでは、可視ソートをimportすることを前提としており、ΨはΣ内で一切変更できない。また、Ψのモデルはデータ（値の）代数とも呼ばれ、固定して話を進めている。すべのて演算は、可視演算（固定されている）、メソッド、属性のどれかに分類される。

一方のobservationalでは、可視ソートに相当する概念（観測可能ソート）があるが、特にΨのような部分指標を特定してなく、指標の階層化（相対化）はされていない。すべのて演算は、観測演算とそれ以外に分類される。観測演算は直接と間接に分類される。直接観測演算＝属性、間接観測演算＝メソッドであるが、その他の演算が可視演算に相当するとは限らない。単に、観測演算に注目するだけのこと。

現実的には、(1)観測演算（ミューテータを含む、テストをする必要があるもの）、(2)基本演算（値の計算、可視演算と同じ）、(3)便宜演算に分けるといいと思う。便宜演算はなくてもいいがあれば便利、短くて簡単な実装。

ところで、隠蔽指標の射は定義されていたが観測可能指標の射の定義がなかった、探そう。
あった、http://citeseer.ist.psu.edu/hennicker98observational.html より：

Definition 5.1 (Observational signature morphism)

Let Σ_Obs = (Σ, S_Obs, OP_Obs) and Σ’_Obs = (Σ’, S’_Obs, OP’_Obs) be two observational signatures with Σ = (S, OP) and Σ’= (S’, OP’). An observational signature morphism σ_Obs: Σ_Obs → Σ’_Obs is a signature morphism σ: Σ → Σ’ such that the following conditions are satisfied:

(1) σ(S_Obs) = σ(S) ∩ S’_Obs.
(2) If (op, i) ∈ OP_Obs then (σ(op), i) ∈ OP’_Obs,
(3) If (op’, i) ∈ OP’_Obs such that op’: s1’,…,sn’ → s’ and si’∈ σ(S) then there exists op ∈ OP such that (op, i) ∈ OP_Obs and op’ = σ(op).