System F

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

System F型付きラムダ計算の一体系で,単純型付きラムダ計算についての全称量化を導入したものである.2階ラムダ計算(ジラール–レイノルズ)多相ラムダ計算としても知られる.プログラミング言語におけるパラメータ多相を形式化するもので,MLHaskellのような関数型言語の論理的な背景となっている.System Fは論理学者ジャン=イヴ・ジラールおよび計算機科学者ジョン・C・レイノルズによって独立に発見された.

単純型付きラムダ計算では,関数についての変数とその束縛が存在するが,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は依存型などを含んだより強力なラムダ計算とともに,ラムダ・キューブの一角であるとみなすこともできる.

参考文献[編集]