単純型付きラムダ

ラムダ計算のセミナーをやるので、[セミナー]タグでネタを記録することにする。

青いProof Theoryの本とは、A. S. Troelstra, H. Schwichtenberg "Basic Proof Theory Second Edition"、著者の読み方（カタカナ表記）はトゥロエルストラ、シュウイッテンブルクかなー？？？ アブラムスキーやアクゼルもエディターになっているケンブリッヂのシリーズ物の一冊。このシリーズの執筆陣の豪華なこと豪華なこと… と、それはまーいいとして。

• 3.6 (P.85)に片側シーケントの古典論理が書いてある。ここだと、Gentzen-Shutte（ゲンツェン／シュッテ）になっている。ん？ ゲンツェン／テイトじゃなかった？
• 8章（p.258）は categorical logic
• 9章（p.283）は様相論理と線形論理

全体にモダンで洗練されている。証明論の本だから当たり前のことだが、モデル論がない。そこがなんかもの足りないね（←別な本読めよ＞自分）。

この本から、simply typed lambdaの項の定義、いつでも肩に型（駄洒落じゃない）を付ける流儀：

1. 型付き変数 x^A, y^Bなど。
2. t^A→B, s^Aに対して、App(t^A→B, s^A)^B
3. t^B, x^Aに対して、(λx^A.t^B)^A→B

これから略記を導入する。非常にスッキリ。

同書p.38から、∧と⊃だけの推論：

1. ∧の導入規則
2. A∧B からのAだけ、Bだけを選ぶ消去規則
3. A⊃Bを導入する含意導入規則、ただしAにはラベルを付ける
4. モダスポネンス

この本には書いてないが、構造規則として、換（Exchange）と増（thinning, copy, dup）は入れていいだろう。推論規則のアリティを記しておくと：

1. 換 2→2
2. 増 1→2
3. ∧導入 2→1
4. 射影 1→1
5. 含意導入 1→1 ただし、横から入るループが作られる。
6. モダスポネンス 2→1