सिस्टम एफ

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{array}{rl}\mathrm{A}\mathrm{N}\mathrm{D}& =\mathrm{\lambda <!--\; \lambda \; -->}{x}^{\mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}}\end{array}$