सिस्टम एफ

For इलेक्ट्रॉनिक ट्रान्स संगीत कलाकार, see फेरी कॉर्स्टन.

सिस्टम एफ (पॉलीमॉर्फिक लैम्ब्डा कैलकुलस या सेकंड-ऑर्डर लैम्ब्डा कैलकुलस भी) एक टाइप किया हुआ लैम्ब्डा कैलकुलस है । जो सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस का परिचय देता है । जो प्रकारों पर सार्वभौमिक परिमाणीकरण का एक तंत्र है। सिस्टम एफ प्रोग्रामिंग भाषाओं में पैरामीट्रिक बहुरूपता को औपचारिक रूप देता है । इस प्रकार हास्केल (प्रोग्रामिंग भाषा) और एमएल (प्रोग्रामिंग भाषा) जैसी भाषाओं के लिए एक सैद्धांतिक आधार तैयार करता है। इसकी खोज तर्कशास्त्री जीन-यवेस गिरार्ड (1972) और कंप्यूटर वैज्ञानिक जॉन सी. रेनॉल्ड्स द्वारा स्वतंत्र रूप से की गई थी।

जबकि सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस में शब्दों से अधिक चर होते हैं, और उनके लिए बाइंडर होते हैं । सिस्टम एफ में अतिरिक्त रूप से 'प्रकार' से अधिक चर होते हैं, और उनके लिए बाइंडर होते हैं। एक उदाहरण के रूप में, तथ्य यह है कि पहचान फंक्शन में किसी भी प्रकार का फॉर्म 'A → A हो सकता है । सिस्टम एफ में निर्णय के रूप में औपचारिक है ।

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

जहाँ $\alpha$ प्रकार चर है। ऊपरी स्थिति $\Lambda$ लोअर-केस के विपरीत पारंपरिक रूप से टाइप-लेवल फ़ंक्शंस $\lambda$ को निरूपित करने के लिए उपयोग किया जाता है । जिसका उपयोग मूल्य-स्तरीय कार्यों के लिए किया जाता है। (सुपरस्क्रिप्टेड $\alpha$ इसका कारण है कि बाध्य x प्रकार $\alpha$ का है । बृहदान्त्र के बाद की अभिव्यक्ति इसके पहले लैम्ब्डा अभिव्यक्ति का प्रकार है।)

शब्द पुनर्लेखन सिस्टम के रूप में, सिस्टम एफ नॉर्मलाइज़ेशन प्रॉपर्टी (लैम्ब्डा-कैलकुलस) है। चूँकि, सिस्टम एफ में अनुमान टाइप करें (स्पष्ट प्रकार के एनोटेशन के बिना) अनिर्णीत है। करी-हावर्ड आइसोमोर्फिज्म के अनुसार, सिस्टम एफ दूसरे क्रम के अंतर्ज्ञानवादी लाजिक के टुकड़े से मेल खाता है । जो केवल सार्वभौमिक मात्रा का उपयोग करता है। सिस्टम एफ को लैम्ब्डा घन के हिस्से के रूप में देखा जा सकता है, साथ में और भी अभिव्यंजक टाइप किए गए लैम्ब्डा कैलकुली के साथ, जिनमें आश्रित प्रकार भी सम्मिलित हैं।

गिरार्ड के अनुसार, सिस्टम एफ में एफ को संयोग से चुना गया था।

टाइपिंग नियम

सिस्टम एफ के टाइपिंग नियम निम्नलिखित के अतिरिक्त के साथ केवल टाइप किए गए लैम्ब्डा कैलकुस के हैं ।

${\frac {\Gamma \vdash M\mathbin {:} \forall \alpha .\sigma }{\Gamma \vdash M\tau \mathbin {:} \sigma [\tau /\alpha ]}}$ (1)

${\frac {\Gamma ,\alpha ~{\text{type}}\vdash M\mathbin {:} \sigma }{\Gamma \vdash \Lambda \alpha .M\mathbin {:} \forall \alpha .\sigma }}$ (2)

जहाँ $\sigma ,\tau$ प्रकार हैं । $\alpha$ एक प्रकार चर है, और $\alpha ~{\text{type}}$ संदर्भ में इंगित करता है । $\alpha$ बाध्य है। पहला नियम प्रयोग का है और दूसरा अमूर्तन का है।

