System F（システム・エフ）は、型付きラムダ計算の一体系であり、単純型付きラムダ計算に、型についての全称量化を取り入れた計算機構である。二階ラムダ計算、ポリモーフィックラムダ計算とも言われる。プログラミング言語での(パラメトリック多相)を形式化するもので、関数型言語のMLやHaskellなどの型システムのベース理論にされている。System Fは、論理学者のジャン＝イヴ・ジラールと計算機科学者の(ジョン・C・レイノルズ)の両者が別個に発見している。ジラールによるとSystem Fの語源は、たまたまそう名付けただけと言う。
単純型付きラムダ計算では、関数についての変数とその束縛が存在するが、System Fでは型についての変数とその束縛が追加されている。例えば恒等関数は任意の型についての形の型を持ちうるが、System Fではこのことが次の判断が成り立つことによって表されている。
- .
ここで、は(型変数)である。また、小文字のが通常の値レベルの抽象を表しているのに対して、大文字のを型レベルの抽象を表すために使用している。
項書換え系として見ると、System Fは(強正規化性)を持つ。しかしながらSystem Fにおける型推論は決定不能である。またSystem Fはカリー＝ハワード同型の下で、全称量化のみを用いる二階直観主義論理の断片に対応する。System Fは、依存型などを含んだより強力なラムダ計算とともに、ラムダ・キューブの一角であるとみなすこともできる。
参考文献
- Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Proceedings of the Second Scandinavian Logic Symposium. Amsterdam. pp. 63–92.
- (Reynolds, John) (1974). "Towards a Theory of Type Structure" (PDF). Colloque sur la Programmation. Paris, France. pp. 408–425.
- Girard, Jean-Yves; (Lafont, Yves); Taylor, Paul (1989). Proofs and Types. Cambridge University Press. ISBN (0-521-37181-3)
- (Wells, J. B.) (1995). "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable". Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 176–185.