落書きしてみた。Hoareのなんか（って何だよ） 圏論ってタグつけるほどのもんじゃないけど…も少し書くと、これはモデルの抽象化の話を可換図式で書いてみたもの。Sがモデルの状態、αが抽象化。 具体的な世界で成り立つ論理式の帰結は、抽象化した世界での論…