System F System Fの概要

ウィキペディア

System F

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/09/07 02:10 UTC 版)

単純型付きラムダ計算では，関数についての変数とその束縛が存在するが，System Fでは型についての変数とその束縛が追加されている．例えば恒等関数は任意の型$A$について$A\to A$の形の型を持ちうるが，System Fではこのことが次の判断が成り立つことによって表されている:

$\vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha$.

ここで，$\alpha$は型変数である．また，小文字の$\lambda$が通常の値レベルの抽象を表しているのに対して，大文字の$\Lambda$を型レベルの抽象を表すために使用している．

項書換え系として見ると，System Fは強正規化性を持つ．しかしながらSystem Fにおける型推論は決定不能である．またSystem Fはカリー＝ハワード同型の下で，全称量化のみを用いる2階直観主義論理の断片に対応する．System Fは依存型などを含んだより強力なラムダ計算とともに，ラムダ・キューブの一角であるとみなすこともできる．