System F

System F（システム・エフ）は、型付きラムダ計算の一体系であり、単純型付きラムダ計算に、型についての全称量化を取り入れた計算機構である。二階ラムダ計算、ポリモーフィックラムダ計算とも言われる。プログラミング言語でのパラメトリック多相を形式化するもので、関数型言語のMLやHaskellなどの型システムのベース理論にされている。System Fは、論理学者のジャン＝イヴ・ジラールと計算機科学者のジョン・C・レイノルズの両者が別個に発見している。ジラールによるとSystem Fの語源は、たまたまそう名付けただけと言う。

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

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

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

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

参考文献

• テンプレート:Cite conference
• テンプレート:Cite conference
• テンプレート:Cite book
• テンプレート:Cite conference

関連項目

• F Sharp