システムF

ウィキペディア

System F

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/09/07 02:10 UTC 版)

System Fは型付きラムダ計算の一体系で，単純型付きラムダ計算に型についての全称量化を導入したものである．2階ラムダ計算や（ジラール–レイノルズ）多相ラムダ計算としても知られる．プログラミング言語におけるパラメータ多相を形式化するもので，MLやHaskellのような関数型言語の理論的な背景となっている．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は依存型などを含んだより強力なラムダ計算とともに，ラムダ・キューブの一角であるとみなすこともできる．

参考文献

• 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

ウィキペディア小見出し辞書

システムF(1999-2002)

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/01/05 01:47 UTC 版)

「フェリー・コーステン」の記事における「システムF(1999-2002)」の解説

詳細は「en:Gouryella」を参照 1990年代末に人気を博しだしたことにより、 DJ Tiësto (グリエラ, Vimana), ヴィンセント・デ・ムーア(音楽ユニットVeracochaを結成),ロバート・スミット(Robert Smit,Starparty)といったトランス界のミュージシャンやDJたちと共演する機会が増えた。1999年2月、 コーステンはソロプロジェクト、システムF(System F)名義でTsunamiから"Out of the Blue"までのアルバムを出した。そのアルバムにはメロディックな楽曲が含まれており、世界中のダンスフロアでヒットし、イギリスのシングルチャートではトップ20に入ったこともあり、その後にでた Robert Smitとの共同プロデュースで出されたシングル "Cry"もイギリスのチャートのトップ20に入った。 5月にリリースされたグリエラ名義の楽曲 "Gouryella" のシングルはUK Singles Top 75で15位を記録するなど、世界中でヒットを巻き起こした。その次に出たシングル "Walhalla"もイギリスのシングルチャートで27位を記録。1999年、コーステンはロンドンのEricsson Muzik Awardでプロデューサー・オブ・イヤーを受賞した 。2000年9月Gouryellaから3rdシングル "Tenshi"がリリースされた。同年にはWilliam Orbit の『弦楽のためのアダージョ』（原作：サミュエル・バーバー） と、U2の『ニュー・イヤーズ・デイ（英語版）』をリミックスし、このうち『弦楽のためのアダージョ』のリミックス版はDancestar 2000アワードを受賞した。Ministry of SoundプレゼンツのダンスコンピレーションシリーズTrance Nation はイギリスでもっともよく売れたダンスコンピレーションアルバムとなり、プラチナディスクを獲得するにいたった。 2001年、日本の歌手浜崎あゆみの楽曲のリミックスを担当。2002年にリリースしたアルバム『I am...』の収録曲「Connected」にトランス色の強いプロデュースとなり、ドイツでは2003年にヨーロッパでシングルとしてリリースされた。 2002年には自身初のベストアルバム「Very Best Of Ferry Corsten System F」をリリース。