そうか、自発性（非因果性）はε遷移で記述できるか。εを空語のみからなる言語だとして、 when (R) sending{ε} changes you(R') causes your{E}. 「私は何もしてないのに、あんたが勝手に変わったんでしょう。」「それが悪いか？」

Cond+(Σ) = Form(Obs(Σ+))（内部条件；直接制御可能）、Cond-(Σ) = Form(Obs(Σ-))（外部条件；直接制御不可能、コマンド経由）だとする。P∈Cond(Σ), Q∈Cond+(Σ), R∈Cond-(Σ), F∈Cmd(Σ), E∈Evt(Σ)に対して、次の形を持つ。メッセージは中括弧にする。 when(P)…

“クアドラプル”は言いにくいから、対話（的）ホーア式にする。極性付きでアメナブルな多ソートprefixed隠蔽指標を対話（的）指標と呼ぶことにする。Σがアメナブルなとき、Obs(Σ)は観測子（observer）の集合、Mut(Σ)が変更子（mutator）の集合。対話指標ΣはΣ=…