सिस्टम एफ

For the electronic trance music artist, see Ferry Corsten.

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

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

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

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

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

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

टाइपिंग नियम

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

${\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}}$ h> प्रकार को इस प्रकार परिभाषित किया गया है: $\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$, लेकिन यह स्वयं सिस्टम F का प्रतीक नहीं है, बल्कि एक मेटा-प्रतीक है। वैसे ही, $\mathbf {T}$ और $\mathbf {F}$ सिस्टम F असेंबली के मेटा-प्रतीक, सुविधाजनक आशुलिपि भी हैं (Bourbaki sense में); अन्यथा, यदि इस तरह के कार्यों को नामित किया जा सकता है (सिस्टम एफ के भीतर), तो लैम्ब्डा-अभिव्यंजक उपकरण की आवश्यकता नहीं होगी जो अज्ञात रूप से कार्यों को परिभाषित करने में सक्षम हो और निश्चित-बिंदु संयोजक के लिए, जो उस प्रतिबंध के आसपास काम करता है।)

फिर इन दोनों के साथ $\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 की कोई आवश्यकता नहीं है IFTHENELSE कार्य करता है क्योंकि कोई केवल कच्चा उपयोग कर सकता है ${\mathsf {Boolean}}$-टाइप की गई शर्तें निर्णय कार्यों के रूप में। हालांकि, अगर किसी से अनुरोध किया जाता है:

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

करूंगा। एक विधेय एक कार्य है जो एक देता है ${\mathsf {Boolean}}$-टाइप किया गया मान। सबसे मौलिक विधेय है ISZERO जो लौटता है $\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 तक) से आगे निकल जाता है और गैर-वाक्यविन्यास प्रकार की समानता के साथ विस्तारित सिस्टम एफ का उपयोग करता है; OCaml के प्रकार सिस्टम में गैर-एचएम सुविधाओं में सामान्यीकृत बीजगणितीय डेटा प्रकार शामिल हैं।

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

दूसरे क्रम के अंतर्ज्ञानवादी तर्क में, दूसरे क्रम के बहुरूपी लैम्ब्डा कैलकुलस (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$ प्रकार के स्तर पर अमूर्तता)।

सिस्टम एफ_<:

सिस्टम एफ_<:, उच्चारित F-sub उपप्रकार के साथ सिस्टम F का विस्तार है। सिस्टम एफ_<: 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 F by Franck Binard.
• System F_ω: the workhorse of modern compilers by Greg Morrisett