S4 and strong monad

PPL で話題に上った classical S4 の ◇ と strong monad について、今更ながらふと思い出したので書いてみます。

疑問

確か、S4 の ◇ を「ある時刻に計算可能」と解釈すると Haskell の monad みたいに見えるけど strong monad ではないのでなんか違う、じゃあ何なのかというとよくわからない、という話だったと記憶しています。classical S4 に strength を足すと様相がつぶれて (x R y iff x = y) ただの古典論理になるのでした。

ところで普通の strong monad は直観主義様相論理である lax logic の lax modality として解釈されます。lax logic は intuitionistic S4 + α みたいなもので strength が成り立つのですが、直観主義であるため様相を完全にはつぶすことなく (if x R y then x <= y) それを実現しています。*1

思い出したこと

そして、この lax logic から IS4 への埋め込みが知られていて、実は lax logic の strength は IS4 の L-strength に対応するのでした。

• strength: ◇A ∧ B → ◇(A ∧ B)
• L-strength: ◇A ∧ □B → ◇(A ∧ □B)

それは何を意味するんだろうとか

たぶん strength が成り立ってほしい気持ちは、「まず B を計算する。その結果を覚えておく。将来 A が計算可能になったら、そっちも計算する。結果がわかったら覚えておいて結果と対にして返す」ということができそうだから。ここでのポイントは「結果を覚えておく」ではないかと。要するに、結果が一度わかったらそれを参照することはいつでもできるという仮定があります。

そこで □ は「いつでも計算可能」と解釈できることを思い出します。どうやら B には □ がついていると理解したらよさそうだと思えないでしょうか。そう思うことにすると、上の手順はただの strength ではなく L-strength の説明になっていると考えられます。

で。問題の古典の場合にはあと何を考えればいいんだろう。古典論理苦手。

参考文献

詳細を知りたい場合は、たぶん S. Kobayashi "Monad as modality" とか N. Alechina et al. "Categorical and Kripke semantics for constructive S4 modal logic" とかを見れば関連しそうなことが書いてあるんじゃないでしょうか。前者が L-strength の初出だったかと。

*1:非自明なのは可能様相だけ。必然様相はつぶれます