対話ホーア式

“クアドラプル”は言いにくいから、対話（的）ホーア式にする。

極性付きでアメナブルな多ソートprefixed隠蔽指標を対話（的）指標と呼ぶことにする。Σがアメナブルなとき、Obs(Σ)は観測子（observer）の集合、Mut(Σ)が変更子（mutator）の集合。対話指標ΣはΣ=(Σ⁺, Σ^-)。

Obs(Σ⁺) + Obs(Σ^-)から作られる（適当な論理の）formulaの全体Form(Obs(Σ⁺) + Obs(Σ^-))をCond(Σ)（条件）とする。Mut(Σ⁺)から作られた言語（メッセージ集合）の集合をCmd(Σ)（コマンド）、Mut(Σ^-)から作られた言語の集合をEvt(Σ)（イベント）とする。実際には、CmdとEvtは言語を表現する式の集まりだと思ってよい。

対話ホーア式は、P, Q∈Cond(Σ)とF∈Cmd(Σ), E∈Evt(Σ)に対して、次の形を持つ。

• when(P) sending(F) results(Q) causes(E).
• when(P) receiving(E) results(Q) motivates(F).

ただし、条件をForm(Obs(Σ⁺) + Obs(Σ^-))としていいかどうかは非常に問題。因果性と自発性がからんでくる。対話の相方が自発的発展をするとき、自分の状態空間（因果的）と相手の状態空間（非因果的、自発的）を一緒にすることは、たぶんダメだろう。もっと詳細な議論が要る。