古い土地

コンピュータサイエンスの勉強をしていると、どこかの段階で型・圏・論理のトライアングル（Computional Trilogy）にぶつかる。すなわち、 カリー＝ハワード同型対応によって、型付きラムダ計算（プログラム）と直観主義論理（証明）が対応する 圏論的論理学は論理学をトポスという圏で書き直し、「論理 → 圏」（モデル論…