सिस्टम एफ: Difference between revisions
From Vigyanwiki
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{{short description|Typed lambda calculus}} | {{short description|Typed lambda calculus}} | ||
{{For| | {{For|इलेक्ट्रॉनिक ट्रान्स संगीत कलाकार|फेरी कॉर्स्टन}} | ||
जबकि सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में शब्दों से अधिक चर होते हैं, और उनके लिए बाइंडर होते हैं | सिस्टम एफ (पॉलीमॉर्फिक लैम्ब्डा कैलकुलस या सेकंड-ऑर्डर लैम्ब्डा कैलकुलस भी) एक टाइप किया हुआ लैम्ब्डा कैलकुलस है । जो सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस का परिचय देता है । जो प्रकारों पर [[सार्वभौमिक परिमाणीकरण]] का एक तंत्र है। सिस्टम एफ [[प्रोग्रामिंग भाषा]]ओं में [[पैरामीट्रिक बहुरूपता]] को औपचारिक रूप देता है । इस प्रकार [[हास्केल (प्रोग्रामिंग भाषा)]] और [[एमएल (प्रोग्रामिंग भाषा)]] जैसी भाषाओं के लिए एक सैद्धांतिक आधार तैयार करता है। इसकी खोज तर्कशास्त्री [[जीन-यवेस गिरार्ड]] (1972) और कंप्यूटर वैज्ञानिक जॉन सी. रेनॉल्ड्स द्वारा स्वतंत्र रूप से की गई थी। | ||
जबकि सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में शब्दों से अधिक चर होते हैं, और उनके लिए बाइंडर होते हैं । सिस्टम एफ में अतिरिक्त रूप से 'प्रकार' से अधिक चर होते हैं, और उनके लिए बाइंडर होते हैं। एक उदाहरण के रूप में, तथ्य यह है कि पहचान फंक्शन में किसी भी प्रकार का फॉर्म '''A'' → ''A'' हो सकता है । सिस्टम एफ में निर्णय के रूप में औपचारिक है । | |||
:<math>\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha</math> | :<math>\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha</math> | ||
जहाँ <math>\alpha</math> [[प्रकार चर]] है। ऊपरी स्थिति <math>\Lambda</math> लोअर-केस के विपरीत पारंपरिक रूप से टाइप-लेवल फ़ंक्शंस <math>\lambda</math> को निरूपित करने के लिए उपयोग किया जाता है । जिसका उपयोग मूल्य-स्तरीय कार्यों के लिए किया जाता है। (सुपरस्क्रिप्टेड <math>\alpha</math> इसका कारण है कि बाध्य x प्रकार <math>\alpha</math> का है । बृहदान्त्र के बाद की अभिव्यक्ति इसके पहले लैम्ब्डा अभिव्यक्ति का प्रकार है।) | |||
[[शब्द पुनर्लेखन प्रणाली]] के रूप में, सिस्टम एफ नॉर्मलाइज़ेशन प्रॉपर्टी (लैम्ब्डा-कैलकुलस) है। | [[शब्द पुनर्लेखन प्रणाली|शब्द पुनर्लेखन सिस्टम]] के रूप में, सिस्टम एफ नॉर्मलाइज़ेशन प्रॉपर्टी (लैम्ब्डा-कैलकुलस) है। चूँकि, सिस्टम एफ में [[अनुमान टाइप करें]] (स्पष्ट प्रकार के एनोटेशन के बिना) अनिर्णीत है। करी-हावर्ड आइसोमोर्फिज्म के अनुसार, सिस्टम एफ दूसरे क्रम के [[अंतर्ज्ञानवादी तर्क|अंतर्ज्ञानवादी लाजिक]] के टुकड़े से मेल खाता है । जो केवल सार्वभौमिक मात्रा का उपयोग करता है। सिस्टम एफ को [[लैम्ब्डा घन]] के हिस्से के रूप में देखा जा सकता है, साथ में और भी अभिव्यंजक टाइप किए गए लैम्ब्डा कैलकुली के साथ, जिनमें [[आश्रित प्रकार]] भी सम्मिलित हैं। | ||
गिरार्ड के अनुसार, सिस्टम एफ में एफ को संयोग से चुना गया था।<ref>{{Cite journal|last=Girard|first=Jean-Yves|title=चर प्रकार की प्रणाली एफ, पंद्रह साल बाद|journal=Theoretical Computer Science|volume=45|page=160|doi=10.1016/0304-3975(86)90044-7|quote=However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.|year=1986|doi-access=free}}</ref> | गिरार्ड के अनुसार, सिस्टम एफ में एफ को संयोग से चुना गया था।<ref>{{Cite journal|last=Girard|first=Jean-Yves|title=चर प्रकार की प्रणाली एफ, पंद्रह साल बाद|journal=Theoretical Computer Science|volume=45|page=160|doi=10.1016/0304-3975(86)90044-7|quote=However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.|year=1986|doi-access=free}}</ref> | ||
| Line 15: | Line 16: | ||
== टाइपिंग नियम == | == टाइपिंग नियम == | ||
सिस्टम एफ के टाइपिंग नियम निम्नलिखित के अतिरिक्त के साथ केवल टाइप किए गए लैम्ब्डा कैलकुस के हैं | सिस्टम एफ के टाइपिंग नियम निम्नलिखित के अतिरिक्त के साथ केवल टाइप किए गए लैम्ब्डा कैलकुस के हैं । | ||
{| align="center" cellpadding="9" | {| align="center" cellpadding="9" | ||
| Line 21: | Line 22: | ||
| align="center" | <math>{\frac{\Gamma,\alpha~\text{type}\vdash M\mathbin{:}\sigma}{\Gamma\vdash\Lambda\alpha.M\mathbin{:}\forall\alpha.\sigma}}</math> (2) | | align="center" | <math>{\frac{\Gamma,\alpha~\text{type}\vdash M\mathbin{:}\sigma}{\Gamma\vdash\Lambda\alpha.M\mathbin{:}\forall\alpha.\sigma}}</math> (2) | ||
|} | |} | ||
जहाँ <math>\sigma, \tau</math> प्रकार हैं । <math>\alpha</math> एक प्रकार चर है, और <math>\alpha~\text{type}</math> संदर्भ में इंगित करता है । <math>\alpha</math> बाध्य है। पहला नियम प्रयोग का है और दूसरा अमूर्तन का है।<ref>{{cite web |url=https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf |title=प्रोग्रामिंग भाषाओं के लिए व्यावहारिक नींव, दूसरा संस्करण|vauthors=Harper R |author-link=Robert_Harper_(computer_scientist) |pages=142–3}}</ref><ref>{{cite web |url=http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/lectnotes_vol1.pdf |title=गणित के कार्यक्रमों और औपचारिकता के प्रमाण|vauthors=Geuvers H, Nordström B, Dowek G |page=51}}</ref> | |||
<ref>{{cite web |url=https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf |title=प्रोग्रामिंग भाषाओं के लिए व्यावहारिक नींव, दूसरा संस्करण|vauthors=Harper R |author-link=Robert_Harper_(computer_scientist) |pages=142–3}}</ref> | |||
<ref>{{cite web |url=http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/lectnotes_vol1.pdf |title=गणित के कार्यक्रमों और औपचारिकता के प्रमाण|vauthors=Geuvers H, Nordström B, Dowek G |page=51}}</ref> | |||
'''लाजिक और विधेय''' | |||
<math>\mathsf{Boolean}</math> प्रकार को इस प्रकार परिभाषित किया गया है । <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, जहाँ <math>\alpha</math> प्रकार चर है। इसका कारण यह है: <math>\mathsf{Boolean}</math> सभी कार्यों का प्रकार है जो इनपुट के रूप में एक प्रकार α और प्रकार α के दो सेन्स लेते हैं, और आउटपुट के रूप में प्रकार α की अभिव्यक्ति उत्पन्न करते हैं (ध्यान दें कि हम विचार करते हैं <math>\to</math> सही-सहयोगी होना।) | |||
<math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, | |||
बूलियन मानों के लिए निम्नलिखित दो परिभाषाएँ <math>\mathbf{T}</math> और <math>\mathbf{F}</math> उपयोग किया जाता है | बूलियन मानों के लिए निम्नलिखित दो परिभाषाएँ <math>\mathbf{T}</math> और <math>\mathbf{F}</math> उपयोग किया जाता है । चर्च एन्कोडिंग चर्च बूलियन्स की परिभाषा का विस्तार करते हुए । | ||
: <math>\mathbf{T} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^\alpha{.}x</math> | : <math>\mathbf{T} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^\alpha{.}x</math> | ||
: <math>\mathbf{F} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^{\alpha}{.}y</math> | : <math>\mathbf{F} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^{\alpha}{.}y</math> | ||
(ध्यान दें कि उपरोक्त दो कार्यों के लिए तीन - दो नहीं - तर्कों की आवश्यकता होती है। | (ध्यान दें कि उपरोक्त दो कार्यों के लिए तीन - दो नहीं - तर्कों की आवश्यकता होती है। दो को लैम्ब्डा अभिव्यक्ति होना चाहिए, किन्तु पहला एक प्रकार होना चाहिए। यह तथ्य इस तथ्य में परिलक्षित होता है कि इन भावों का प्रकार है । <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>; α को बांधने वाला यूनिवर्सल क्वांटिफायर लैम्ब्डा एक्सप्रेशन में अल्फा को बांधने वाले Λ से मेल खाता है। साथ ही, ध्यान दें <math>\mathsf{Boolean}</math> के लिए एक सुविधाजनक आशुलिपि है । <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, किन्तु यह स्वयं सिस्टम एफ का प्रतीक नहीं है, किन्तु एक मेटा-प्रतीक है। वैसे ही, <math> \mathbf{T}</math> और <math> \mathbf{F}</math> सिस्टम एफ असेंबली के मेटा-प्रतीक, सुविधाजनक आशुलिपि भी हैं ([https://books.google.com/books?id=IL-SI67hjI4C&q=Nicolas+Bourbaki बोरबाकी सेन्स] में); अन्यथा, यदि इस तरह के कार्यों को नामित किया जा सकता है (सिस्टम एफ के अंदर), तो लैम्ब्डा-अभिव्यंजक उपकरण की आवश्यकता नहीं होगी । जो अज्ञात रूप से कार्यों को परिभाषित करने में सक्षम हो और निश्चित-बिंदु संयोजक के लिए, जो उस प्रतिबंध के आसपास काम करता है।) | ||
फिर इन दोनों के साथ <math>\lambda</math>-टर्म्स, हम कुछ लॉजिक | फिर इन दोनों के साथ <math>\lambda</math>-टर्म्स, हम कुछ लॉजिक संचालक को परिभाषित कर सकते हैं (जो टाइप <math> \mathsf{Boolean} \rightarrow \mathsf{Boolean} \rightarrow \mathsf{Boolean}</math> के हैं ): | ||
: <math>\begin{align} | : <math>\begin{align} | ||
\mathrm{AND} &= \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, y\, \mathbf{F}\\ | \mathrm{AND} &= \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, y\, \mathbf{F}\\ | ||
| Line 41: | Line 42: | ||
\mathrm{NOT} &= \lambda x^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, \mathbf{F}\, \mathbf{T} | \mathrm{NOT} &= \lambda x^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, \mathbf{F}\, \mathbf{T} | ||
\end{align}</math> | \end{align}</math> | ||
ध्यान दें कि उपरोक्त परिभाषाओं में, <math>\mathsf{Boolean}</math> एक प्रकार का | ध्यान दें कि उपरोक्त परिभाषाओं में, <math>\mathsf{Boolean}</math> एक प्रकार का लाजिक <math>x</math> है । यह निर्दिष्ट करते हुए कि अन्य दो पैरामीटर जो दिए गए हैं । <math>x</math> प्रकार के हैं । <math>\mathsf{Boolean}</math>. जैसा कि चर्च एनकोडिंग में होता है । a की कोई आवश्यकता नहीं है । {{mono|IFTHENELSE}} कार्य करता है । क्योंकि कोई केवल कच्चा उपयोग कर सकता है । <math>\mathsf{Boolean}</math>-टाइप की गई नियम निर्णय कार्यों के रूप में होता है। चूँकि, यदि किसी से अनुरोध किया जाता है । | ||
: <math>\mathrm{IFTHENELSE} = \Lambda \alpha.\lambda x^{\mathsf{Boolean}}\lambda y^{\alpha}\lambda z^{\alpha}. x \alpha y z </math> | : <math>\mathrm{IFTHENELSE} = \Lambda \alpha.\lambda x^{\mathsf{Boolean}}\lambda y^{\alpha}\lambda z^{\alpha}. x \alpha y z </math> | ||
विधेय एक कार्य है जो एक <math>\mathsf{Boolean}</math>-टाइप किया गया मान देता है । सबसे मौलिक विधेय है । {{mono|ISZERO}} जो लौटता है । <math>\mathbf{T}</math> यदि और केवल यदि इसका लाजिक चर्च एन्कोडिंग {{mono|0}} चर्च अंक है । | |||
: <math>\mathrm{ISZERO} = \lambda n^{\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha}{.}n \, \mathsf{Boolean} \, (\lambda x^{\mathsf{Boolean}}{.}\mathbf{F})\, \mathbf{T}</math> | : <math>\mathrm{ISZERO} = \lambda n^{\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha}{.}n \, \mathsf{Boolean} \, (\lambda x^{\mathsf{Boolean}}{.}\mathbf{F})\, \mathbf{T}</math> | ||
| Line 50: | Line 50: | ||
== सिस्टम एफ संरचनाएं == | == सिस्टम एफ संरचनाएं == | ||
सिस्टम एफ पुनरावर्ती निर्माणों को मार्टिन-लोफ के प्रकार के सिद्धांत से संबंधित एक प्राकृतिक | सिस्टम एफ पुनरावर्ती निर्माणों को मार्टिन-लोफ के प्रकार के सिद्धांत से संबंधित एक प्राकृतिक विधि से एम्बेड करने की अनुमति देता है। सार संरचनाएं ({{mvar|S}}) कंस्ट्रक्टर्स का उपयोग करके बनाए गए हैं। ये टाइप किए गए कार्य हैं । | ||
:<math>K_1\rightarrow K_2\rightarrow\dots\rightarrow S</math>. | :<math>K_1\rightarrow K_2\rightarrow\dots\rightarrow S</math>. | ||
पुनरावर्तन तब प्रकट होता है जब {{mvar|S}} स्वयं एक प्रकार | पुनरावर्तन तब प्रकट होता है । जब {{mvar|S}} स्वयं एक प्रकार <math>K_i</math> के अंदर प्रकट होता है। यदि {{mvar|m}} आपके पास है । इन कंस्ट्रक्टर्स {{mvar|S}} के प्रकार को परिभाषित कर सकते हैं । जैसा: | ||
:<math>\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha</math> | :<math>\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha</math> | ||
उदाहरण के लिए, प्राकृतिक संख्याओं को आगमनात्मक डेटा प्रकार | उदाहरण के लिए, प्राकृतिक संख्याओं को आगमनात्मक डेटा प्रकार {{mvar|N}} कंस्ट्रक्टर्स के रूप में परिभाषित किया जा सकता है । | ||
: <math>\begin{align} | : <math>\begin{align} | ||
\mathit{zero} &: \mathrm{N}\\ | \mathit{zero} &: \mathrm{N}\\ | ||
\mathit{succ} &: \mathrm{N} \rightarrow \mathrm{N} | \mathit{succ} &: \mathrm{N} \rightarrow \mathrm{N} | ||
\end{align}</math> | \end{align}</math> | ||
इस संरचना के अनुरूप सिस्टम एफ प्रकार | इस संरचना के अनुरूप सिस्टम एफ प्रकार <math>\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha</math> है । इस प्रकार की नियमो में [[चर्च अंक]] का एक टाइप किया हुआ संस्करण सम्मिलित है । जिनमें से पहले कुछ हैं । | ||
<math>\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha</math> | |||
: <math>\begin{align} | : <math>\begin{align} | ||
0 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x\\ | 0 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x\\ | ||
| Line 68: | Line 67: | ||
3 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x)) | 3 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x)) | ||
\end{align}</math> | \end{align}</math> | ||
यदि हम करी गई तर्कों के क्रम को उलट देते हैं (अर्थात, <math>\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha</math>), फिर चर्च अंक के लिए {{mvar|n}} एक ऐसा फ़ंक्शन है जो | यदि हम करी गई तर्कों के क्रम को उलट देते हैं (अर्थात, <math>\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha</math>), फिर चर्च अंक के लिए {{mvar|n}} एक ऐसा फ़ंक्शन है । जो {{mvar|f}} फ़ंक्शन लेता है । लाजिक के रूप में और {{mvar|n}}<sup>वें</sup> की शक्ति {{mvar|f}}. रिटर्न करता है । कहने का तात्पर्य यह है कि, एक चर्च अंक एक उच्च-क्रम का कार्य है । यह एक {{mvar|f}} एकल-लाजिक कार्य करता है , और एक और एकल-लाजिक फ़ंक्शन लौटाता है। | ||
== प्रोग्रामिंग भाषाओं में प्रयोग == | == प्रोग्रामिंग भाषाओं में प्रयोग == | ||
इस आलेख में प्रयुक्त सिस्टम एफ का संस्करण स्पष्ट रूप से टाइप किया गया, या चर्च-शैली, कलन के रूप में है। λ- | इस आलेख में प्रयुक्त सिस्टम एफ का संस्करण स्पष्ट रूप से टाइप किया गया, या चर्च-शैली, कलन के रूप में है। λ-नियमो में निहित टंकण सूचना टंकण जाँच को सरल बनाती है। [[जो वेल्स]] (1994) ने यह सिद्ध करके एक खुली समस्या का समाधान किया कि टाइप चेकिंग सिस्टम एफ के करी-शैली संस्करण के लिए [[निर्णय समस्या]] है, अर्थात, जिसमें स्पष्ट [[प्रकार-चेकिंग]] एनोटेशन का अभाव है।<ref>{{cite web |url=http://www.macs.hw.ac.uk/~jbw/research-summary.html |title= जो वेल्स रिसर्च इंटरेस्ट्स|date=2005-01-20 |publisher=Heriot-Watt University |first=J.B. |last=Wells }}</ref><ref>{{cite journal |first=J.B. |last=Wells |title=सिस्टम एफ में टाइपेबिलिटी और टाइप चेकिंग समतुल्य और अनिर्णीत हैं|journal=Ann. Pure Appl. Logic |volume=98 |issue=1–3 |pages=111–156 |year=1999 |doi=10.1016/S0168-0072(98)00047-5 |doi-access=free }}{{cite web|url=http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html|title=The Church Project: Typability and type checking in {S}ystem {F} are equivalent and undecidable|date=29 September 2007|url-status=dead|archive-url=https://web.archive.org/web/20070929211126/http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html|archive-date=29 September 2007}}</ref> | ||
वेल्स के परिणाम का तात्पर्य है कि सिस्टम एफ के लिए प्रकार का अनुमान लगाना असंभव है। | वेल्स के परिणाम का तात्पर्य है कि सिस्टम एफ के लिए प्रकार का अनुमान लगाना असंभव है। | ||
हिंडले-मिलनर, या केवल एचएम के रूप में जाना जाने वाला सिस्टम एफ का प्रतिबंध, एक आसान प्रकार का अनुमान एल्गोरिथ्म है और इसका उपयोग कई वैधानिक रूप से टाइप की गई कार्यात्मक प्रोग्रामिंग भाषाओं जैसे हास्केल (प्रोग्रामिंग भाषा) और [[एमएल प्रोग्रामिंग भाषा]] | |||
हिंडले-मिलनर, या केवल एचएम के रूप में जाना जाने वाला सिस्टम एफ का प्रतिबंध, एक आसान प्रकार का अनुमान एल्गोरिथ्म है और इसका उपयोग कई वैधानिक रूप से टाइप की गई कार्यात्मक प्रोग्रामिंग भाषाओं जैसे हास्केल (प्रोग्रामिंग भाषा) और [[एमएल प्रोग्रामिंग भाषा]] वर्ग के लिए किया जाता है। समय के साथ, जैसा कि एचएम-शैली प्रकार प्रणालियों के प्रतिबंध स्पष्ट हो गए हैं । भाषाएं अपने प्रकार प्रणालियों के लिए अधिक अभिव्यंजक लॉजिक्स में तेजी से स्थानांतरित हो गई हैं। [[ग्लासगो हास्केल कंपाइलर]] एक हास्केल कंपाइलर, एचएम (2008 तक) से आगे निकल जाता है और गैर-वाक्यविन्यास प्रकार की समानता के साथ विस्तारित सिस्टम एफ का उपयोग करता है ।<ref>{{Cite web|url=https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/fc|title=System FC: equality constraints and coercions|website=gitlab.haskell.org|access-date=2019-07-08}}</ref> [[OCaml|ओकैमल]] के प्रकार सिस्टम में गैर-एचएम सुविधाओं में [[सामान्यीकृत बीजगणितीय डेटा प्रकार]] सम्मिलित हैं।<ref>{{cite web|title=OCaml 4.00.1 release notes|date=2012-10-05|access-date=2019-09-23|url=https://ocaml.org/releases/4.00.1.html|website=ocaml.org}}</ref><ref>{{cite web|title=OCaml 4.09 reference manual|date=2012-09-11|access-date=2019-09-23|url=http://caml.inria.fr/pub/docs/manual-ocaml-4.09/manual033.html#s%3Agadts}}</ref> | |||
== गिरार्ड-रेनॉल्ड्स समरूपता == | == गिरार्ड-रेनॉल्ड्स समरूपता == | ||
दूसरे क्रम के अंतर्ज्ञानवादी | दूसरे क्रम के अंतर्ज्ञानवादी लाजिक में, दूसरे क्रम के बहुरूपी लैम्ब्डा कैलकुलस (F2) की खोज गिरार्ड (1972) और स्वतंत्र रूप से रेनॉल्ड्स (1974) द्वारा की गई थी।<ref name=gr2 /> गिरार्ड ने प्रतिनिधित्व प्रमेय को सिद्ध किया कि दूसरे क्रम के अंतर्ज्ञानवादी विधेय लाजिक (पी 2) में, प्राकृतिक संख्याओं से लेकर प्राकृतिक संख्याओं तक के कार्यों को कुल सिद्ध किया जा सकता है । पी 2 से एफ 2 में एक प्रक्षेपण बनाते हैं।<ref name=gr2 /> रेनॉल्ड्स ने अमूर्त प्रमेय को सिद्ध किया कि F2 में प्रत्येक शब्द एक तार्किक संबंध को संतुष्ट करता है । जिसे तार्किक संबंध P2 में एम्बेड किया जा सकता है ।<ref name=gr2 /> रेनॉल्ड्स ने सिद्ध किया कि रेनॉल्ड्स एम्बेडिंग के बाद एक गिरार्ड प्रक्षेपण पहचान बनाता है ।<ref name=gr2>[[Philip Wadler]] (2005) [http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf The Girard-Reynolds Isomorphism (second edition)] [[University of Edinburgh]], [http://wcms.inf.ed.ac.uk/lfcs/research/groups-and-projects/pl/programming-research-at-lfcs Programming Languages and Foundations at Edinburgh]</ref> | ||
== सिस्टम एफ<sub>ω</sub> == | == सिस्टम एफ<sub>ω</sub> == | ||
जबकि सिस्टम एफ हेंक बारेंड्रेगट के पहले अक्ष से मेल खाता है|बैरेन्ड्रेग के लैम्ब्डा क्यूब, सिस्टम एफ<sub>ω</sub>या उच्च-क्रम बहुरूपी लैम्ब्डा कलन पहली धुरी (बहुरूपता) को दूसरी धुरी ([[टाइप ऑपरेटर]]) के साथ जोड़ती है | जबकि सिस्टम एफ हेंक बारेंड्रेगट के पहले अक्ष से मेल खाता है | बैरेन्ड्रेग के लैम्ब्डा क्यूब, सिस्टम एफ<sub>ω</sub> या उच्च-क्रम बहुरूपी लैम्ब्डा कलन पहली धुरी (बहुरूपता) को दूसरी धुरी ([[टाइप ऑपरेटर|टाइप संचालक]]) के साथ जोड़ती है । यह एक अलग, अधिक जटिल सिस्टम है। | ||
सिस्टम एफ<sub>ω</sub> प्रणालियों के एक | सिस्टम एफ<sub>ω</sub> प्रणालियों के एक वर्ग पर आगमनात्मक रूप से परिभाषित किया जा सकता है । जहां प्रेरण प्रत्येक सिस्टम में अनुमत प्रकार (प्रकार सिद्धांत) पर आधारित है । | ||
* <math>F_n</math> परमिट प्रकार: | * <math>F_n</math> परमिट प्रकार: | ||
** <math>\star</math> (प्रकार के प्रकार) और | ** <math>\star</math> (प्रकार के प्रकार) और | ||
** <math>J\Rightarrow K</math> | ** <math>J\Rightarrow K</math> जहाँ <math>J\in F_{n-1}</math> और <math>K\in F_n</math> (प्रकार से प्रकार के प्रकार, जहां लाजिक प्रकार निम्न क्रम का है) | ||
सीमा में, हम | सीमा में, हम सिस्टम <math>F_\omega</math> को परिभाषित कर सकते हैं । | ||
* <math>F_\omega = \underset{1 \leq i}{\bigcup} F_i</math> | * <math>F_\omega = \underset{1 \leq i}{\bigcup} F_i</math> | ||
अर्थात एफ<sub>ω</sub> वह सिस्टम है । जो कार्यों को प्रकारों से प्रकारों की अनुमति देती है । जहां लाजिक (और परिणाम) किसी भी क्रम का हो सकता है। | |||
ध्यान दें कि | ध्यान दें कि चूँकि एफ<sub>ω</sub> इन मानचित्रणों में तर्कों के क्रम पर कोई प्रतिबंध नहीं लगाता है । यह इन मानचित्रणों के तर्कों के ब्रह्मांड को प्रतिबंधित करता है । उन्हें मूल्यों के अतिरिक्त प्रकार होना चाहिए। सिस्टम एफ<sub>ω</sub> मान से प्रकार (आश्रित प्रकार) तक मैपिंग की अनुमति नहीं देता है । चूँकि यह मान से मान तक मैपिंग की अनुमति देता है (<math>\lambda</math> अमूर्तता), प्रकार से मूल्यों तक मैपिंग (<math>\Lambda</math> अमूर्तता), और प्रकार से प्रकार तक मैपिंग (<math>\lambda</math> प्रकार के स्तर पर अमूर्तता)। | ||
== सिस्टम एफ<sub><:</sub> == | == सिस्टम एफ<sub><:</sub> == | ||
सिस्टम एफ<sub><:</sub>, उच्चारित | सिस्टम एफ<sub><:</sub>, उच्चारित एफ-सब उपप्रकार के साथ सिस्टम एफ का विस्तार है। सिस्टम एफ<sub><:</sub> 1980 के दशक से [[प्रोग्रामिंग भाषा सिद्धांत]] के लिए केंद्रीय महत्व रहा है । क्योंकि कार्यात्मक प्रोग्रामिंग भाषाओं का मूल, जैसे एमएल (प्रोग्रामिंग भाषा) वर्ग में, पैरामीट्रिक बहुरूपता और [[रिकॉर्ड (कंप्यूटर विज्ञान)]] उपप्रकार दोनों का समर्थन करता है । जिसे सिस्टम एफ<sub><</sub> में व्यक्त किया जा सकता है ।<ref>{{cite conference | ||
| first = Luca | | first = Luca | ||
| last = Cardelli |author2=Martini, Simone |author3=Mitchell, John C. |author4=Scedrov, Andre | | last = Cardelli |author2=Martini, Simone |author3=Mitchell, John C. |author4=Scedrov, Andre | ||
| Line 112: | Line 114: | ||
== यह भी देखें == | == यह भी देखें == | ||
* [[अस्तित्वगत प्रकार]] - सार्वभौमिक प्रकारों के अस्तित्वगत रूप से परिमाणित प्रतिरूप | * [[अस्तित्वगत प्रकार]] - सार्वभौमिक प्रकारों के अस्तित्वगत रूप से परिमाणित प्रतिरूप है । | ||
* [[सिस्टम यू]] | * [[सिस्टम यू]] | ||
| Line 152: | Line 154: | ||
==बाहरी संबंध== | ==बाहरी संबंध== | ||
{{Wikibooks|Haskell}} | {{Wikibooks|Haskell}} | ||
*[http://www.site.uottawa.ca/~fbinard/Intuitionism/TypeTheory/SystemF/ Summary of System | *[http://www.site.uottawa.ca/~fbinard/Intuitionism/TypeTheory/SystemF/ Summary of System एफ] by Franck Binard. | ||
*[https://web.archive.org/web/20140917015759/http://www.eecs.harvard.edu/~greg/cs256sp2005/lec16.txt System | *[https://web.archive.org/web/20140917015759/http://www.eecs.harvard.edu/~greg/cs256sp2005/lec16.txt System एफ<sub>ω</sub>: the workhorse of modern compilers] by [[Greg Morrisett]] | ||
[[Category: कंप्यूटिंग में 1971]] [[Category: कंप्यूटिंग में 1974]] [[Category: लैम्ब्डा कैलकुलस]] [[Category: प्रकार सिद्धांत]] [[Category: बहुरूपता (कंप्यूटर विज्ञान)]] [[Category: तर्क]] | [[Category: कंप्यूटिंग में 1971]] [[Category: कंप्यूटिंग में 1974]] [[Category: लैम्ब्डा कैलकुलस]] [[Category: प्रकार सिद्धांत]] [[Category: बहुरूपता (कंप्यूटर विज्ञान)]] [[Category: तर्क]] | ||
Revision as of 16:23, 24 May 2023
सिस्टम एफ (पॉलीमॉर्फिक लैम्ब्डा कैलकुलस या सेकंड-ऑर्डर लैम्ब्डा कैलकुलस भी) एक टाइप किया हुआ लैम्ब्डा कैलकुलस है । जो सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस का परिचय देता है । जो प्रकारों पर सार्वभौमिक परिमाणीकरण का एक तंत्र है। सिस्टम एफ प्रोग्रामिंग भाषाओं में पैरामीट्रिक बहुरूपता को औपचारिक रूप देता है । इस प्रकार हास्केल (प्रोग्रामिंग भाषा) और एमएल (प्रोग्रामिंग भाषा) जैसी भाषाओं के लिए एक सैद्धांतिक आधार तैयार करता है। इसकी खोज तर्कशास्त्री जीन-यवेस गिरार्ड (1972) और कंप्यूटर वैज्ञानिक जॉन सी. रेनॉल्ड्स द्वारा स्वतंत्र रूप से की गई थी।
जबकि सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में शब्दों से अधिक चर होते हैं, और उनके लिए बाइंडर होते हैं । सिस्टम एफ में अतिरिक्त रूप से 'प्रकार' से अधिक चर होते हैं, और उनके लिए बाइंडर होते हैं। एक उदाहरण के रूप में, तथ्य यह है कि पहचान फंक्शन में किसी भी प्रकार का फॉर्म 'A → A हो सकता है । सिस्टम एफ में निर्णय के रूप में औपचारिक है ।
जहाँ प्रकार चर है। ऊपरी स्थिति लोअर-केस के विपरीत पारंपरिक रूप से टाइप-लेवल फ़ंक्शंस को निरूपित करने के लिए उपयोग किया जाता है । जिसका उपयोग मूल्य-स्तरीय कार्यों के लिए किया जाता है। (सुपरस्क्रिप्टेड इसका कारण है कि बाध्य x प्रकार का है । बृहदान्त्र के बाद की अभिव्यक्ति इसके पहले लैम्ब्डा अभिव्यक्ति का प्रकार है।)
शब्द पुनर्लेखन सिस्टम के रूप में, सिस्टम एफ नॉर्मलाइज़ेशन प्रॉपर्टी (लैम्ब्डा-कैलकुलस) है। चूँकि, सिस्टम एफ में अनुमान टाइप करें (स्पष्ट प्रकार के एनोटेशन के बिना) अनिर्णीत है। करी-हावर्ड आइसोमोर्फिज्म के अनुसार, सिस्टम एफ दूसरे क्रम के अंतर्ज्ञानवादी लाजिक के टुकड़े से मेल खाता है । जो केवल सार्वभौमिक मात्रा का उपयोग करता है। सिस्टम एफ को लैम्ब्डा घन के हिस्से के रूप में देखा जा सकता है, साथ में और भी अभिव्यंजक टाइप किए गए लैम्ब्डा कैलकुली के साथ, जिनमें आश्रित प्रकार भी सम्मिलित हैं।
गिरार्ड के अनुसार, सिस्टम एफ में एफ को संयोग से चुना गया था।[1]
टाइपिंग नियम
सिस्टम एफ के टाइपिंग नियम निम्नलिखित के अतिरिक्त के साथ केवल टाइप किए गए लैम्ब्डा कैलकुस के हैं ।
| (1) | (2) |
जहाँ प्रकार हैं । एक प्रकार चर है, और संदर्भ में इंगित करता है । बाध्य है। पहला नियम प्रयोग का है और दूसरा अमूर्तन का है।[2][3]
लाजिक और विधेय
प्रकार को इस प्रकार परिभाषित किया गया है । , जहाँ प्रकार चर है। इसका कारण यह है: सभी कार्यों का प्रकार है जो इनपुट के रूप में एक प्रकार α और प्रकार α के दो सेन्स लेते हैं, और आउटपुट के रूप में प्रकार α की अभिव्यक्ति उत्पन्न करते हैं (ध्यान दें कि हम विचार करते हैं सही-सहयोगी होना।)
बूलियन मानों के लिए निम्नलिखित दो परिभाषाएँ और उपयोग किया जाता है । चर्च एन्कोडिंग चर्च बूलियन्स की परिभाषा का विस्तार करते हुए ।
(ध्यान दें कि उपरोक्त दो कार्यों के लिए तीन - दो नहीं - तर्कों की आवश्यकता होती है। दो को लैम्ब्डा अभिव्यक्ति होना चाहिए, किन्तु पहला एक प्रकार होना चाहिए। यह तथ्य इस तथ्य में परिलक्षित होता है कि इन भावों का प्रकार है । ; α को बांधने वाला यूनिवर्सल क्वांटिफायर लैम्ब्डा एक्सप्रेशन में अल्फा को बांधने वाले Λ से मेल खाता है। साथ ही, ध्यान दें के लिए एक सुविधाजनक आशुलिपि है । , किन्तु यह स्वयं सिस्टम एफ का प्रतीक नहीं है, किन्तु एक मेटा-प्रतीक है। वैसे ही, और सिस्टम एफ असेंबली के मेटा-प्रतीक, सुविधाजनक आशुलिपि भी हैं (बोरबाकी सेन्स में); अन्यथा, यदि इस तरह के कार्यों को नामित किया जा सकता है (सिस्टम एफ के अंदर), तो लैम्ब्डा-अभिव्यंजक उपकरण की आवश्यकता नहीं होगी । जो अज्ञात रूप से कार्यों को परिभाषित करने में सक्षम हो और निश्चित-बिंदु संयोजक के लिए, जो उस प्रतिबंध के आसपास काम करता है।)
फिर इन दोनों के साथ -टर्म्स, हम कुछ लॉजिक संचालक को परिभाषित कर सकते हैं (जो टाइप के हैं ):
ध्यान दें कि उपरोक्त परिभाषाओं में, एक प्रकार का लाजिक है । यह निर्दिष्ट करते हुए कि अन्य दो पैरामीटर जो दिए गए हैं । प्रकार के हैं । . जैसा कि चर्च एनकोडिंग में होता है । a की कोई आवश्यकता नहीं है । IFTHENELSE कार्य करता है । क्योंकि कोई केवल कच्चा उपयोग कर सकता है । -टाइप की गई नियम निर्णय कार्यों के रूप में होता है। चूँकि, यदि किसी से अनुरोध किया जाता है ।
विधेय एक कार्य है जो एक -टाइप किया गया मान देता है । सबसे मौलिक विधेय है । ISZERO जो लौटता है । यदि और केवल यदि इसका लाजिक चर्च एन्कोडिंग 0 चर्च अंक है ।
सिस्टम एफ संरचनाएं
सिस्टम एफ पुनरावर्ती निर्माणों को मार्टिन-लोफ के प्रकार के सिद्धांत से संबंधित एक प्राकृतिक विधि से एम्बेड करने की अनुमति देता है। सार संरचनाएं (S) कंस्ट्रक्टर्स का उपयोग करके बनाए गए हैं। ये टाइप किए गए कार्य हैं ।
- .
पुनरावर्तन तब प्रकट होता है । जब S स्वयं एक प्रकार के अंदर प्रकट होता है। यदि m आपके पास है । इन कंस्ट्रक्टर्स S के प्रकार को परिभाषित कर सकते हैं । जैसा:
उदाहरण के लिए, प्राकृतिक संख्याओं को आगमनात्मक डेटा प्रकार N कंस्ट्रक्टर्स के रूप में परिभाषित किया जा सकता है ।
इस संरचना के अनुरूप सिस्टम एफ प्रकार है । इस प्रकार की नियमो में चर्च अंक का एक टाइप किया हुआ संस्करण सम्मिलित है । जिनमें से पहले कुछ हैं ।
यदि हम करी गई तर्कों के क्रम को उलट देते हैं (अर्थात, ), फिर चर्च अंक के लिए n एक ऐसा फ़ंक्शन है । जो f फ़ंक्शन लेता है । लाजिक के रूप में और nवें की शक्ति f. रिटर्न करता है । कहने का तात्पर्य यह है कि, एक चर्च अंक एक उच्च-क्रम का कार्य है । यह एक f एकल-लाजिक कार्य करता है , और एक और एकल-लाजिक फ़ंक्शन लौटाता है।
प्रोग्रामिंग भाषाओं में प्रयोग
इस आलेख में प्रयुक्त सिस्टम एफ का संस्करण स्पष्ट रूप से टाइप किया गया, या चर्च-शैली, कलन के रूप में है। λ-नियमो में निहित टंकण सूचना टंकण जाँच को सरल बनाती है। जो वेल्स (1994) ने यह सिद्ध करके एक खुली समस्या का समाधान किया कि टाइप चेकिंग सिस्टम एफ के करी-शैली संस्करण के लिए निर्णय समस्या है, अर्थात, जिसमें स्पष्ट प्रकार-चेकिंग एनोटेशन का अभाव है।[4][5]
वेल्स के परिणाम का तात्पर्य है कि सिस्टम एफ के लिए प्रकार का अनुमान लगाना असंभव है।
हिंडले-मिलनर, या केवल एचएम के रूप में जाना जाने वाला सिस्टम एफ का प्रतिबंध, एक आसान प्रकार का अनुमान एल्गोरिथ्म है और इसका उपयोग कई वैधानिक रूप से टाइप की गई कार्यात्मक प्रोग्रामिंग भाषाओं जैसे हास्केल (प्रोग्रामिंग भाषा) और एमएल प्रोग्रामिंग भाषा वर्ग के लिए किया जाता है। समय के साथ, जैसा कि एचएम-शैली प्रकार प्रणालियों के प्रतिबंध स्पष्ट हो गए हैं । भाषाएं अपने प्रकार प्रणालियों के लिए अधिक अभिव्यंजक लॉजिक्स में तेजी से स्थानांतरित हो गई हैं। ग्लासगो हास्केल कंपाइलर एक हास्केल कंपाइलर, एचएम (2008 तक) से आगे निकल जाता है और गैर-वाक्यविन्यास प्रकार की समानता के साथ विस्तारित सिस्टम एफ का उपयोग करता है ।[6] ओकैमल के प्रकार सिस्टम में गैर-एचएम सुविधाओं में सामान्यीकृत बीजगणितीय डेटा प्रकार सम्मिलित हैं।[7][8]
गिरार्ड-रेनॉल्ड्स समरूपता
दूसरे क्रम के अंतर्ज्ञानवादी लाजिक में, दूसरे क्रम के बहुरूपी लैम्ब्डा कैलकुलस (F2) की खोज गिरार्ड (1972) और स्वतंत्र रूप से रेनॉल्ड्स (1974) द्वारा की गई थी।[9] गिरार्ड ने प्रतिनिधित्व प्रमेय को सिद्ध किया कि दूसरे क्रम के अंतर्ज्ञानवादी विधेय लाजिक (पी 2) में, प्राकृतिक संख्याओं से लेकर प्राकृतिक संख्याओं तक के कार्यों को कुल सिद्ध किया जा सकता है । पी 2 से एफ 2 में एक प्रक्षेपण बनाते हैं।[9] रेनॉल्ड्स ने अमूर्त प्रमेय को सिद्ध किया कि F2 में प्रत्येक शब्द एक तार्किक संबंध को संतुष्ट करता है । जिसे तार्किक संबंध P2 में एम्बेड किया जा सकता है ।[9] रेनॉल्ड्स ने सिद्ध किया कि रेनॉल्ड्स एम्बेडिंग के बाद एक गिरार्ड प्रक्षेपण पहचान बनाता है ।[9]
सिस्टम एफω
जबकि सिस्टम एफ हेंक बारेंड्रेगट के पहले अक्ष से मेल खाता है | बैरेन्ड्रेग के लैम्ब्डा क्यूब, सिस्टम एफω या उच्च-क्रम बहुरूपी लैम्ब्डा कलन पहली धुरी (बहुरूपता) को दूसरी धुरी (टाइप संचालक) के साथ जोड़ती है । यह एक अलग, अधिक जटिल सिस्टम है।
सिस्टम एफω प्रणालियों के एक वर्ग पर आगमनात्मक रूप से परिभाषित किया जा सकता है । जहां प्रेरण प्रत्येक सिस्टम में अनुमत प्रकार (प्रकार सिद्धांत) पर आधारित है ।
- परमिट प्रकार:
- (प्रकार के प्रकार) और
- जहाँ और (प्रकार से प्रकार के प्रकार, जहां लाजिक प्रकार निम्न क्रम का है)
सीमा में, हम सिस्टम को परिभाषित कर सकते हैं ।
अर्थात एफω वह सिस्टम है । जो कार्यों को प्रकारों से प्रकारों की अनुमति देती है । जहां लाजिक (और परिणाम) किसी भी क्रम का हो सकता है।
ध्यान दें कि चूँकि एफω इन मानचित्रणों में तर्कों के क्रम पर कोई प्रतिबंध नहीं लगाता है । यह इन मानचित्रणों के तर्कों के ब्रह्मांड को प्रतिबंधित करता है । उन्हें मूल्यों के अतिरिक्त प्रकार होना चाहिए। सिस्टम एफω मान से प्रकार (आश्रित प्रकार) तक मैपिंग की अनुमति नहीं देता है । चूँकि यह मान से मान तक मैपिंग की अनुमति देता है ( अमूर्तता), प्रकार से मूल्यों तक मैपिंग ( अमूर्तता), और प्रकार से प्रकार तक मैपिंग ( प्रकार के स्तर पर अमूर्तता)।
सिस्टम एफ<:
सिस्टम एफ<:, उच्चारित एफ-सब उपप्रकार के साथ सिस्टम एफ का विस्तार है। सिस्टम एफ<: 1980 के दशक से प्रोग्रामिंग भाषा सिद्धांत के लिए केंद्रीय महत्व रहा है । क्योंकि कार्यात्मक प्रोग्रामिंग भाषाओं का मूल, जैसे एमएल (प्रोग्रामिंग भाषा) वर्ग में, पैरामीट्रिक बहुरूपता और रिकॉर्ड (कंप्यूटर विज्ञान) उपप्रकार दोनों का समर्थन करता है । जिसे सिस्टम एफ< में व्यक्त किया जा सकता है ।[10][11]
यह भी देखें
- अस्तित्वगत प्रकार - सार्वभौमिक प्रकारों के अस्तित्वगत रूप से परिमाणित प्रतिरूप है ।
- सिस्टम यू
टिप्पणियाँ
- ↑ Girard, Jean-Yves (1986). "चर प्रकार की प्रणाली एफ, पंद्रह साल बाद". Theoretical Computer Science. 45: 160. doi:10.1016/0304-3975(86)90044-7.
However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.
- ↑ Harper R. "प्रोग्रामिंग भाषाओं के लिए व्यावहारिक नींव, दूसरा संस्करण" (PDF). pp. 142–3.
- ↑ Geuvers H, Nordström B, Dowek G. "गणित के कार्यक्रमों और औपचारिकता के प्रमाण" (PDF). p. 51.
- ↑ Wells, J.B. (2005-01-20). "जो वेल्स रिसर्च इंटरेस्ट्स". Heriot-Watt University.
- ↑ Wells, J.B. (1999). "सिस्टम एफ में टाइपेबिलिटी और टाइप चेकिंग समतुल्य और अनिर्णीत हैं". Ann. Pure Appl. Logic. 98 (1–3): 111–156. doi:10.1016/S0168-0072(98)00047-5."The Church Project: Typability and type checking in {S}ystem {F} are equivalent and undecidable". 29 September 2007. Archived from the original on 29 September 2007.
- ↑ "System FC: equality constraints and coercions". gitlab.haskell.org. Retrieved 2019-07-08.
- ↑ "OCaml 4.00.1 release notes". ocaml.org. 2012-10-05. Retrieved 2019-09-23.
- ↑ "OCaml 4.09 reference manual". 2012-09-11. Retrieved 2019-09-23.
- ↑ 9.0 9.1 9.2 9.3 Philip Wadler (2005) The Girard-Reynolds Isomorphism (second edition) University of Edinburgh, Programming Languages and Foundations at Edinburgh
- ↑ Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). "An extension of system F with subtyping". Information and Computation, vol. 9. North Holland, Amsterdam. pp. 4–56. doi:10.1006/inco.1994.1013.
- ↑ Pierce, Benjamin (2002). प्रकार और प्रोग्रामिंग भाषाएँ. MIT Press. ISBN 978-0-262-16209-8., Chapter 26: Bounded quantification
संदर्भ
- 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. doi:10.1016/S0049-237X(08)70843-7.
- Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (Ph.D. thesis) (in français), Université Paris 7.
- Reynolds, John (1974). Towards a Theory of Type Structure (PDF).
- Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Proofs and Types. Cambridge University Press. ISBN 978-0-521-37181-0.
- Wells, J. B. (1994). "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. doi:10.1109/LICS.1994.316068. ISBN 0-8186-6310-3. Postscript version
अग्रिम पठन
- Pierce, Benjamin (2002). "V Polymorphism Ch. 23. Universal Types, Ch. 25. An ML Implementation of System F". Types and Programming Languages. MIT Press. pp. 339–362, 381–388. ISBN 0-262-16209-1.
बाहरी संबंध
Wikibooks has a book on the topic of: Haskell
- Summary of System एफ by Franck Binard.
- System एफω: the workhorse of modern compilers by Greg Morrisett