लाजिक और विधेय

${\mathsf {Boolean}}$ प्रकार को इस प्रकार परिभाषित किया गया है । $\forall \alpha .\alpha \to \alpha \to \alpha$, जहाँ $\alpha$ प्रकार चर है। इसका कारण यह है: ${\mathsf {Boolean}}$ सभी कार्यों का प्रकार है जो इनपुट के रूप में एक प्रकार α और प्रकार α के दो सेन्स लेते हैं, और आउटपुट के रूप में प्रकार α की अभिव्यक्ति उत्पन्न करते हैं (ध्यान दें कि हम विचार करते हैं $\to$ सही-सहयोगी होना।)

बूलियन मानों के लिए निम्नलिखित दो परिभाषाएँ $\mathbf {T}$ और $\mathbf {F}$ उपयोग किया जाता है । चर्च एन्कोडिंग चर्च बूलियन्स की परिभाषा का विस्तार करते हुए ।

$\mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x$

$\mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y$

(ध्यान दें कि उपरोक्त दो कार्यों के लिए तीन - दो नहीं - तर्कों की आवश्यकता होती है। दो को लैम्ब्डा अभिव्यक्ति होना चाहिए, किन्तु पहला एक प्रकार होना चाहिए। यह तथ्य इस तथ्य में परिलक्षित होता है कि इन भावों का प्रकार है । $\forall \alpha .\alpha \to \alpha \to \alpha$; α को बांधने वाला यूनिवर्सल क्वांटिफायर लैम्ब्डा एक्सप्रेशन में अल्फा को बांधने वाले Λ से मेल खाता है। साथ ही, ध्यान दें ${\mathsf {Boolean}}$ के लिए एक सुविधाजनक आशुलिपि है । $\forall \alpha .\alpha \to \alpha \to \alpha$, किन्तु यह स्वयं सिस्टम एफ का प्रतीक नहीं है, किन्तु एक मेटा-प्रतीक है। वैसे ही, $\mathbf {T}$ और $\mathbf {F}$ सिस्टम एफ असेंबली के मेटा-प्रतीक, सुविधाजनक आशुलिपि भी हैं (बोरबाकी सेन्स में); अन्यथा, यदि इस तरह के कार्यों को नामित किया जा सकता है (सिस्टम एफ के अंदर), तो लैम्ब्डा-अभिव्यंजक उपकरण की आवश्यकता नहीं होगी । जो अज्ञात रूप से कार्यों को परिभाषित करने में सक्षम हो और निश्चित-बिंदु संयोजक के लिए, जो उस प्रतिबंध के आसपास काम करता है।)

फिर इन दोनों के साथ $\lambda$-टर्म्स, हम कुछ लॉजिक संचालक को परिभाषित कर सकते हैं (जो टाइप ${\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}$ के हैं ):

${\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {F} \,\mathbf {T} \end{aligned}}$

ध्यान दें कि उपरोक्त परिभाषाओं में, ${\mathsf {Boolean}}$ एक प्रकार का लाजिक $x$ है । यह निर्दिष्ट करते हुए कि अन्य दो पैरामीटर जो दिए गए हैं । $x$ प्रकार के हैं । ${\mathsf {Boolean}}$. जैसा कि चर्च एनकोडिंग में होता है । a की कोई आवश्यकता नहीं है । यदि फिर कार्य करता है । क्योंकि कोई केवल कच्चा उपयोग कर सकता है । ${\mathsf {Boolean}}$-टाइप की गई नियम निर्णय कार्यों के रूप में होता है। चूँकि, यदि किसी से अनुरोध किया जाता है ।

$\mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz$

विधेय एक कार्य है जो एक ${\mathsf {Boolean}}$-टाइप किया गया मान देता है । सबसे मौलिक विधेय है । इस्ज़ेरो जो लौटता है । $\mathbf {T}$ यदि और केवल यदि इसका लाजिक चर्च एन्कोडिंग 0 चर्च अंक है ।

$\mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T}$

सिस्टम एफ संरचनाएं

