System F塔
二階多相λ計算で型抽象を積み上げるパズル
背景： System F (Girard 1972 / Reynolds 1974) は 型抽象
例: 多相恒等関数
Λα. e と 型適用 e [τ] を持つ二階多相λ。Curry-Howard対応で二階直観論理に対応。例: 多相恒等関数
id = Λα. λx:α. x に id [Int] 7 と適用すると β-簡約で (λx:Int. x) 7 → 7。型もλ抽象の対象になる。
STAGE: 1/5
項: id
目標: --
簡約数: 0
最良: --
操作
パレットでパーツを選択 → キャンバスをクリックして縦に積む。下から順に評価される (内側から)。
APPLY (Enter) 一番外側の簡約を実行 (β: (λx.e) v → e[v/x], β-Type: (Λα.e) [τ] → e[τ/α], η)
UNDO 1手戻す RESET 最初から
勝利条件: 最終塔の式が「目標型/値」と完全一致するまで簡約。
Y Lab tieup: Girard-Reynoldsの多相λ計算。Curry-Howard 対応で 二階論理 に対応する型理論。横山研で扱う型システムの基礎中の基礎。