System Fのソースを表示

{{for|音楽家|フェリー・コーステン}}

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

単純型付きラムダ計算では、関数についての変数とその束縛が存在するが、System Fでは''型''についての変数とその束縛が追加されている。例えば恒等関数は任意の型<math>A</math>について<math>A \to A</math>の形の型を持ちうるが、System Fではこのことが次の判断が成り立つことによって表されている。
:<math>\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha</math>.
ここで、<math>\alpha</math>は[[型変数]]である。また、小文字の<math>\lambda</math>が通常の値レベルの抽象を表しているのに対して、大文字の<math>\Lambda</math>を型レベルの抽象を表すために使用している。

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

==参考文献==
*{{cite conference
  | first = Jean-Yves | last = Girard | authorlink = ジャン＝イヴ・ジラール
  | title = 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
  | book-title = Proceedings of the Second Scandinavian Logic Symposium
  | date = 1971
  | location = Amsterdam
  | pages = 63–92
  }}
*{{cite conference
  | first = John | last = Reynolds | authorlink = ジョン・C・レイノルズ
  | title = Towards a Theory of Type Structure
  | book-title = Colloque sur la Programmation
  | date = 1974
  | location = Paris, France
  | pages = 408&ndash;425
  | url = ftp://ftp.cs.cmu.edu/user/jcr/theotypestr.pdf
  }}
*{{cite book
  | first = Jean-Yves | last = Girard | authorlink = ジャン＝イヴ・ジラール
  | first2 = Yves | last2 = Lafont | authorlink2 = イブ・ラフォン
  | first3 = Paul | last3 = Taylor | authorlink3 = ポール・テイラー
  | title = Proofs and Types
  | publisher = Cambridge University Press
  | year = 1989
  | isbn = 0-521-37181-3
  | url = http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html
  }}
*{{cite conference
  | first = J. B. | last = Wells | authorlink = J・B・ウェルズ
  | title = Typability and type checking in the second-order lambda-calculus are equivalent and undecidable
  | book-title = Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS)
  | date = 1995
  | pages = 176&ndash;185
  | url = 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]]

[[Category:型理論]]
[[Category:ポリモーフィズム (計算機科学)]]