सिस्टम एफ पुनरावर्ती निर्माणों को मार्टिन-लोफ के प्रकार के सिद्धांत से संबंधित एक प्राकृतिक विधि से एम्बेड करने की अनुमति देता है। सार संरचनाएं (S) कंस्ट्रक्टर्स का उपयोग करके बनाए गए हैं। ये टाइप किए गए कार्य हैं ।

$K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S$.

पुनरावर्तन तब प्रकट होता है । जब S स्वयं एक प्रकार $K_{i}$ के अंदर प्रकट होता है। यदि m आपके पास है । इन कंस्ट्रक्टर्स S के प्रकार को परिभाषित कर सकते हैं । जैसा:

$\forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha$

उदाहरण के लिए, प्राकृतिक संख्याओं को आगमनात्मक डेटा प्रकार N कंस्ट्रक्टर्स के रूप में परिभाषित किया जा सकता है ।

${\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}$

इस संरचना के अनुरूप सिस्टम एफ प्रकार $\forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha$ है । इस प्रकार की नियमो में चर्च अंक का एक टाइप किया हुआ संस्करण सम्मिलित है । जिनमें से पहले कुछ हैं ।

${\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}$

यदि हम करी गई तर्कों के क्रम को उलट देते हैं (अर्थात, $\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha$), फिर चर्च अंक के लिए n एक ऐसा फ़ंक्शन है । जो f फ़ंक्शन लेता है । लाजिक के रूप में और n^वें की शक्ति f. रिटर्न करता है । कहने का तात्पर्य यह है कि, एक चर्च अंक एक उच्च-क्रम का कार्य है । यह एक f एकल-लाजिक कार्य करता है , और एक और एकल-लाजिक फ़ंक्शन लौटाता है।

प्रोग्रामिंग भाषाओं में प्रयोग

इस आलेख में प्रयुक्त सिस्टम एफ का संस्करण स्पष्ट रूप से टाइप किया गया, या चर्च-शैली, कलन के रूप में है। λ-नियमो में निहित टंकण सूचना टंकण जाँच को सरल बनाती है। जो वेल्स (1994) ने यह सिद्ध करके एक खुली समस्या का समाधान किया कि टाइप चेकिंग सिस्टम एफ के करी-शैली संस्करण के लिए निर्णय समस्या है, अर्थात, जिसमें स्पष्ट प्रकार-चेकिंग एनोटेशन का अभाव है।

वेल्स के परिणाम का तात्पर्य है कि सिस्टम एफ के लिए प्रकार का अनुमान लगाना असंभव है।

हिंडले-मिलनर, या केवल एचएम के रूप में जाना जाने वाला सिस्टम एफ का प्रतिबंध, एक आसान प्रकार का अनुमान एल्गोरिथ्म है और इसका उपयोग कई वैधानिक रूप से टाइप की गई कार्यात्मक प्रोग्रामिंग भाषाओं जैसे हास्केल (प्रोग्रामिंग भाषा) और एमएल प्रोग्रामिंग भाषा वर्ग के लिए किया जाता है। समय के साथ, जैसा कि एचएम-शैली प्रकार प्रणालियों के प्रतिबंध स्पष्ट हो गए हैं । भाषाएं अपने प्रकार प्रणालियों के लिए अधिक अभिव्यंजक लॉजिक्स में तेजी से स्थानांतरित हो गई हैं। ग्लासगो हास्केल कंपाइलर एक हास्केल कंपाइलर, एचएम (2008 तक) से आगे निकल जाता है और गैर-वाक्यविन्यास प्रकार की समानता के साथ विस्तारित सिस्टम एफ का उपयोग करता है । ओकैमल के प्रकार सिस्टम में गैर-एचएम सुविधाओं में सामान्यीकृत बीजगणितीय डेटा प्रकार सम्मिलित हैं।

गिरार्ड-रेनॉल्ड्स समरूपता

