System F

音楽家については「フェリー・コーステン」をご覧ください。

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

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

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

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

項書換え系として見ると，System Fは強正規化性を持つ．しかしながらSystem Fにおける型推論は決定不能である．またSystem Fはカリー＝ハワード同型の下で，全称量化のみを用いる2階直観主義論理の断片に対応する．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”. Colloque sur la Programmation. Paris, France. pp. 408–425. ftp://ftp.cs.cmu.edu/user/jcr/theotypestr.pdf 
• Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Proofs and Types. Cambridge University Press. ISBN 0-521-37181-3. http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html. 
• 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. http://www.macs.hw.ac.uk/~jbw/papers/Wells:Typability-and-Type-Checking-in-the-Second-Order-Lambda-Calculus-Are-Equivalent-and-Undecidable:LICS-1994.ps.gz 

関連項目[編集]

• F Sharp