指標が極性付きでΣ=Σ++Σ-でも、指標Σ上の制約やセオリーが、Σ+上の制約とΣ-上の制約に直和分解できるわけじゃない。そうじゃなくて、Sen(Σ++Σ-)のなかで考えることになる。これはコンポネント（双方向）のコンパクト閉圏が、単方向であるトレース付きモノイ…

πPインスティチューションからあらためて見て、“既に動いている実装の正しさ”と“プログラムソースコードの正しさ”は別な概念だな。実装が正しいとは仕様に対する充足性の問題で、たぶんvalidというのだろう。一方プログラムの正しさは、メイヤーの契約のよう…

インスティチューションがあって、Σ∈|Sign|ごとに、証明可能性“|-”が付いているとする。A⊆Sen(Σ)、b∈Sen(Σ)に対して、A|-b は、Aを仮定してbが証明できること。|-を拡張して、A|-Bが定義できる。「A|-B ならば A|⇒B」が健全性。ここで、A|⇒B は、BがAの帰結…

メモ編ネタがあるときは本編ネタがなくなる。まー、そういうもんだな。メモ編ネタ： Programming in the Hugeをやりたい。 仕様証明とプログラム証明は別物だ。ちゃんと区別。仕様証明はπインスティチューションの概念、プログラム証明はπPインスティチュー…