System F









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


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


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



⊢Λα.λxα.x:∀α.α→α{displaystyle vdash Lambda alpha .lambda x^{alpha }.x:forall alpha .alpha to alpha }vdash Lambda alpha .lambda x^{alpha }.x:forall alpha .alpha to alpha .

ここで，α{displaystyle alpha }alpha は型変数である．また，小文字のλ{displaystyle lambda }lambda が通常の値レベルの抽象を表しているのに対して，大文字のΛ{displaystyle 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



Popular posts from this blog

MongoDB - Not Authorized To Execute Command

Image
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box; } 0 I have successfully enabled authorization on MongoDB and I have created an account on the admin database and then I created an account for my database called test. The following connection string to connect to my test database works successfully: mongo --host 192.168.17.52 --port 27017 -u user1 -p password --authenticationDatabase test Only problem I have now is, I cannot execute commands such as: show dbs. I get the following error when I try to do so: "errmsg" : "not authorized on admin to execute command { listDatabases: 1.0, lsid: { id: UUID("a1d5bc0d-bc58-485e-b232-270758a89455") }, $db: "admin...
Read more

Npm cannot find a required file even through it is in the searched directory

Image
up vote 0 down vote favorite I got that error: users-Air:pdfuploader user$ npm run start client@0.1.0 start /Users/user/Documents/pdfuploader react-scripts start Could not find a required file. Name: index.html Searched in: /Users/user/Documents/pdfuploader/public npm ERR! code ELIFECYCLE npm ERR! errno 1 npm ERR! client@0.1.0 start: `react-scripts start` npm ERR! Exit status 1 npm ERR! npm ERR! Failed at the client@0.1.0 start script. npm ERR! This is probably not a problem with npm. There is likely additional logging output above. npm ERR! A complete log of this run can be found in: npm ERR! /Users/user/.npm/_logs/2018-11-19T10_19_14_555Z-debug.log users-Air:pdfuploader user$ And the file is in /Users/user/Documents/pdfuploader/public as you can see in my github repository: https://github.c...
Read more

in spring boot 2.1 many test slices are not allowed anymore due to multiple @BootstrapWith

Image
1 I tried to upgrade a yummy sandwich made of two test slices (@JsonTest and @JdbcTest in my case, crunchy test code in between) adding spring boot 2.1 flavour to it. But it seems it was not much of a success. I cannot annotate my tests with many @...Test since they are now each bringing their own XxxTestContextBootstrapper. It used to work when they all used same SpringBootTestContextBootstrapper. @RunWith(SpringRunner.class) @JdbcTest @JsonTest public class Test { @Test public void test() { System.out.printn("Hello, World !"); } } The error I get from BootstrapUtils is illegalStateException : Configuration error: found multiple declarations of @BootstrapWith for test class I understand I might be doing something wrong here but is there an easy way I could load both Json and Jdbc contex...
Read more