シーケント計算のPow意味論
昨日の話の続き。モノイド圏に意味を持つシーケント計算は、あたりまえだがモノイド圏に意味を持つ。特に、集合直和を圏論的直積＝デカルト・モノイド積とする関係圏で解釈すると具合がいい。だが、ここではあえて集合圏（実際は順序も入るが）を使ってみる。
シーケント計算の論理としては、論理結合子が1つしかないコンパクト論理。否定も含意もない。含意がないからモダスポネンスもないという、ひどく原始的な論理だ。「そんなもん論理じゃねー」 -- ごもっとも。
それでもなお、無理クリにでも命題論理の計算だと思うのだ。基本記号A, Bなどには集合【A】, 【B】などが前もって割り当てられているとする。めんどうなので、【A】, 【B】などを単にA, Bと書く。あるいは、最初からA, Bなどは集合だと思ってもよい。論理式は、基本記号、論理定数I、論理結合子∧、括弧で組み立てた形（構文木）。論理式の意味は：
- 【A】 = 【A】 （Aは基本記号）
- 【I】 = φ（空集合）
- 【α∧β】 = 【α】+【β】（直和）
以下、必ずしも基本記号ではない論理式もA, Bなどと書く。
論理式の列 A1, ..., An の意味は、Pow(【A1】)× ...×Pow(【An】) だとする。特に空列εに対しては、Pow(φ) = {φ} = 1 とする。と、こうすると、シーケントの左も右も順序集合になる。そして、シーケント自体には順序の意味で連続な写像を対応させる。
ミソは、Pow(【α∧β】) = Pow(【α】+【β】) = Pow(【α】)×Pow(【β】) となること。まさにPowは指数関数なので、足し算と掛け算が入れ替わってくれる -- これだけのことだが、とてもありがたい！
この状況を外から眺めてみる； Powを取ると、順序が入るので、【A】* = Pow(【A】) として定義された【-】*は、シーケント計算の順序圏Ordによる意味論となる。実際の議論に必要な性質は、最小限⊥を持つこと（従って非空）、ω完備であることくらいだ。ようするに、ωCPOだ。
シーケント計算のωCPOでの意味論が構成可能だということは、RelからωCPOへの関手があることを示唆する。実際、Powがその関手となる。この関手によって、Rel側のトレースや不動点オペレータがどう写るか、ωCPO側のカリー化などがRelとどう関係するのか、などを調べられる。
