右カン拡張もラムダ計算の仲間らしいので、カリー／ハワード・スタイルの対応がありますね。表にします。
| 連言・含意の論理 | 型付きラムダ計算 | 右カン拡張 |
|---|---|---|
| 命題 P, Q | 集合 A, B | 関手 F, G |
| 帰結関係 P |- Q | 写像 f:A→B | 自然変換 α::F⇒G |
| 連言 P∧Q | 直積 A×B | 結合 F;G |
| 含意 P⊃Q | 写像集合 BA | 右カン拡張 FG |
| 演繹定理 | カリー双射対応 | カン双射対応 |
| 含意導入 | ラムダ抽象 | 自然変換のシフト |
| モーダスポネンス | 適用／評価 | 自然変換のアンシフト |
| 推論／証明 | 写像の計算 | 自然変換の計算 |
| 証明図 | 計算図 | ストリング図 |
自然変換の「シフト（shift）」という言葉は次の論文で使われていた用語です。
- Ralf Hinze, "Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick." http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
「アンシフト」はシフトの逆として、僕が勝手に使っているだけです。
