多段階計算における継続

最近，古典論理に対応する計算体系について勉強してます。

古典論理だと Peirce's law と call/cc が対応するとかいう話がわりと有名で，基本的にはコントロールオペレータを含む体系になります。それで，そこにさらに様相が入った場合にはどんなことになるのだろうかということが気になっています。

様相の一つの解釈として，多段階計算におけるコード片の型を様相型で表すというものがあります。これはもともと直観主義の上でやってた話ですが，その解釈を古典様相論理でできないかと考えてみました。そうすると，いくつか引っかかるところが出てきます。

古典に対応する体系だと，継続がわりとそこらじゅうに出てくる感じになるようですが，そもそも多段階計算における継続とは何なのかということがそんなに明らかではないような気がします。

一番それらしく思われる定義は，継続とは「今の段階における残りの計算」である，というものです。しかし(正規)古典様相論理においては ◇⊥→⊥ が成立するので，これだと ◇ を，様相論理の直感からすると自然な解釈である「ある段階で使えるコード片の型」とは考えにくくなりそうです。もっとも，◇ をそのように解釈しないで ¬□¬ だと思ってしまえばよいといえばよいのですが。

もう一つの可能性は，継続を「今以降のすべての段階における残りの計算」と考えることで，こうすると ◇⊥→⊥ が成立してもおかしくないようには思われます。ただ，継続をそのように解釈するのが適切かというと，怪しい気がします。そのような「継続」は必然的に計算の段階を跨いで何かすることになりますが，それは段階計算の直感に反するように思われるのです。段階の間を移動するという現象は，言語の枠組みの外にある超越的なところで行われるものなんじゃないか，というような気がするからです。

ちなみに古典様相論理に対応する計算体系についてはいくつか考えられてます。例えば Distributed Control Flow with Classical Modal Logic, A Computational Interpretation of Classical S4 Modal Logic, Classical Natural Deduction for S4 Modal Logic など。他にもありそう。上に書いた話は三つ目の論文といくらか重複してます。