दूसरे क्रम के अंतर्ज्ञानवादी लाजिक में, दूसरे क्रम के बहुरूपी लैम्ब्डा कैलकुलस (F2) की खोज गिरार्ड (1972) और स्वतंत्र रूप से रेनॉल्ड्स (1974) द्वारा की गई थी। गिरार्ड ने प्रतिनिधित्व प्रमेय को सिद्ध किया कि दूसरे क्रम के अंतर्ज्ञानवादी विधेय लाजिक (पी 2) में, प्राकृतिक संख्याओं से लेकर प्राकृतिक संख्याओं तक के कार्यों को कुल सिद्ध किया जा सकता है । पी 2 से एफ 2 में एक प्रक्षेपण बनाते हैं। रेनॉल्ड्स ने अमूर्त प्रमेय को सिद्ध किया कि F2 में प्रत्येक शब्द एक तार्किक संबंध को संतुष्ट करता है । जिसे तार्किक संबंध P2 में एम्बेड किया जा सकता है । रेनॉल्ड्स ने सिद्ध किया कि रेनॉल्ड्स एम्बेडिंग के बाद एक गिरार्ड प्रक्षेपण पहचान बनाता है ।

सिस्टम एफ_ω

जबकि सिस्टम एफ हेंक बारेंड्रेगट के पहले अक्ष से मेल खाता है | बैरेन्ड्रेग के लैम्ब्डा क्यूब, सिस्टम एफ_ω या उच्च-क्रम बहुरूपी लैम्ब्डा कलन पहली धुरी (बहुरूपता) को दूसरी धुरी (टाइप संचालक) के साथ जोड़ती है । यह एक अलग, अधिक जटिल सिस्टम है।

सिस्टम एफ_ω प्रणालियों के एक वर्ग पर आगमनात्मक रूप से परिभाषित किया जा सकता है । जहां प्रेरण प्रत्येक सिस्टम में अनुमत प्रकार (प्रकार सिद्धांत) पर आधारित है ।

• $F_{n}$ परमिट प्रकार:
  • $\star$ (प्रकार के प्रकार) और
  • $J\Rightarrow K$ जहाँ $J\in F_{n-1}$ और $K\in F_{n}$ (प्रकार से प्रकार के प्रकार, जहां लाजिक प्रकार निम्न क्रम का है)

सीमा में, हम सिस्टम $F_{\omega }$ को परिभाषित कर सकते हैं ।

• $F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}$

अर्थात एफ_ω वह सिस्टम है । जो कार्यों को प्रकारों से प्रकारों की अनुमति देती है । जहां लाजिक (और परिणाम) किसी भी क्रम का हो सकता है।

ध्यान दें कि चूँकि एफ_ω इन मानचित्रणों में तर्कों के क्रम पर कोई प्रतिबंध नहीं लगाता है । यह इन मानचित्रणों के तर्कों के ब्रह्मांड को प्रतिबंधित करता है । उन्हें मूल्यों के अतिरिक्त प्रकार होना चाहिए। सिस्टम एफ_ω मान से प्रकार (आश्रित प्रकार) तक मैपिंग की अनुमति नहीं देता है । चूँकि यह मान से मान तक मैपिंग की अनुमति देता है ($\lambda$ अमूर्तता), प्रकार से मूल्यों तक मैपिंग ($\Lambda$ अमूर्तता), और प्रकार से प्रकार तक मैपिंग ($\lambda$ प्रकार के स्तर पर अमूर्तता)।

सिस्टम एफ_<:

सिस्टम एफ_<:, उच्चारित एफ-सब उपप्रकार के साथ सिस्टम एफ का विस्तार है। सिस्टम एफ_<: 1980 के दशक से प्रोग्रामिंग भाषा सिद्धांत के लिए केंद्रीय महत्व रहा है । क्योंकि कार्यात्मक प्रोग्रामिंग भाषाओं का मूल, जैसे एमएल (प्रोग्रामिंग भाषा) वर्ग में, पैरामीट्रिक बहुरूपता और रिकॉर्ड (कंप्यूटर विज्ञान) उपप्रकार दोनों का समर्थन करता है । जिसे सिस्टम एफ_< में व्यक्त किया जा सकता है ।

यह भी देखें

• अस्तित्वगत प्रकार - सार्वभौमिक प्रकारों के अस्तित्वगत रूप से परिमाणित प्रतिरूप है ।
• सिस्टम यू

संदर्भ

• 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.

बाहरी संबंध

• Summary of System एफ by Franck Binard.
• System एफ_ω: the workhorse of modern compilers by Greg Morrisett