कप्पा कैलकुलस

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

लैम्ब्डा कैलकुलस के विपरीत, कप्पा कैलकुलस में कोई नहीं है, जिसके लिए उच्च-क्रम के कार्य द्वारा इसे प्रदर्शित करते हैं। इसके निम्नलिखित कार्य हैं, प्रथम श्रेणी की वस्तु नहीं रहती है, जिसके आधार पर यह कप्पा-कैलकुलस हो सकता है, टाइप किए गए प्रथम-क्रम के टुकड़े के पुनर्रचना के रूप में माना जाता है, जो लैम्ब्डा कैलकुलस को व्यक्त करता हैं।

क्योंकि इसके कार्य प्रथम श्रेणी की वस्तुएं नहीं हैं, कप्पा का मूल्यांकन कैलकुलस मुख्य रूप से अभिव्यक्ति की आवश्यकता नहीं है, जो समापन (कंप्यूटर विज्ञान) को व्यक्त करता हैं।

परिभाषा

नीचे दी गई परिभाषा हसेगावा के पृष्ठ 205 और 207 पर दिए गए चित्र से ली गई है।

व्याकरण

कप्पा कैलकुलस में दिए गए प्रकार और अभिव्यक्तियाँ उपस्थित हैं, नीचे व्याकरण:

$\tau =1\mid \tau \times \tau \mid \ldots$

$e=x\mid id_{\tau }\mid !_{\tau }\mid \operatorname {lift} _{\tau }(e)\mid e\circ e\mid \kappa x:1{\to }\tau .e$

दूसरे शब्दों में,

• 1 प्रकार है
• यदि $\tau _{1}$ और $\tau _{2}$ तो प्रकार हैं, तो $\tau _{1}\times \tau _{2}$ इसका प्रकार है।
• प्रत्येक वैरियेबल एक अभिव्यक्ति है।
• यदि τ तो प्रकार है, तथा $id_{\tau }$ अभिव्यक्ति ।है
• यदि τ तो प्रकार है, तथा $!_{\tau }$ अभिव्यक्ति है।
• यदि τ प्रकार है और e अभिव्यक्ति है, तथा $\operatorname {lift} _{\tau }(e)$ अभिव्यक्ति है।
• यदि $e_{1}$ और $e_{2}$ तो फिर अभिव्यक्ति हैं, तथा $e_{1}\circ e_{2}$ अभिव्यक्ति है।
• यदि x चर है, τ प्रकार है, और e अभिव्यक्ति है, तथा $\kappa x{:}1{\to }\tau \;.\;e$ अभिव्यक्ति है $:1{\to }\tau$ h> और की सबस्क्रिप्ट id, !, और $\operatorname {lift}$ हैं।

कभी-कभी छोड़ दिया जाता है जब उन्हें स्पष्ट रूप से इसके प्रसंग द्वारा निर्धारित किया जा सकता है।

जक्स्टापोजीशन का प्रयोग अधिकांशतः $\operatorname {lift}$ और रचना के संयोजन के संक्षिप्त रूप के रूप में किया जाता है,:

$e_{1}e_{2}\ {\overset {\operatorname {def} }{=}}\ e_{1}\circ \operatorname {lift} (e_{2})$

टाइपिंग नियम

यहां प्रस्तुतीकरण अनुक्रमों ($\Gamma \vdash e:\tau$) का उपयोग करता है, जो केवल टाइप किए गए लैम्ब्डा कैलकुलस के साथ तुलना को साधारण बनाने के लिए काल्पनिक निर्णयों के अतिरिक्त उपयोगी हैं। इसके लिए अतिरिक्त वार नियम की आवश्यकता है, जो हसेगावा में प्रकट नहीं होता है

कप्पा कैलकुलस में अभिव्यक्ति के दो प्रकार होते हैं: उसके स्रोत का प्रकार और यह इसके लक्ष्य का प्रकार हैं। इसका संकेतन $e:\tau _{1}{\to }\tau _{2}$ द्वारा किया जाता हैं, जिसका यह इंगित करने के लिए प्रयोग किया जाता है कि अभिव्यक्ति ई में ${\tau _{1}}$ और लक्ष्य प्रकार ${\tau _{2}}$ स्रोत प्रकार है।

कप्पा कैलकुलस में अभिव्यक्तियों को निम्नलिखित नियमों के अनुसार प्रकार निर्दिष्ट किया गया है:

${x{:}1{\to }\tau \;\in \;\Gamma } \over {\Gamma \vdash x:1{\to }\tau }$	(Var)
${} \over {\vdash id_{\tau }\;:\;\tau \to \tau }$	(Id)
${} \over {\vdash !_{\tau }\;:\;\tau \to 1}$	(Bang)
${\Gamma \vdash e_{1}{:}\tau _{1}{\to }\tau _{2}\;\;\;\;\;\;\Gamma \vdash e_{2}{:}\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash e_{2}\circ e_{1}:\tau _{1}{\to }\tau _{3}}$	(Comp)
${\Gamma \vdash e{:}1{\to }\tau _{1}} \over {\Gamma \vdash \operatorname {lift} _{\tau _{2}}(e)\;:\;\tau _{2}\to (\tau _{1}\times \tau _{2})}$	(Lift)
${\Gamma ,\;x{:}1{\to }\tau _{1}\;\vdash \;e:\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}$	(Kappa)

दूसरे शब्दों में,

• वीएआर: मान लेना $x:1{\to }\tau$ आपको $x:1{\to }\tau$ निष्कर्ष निकालने देता है।
• आईडी: किसी भी प्रकार के लिए τ, $id_{\tau }:\tau {\to }\tau$ का उपयोग करता हैं।
• बैंग: किसी भी प्रकार के लिए τ, $!_{\tau }:\tau {\to }1$ का उपयोग करता हैं।
• कंप: यदि लक्ष्य प्रकार का $e_{1}$ के स्रोत प्रकार से मेल खाता है $e_{2}$ उन्हें अभिव्यक्ति बनाने के लिए रचा जा सकता है, $e_{2}\circ e_{1}$ स्रोत प्रकार के साथ $e_{1}$ और लक्ष्य प्रकार $e_{2}$ प्रकार का हैं।
• लिफ्ट: यदि $e:1{\to }\tau _{1}$, तब $\operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})$ प्राप्त होता हैं।
• कप्पा: यदि हम $e:\tau _{2}\to \tau _{3}$ निष्कर्ष निकाल सकें, इस धारणा के अनुसार $x:1{\to }\tau _{1}$ को हम इस धारणा के बिना निष्कर्ष निकाल सकते हैं कि $\kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}$ प्राप्त हो।

समानताएँ

कप्पा कैलकुलस निम्नलिखित समानताओं का पालन करता है:

• तटस्थता: यदि $f:\tau _{1}{\to }\tau _{2}$ तब $f{\circ }id_{\tau _{1}}=f$ और $f=id_{\tau _{2}}{\circ }f$ हैं।
• सहयोगिता: यदि $f:\tau _{1}{\to }\tau _{2}$, $g:\tau _{2}{\to }\tau _{3}$, और $h:\tau _{3}{\to }\tau _{4}$, तब $(h{\circ }g){\circ }f=h{\circ }(g{\circ }f)$ हैं।
• टर्मिनललिटी: यदि $f{:}\tau {\to }1$ और $g{:}\tau {\to }1$ तब $f=g$ हैं।
• लिफ्ट-कमी: $(\kappa x.f)\circ \operatorname {lift} _{\tau }(c)=f[c/x]$ हैं।
• कप्पा-कमी: $\kappa x.(h\circ \operatorname {lift} _{\tau }(x))=h$ यदि x, h में मुफ़्त नहीं है।

अंतिम दो समानताएं कलन के लिए कटौती नियम हैं, जिसे बाएँ से दाएँ पुनः लिखा जाता हैं।।

गुण

प्रारूप 1 को इकाई प्रकार माना जा सकता है। इसके कारण, कोई भी दो फ़ंक्शन जिनका तर्क प्रकार समान है और जिनका परिणाम प्रकार समान है, वे 1 के बराबर होने चाहिए- क्योंकि प्रकार का केवल ही मान है, इस प्रकार 1 दोनों फ़ंक्शन को प्रत्येक तर्क (टर्मिनैलिटी) के लिए वह मान लौटाना होगा।

इस प्रकार इसके सहित $1{\to }\tau$ भाव को इसके आधार के स्थिरांक या मान के रूप में माना जा सकता है, जो यह है क्योंकि 1 इकाई प्रकार का है, और इसलिए इस प्रकार का फ़ंक्शन आवश्यक रूप से स्थिर फ़ंक्शन है। ध्यान दें कि कप्पा नियम केवल अमूर्तता की अनुमति देता है, जब अमूर्त किए जा रहे वैरियेबल का प्रकार $1{\to }\tau$ होता है, तब कुछ τ के लिए यह मौलिक तंत्र है, जो यह सुनिश्चित करता है कि सभी कार्य प्रथम-क्रम के हों।

श्रेणीबद्ध शब्दार्थ

कप्पा कैलकुलस की आंतरिक भाषा होने का चिह्न है, इसके प्रासंगिक रूप से पूर्ण श्रेणियाँ प्राप्त होती हैं।

उदाहरण

अनेक तर्कों वाले भावों के स्रोत प्रकार होते हैं जो हैं, जिसके लिए दाएँ-असंतुलित बाइनरी ट्री को उदाहरण के लिए तीन f फ़ंक्शन प्रकार के ए, बी, और सी के तर्क और परिणाम प्रकार डी में प्रकार होगा जो इस प्रकार हैं।

$f:A\times (B\times (C\times 1))\to D$

यदि हम वाम-सहयोगी जुड़ाव को $f\;c$ संक्षिप्त रूप में परिभाषित करते हैं, जिसके लिए $(f\circ \operatorname {lift} (c))$, फिर $a:1{\to }A$, $b:1{\to }B$ को मानकर और $c:1{\to }C$ को हम इस फ़ंक्शन को लागू कर सकते हैं:

$f\;a\;b\;c\;:\;1\to D$

अभिव्यक्ति के बाद से $f\;a\;b\;c$ स्रोत प्रकार है 1, यह ग्राउंड वैल्यू है और इसे किसी अन्य फ़ंक्शन के तर्क के रूप में पारित किया जा सकता है। यदि $g:(D\times E){\to }F$, तब

$g\;(f\;a\;b\;c)\;:\;E\to F$

इस सीमा तक प्राप्त होने वाले इन प्रकारों के फ़ंक्शन $A{\to }(B{\to }(C{\to }D))$ के समान लैम्ब्डा कैलकुलस में, आंशिक आवेदन संभव है:

$f\;a\;:\;B\times (C\times 1)\to D$

चूंकि इसका कोई उच्चतर प्रकार नहीं हैं, अर्थात $(\tau {\to }\tau ){\to }\tau$) इसमें उपस्थित हैं। ध्यान दें क्योंकि स्रोत प्रकार का f a क्या 1 नहीं है, अब तक उल्लिखित मान्यताओं के तहत निम्नलिखित अभिव्यक्ति को अच्छी तरह से टाइप नहीं किया जा सकता है:

$h\;(f\;a)$

क्योंकि क्रमिक अनुप्रयोग का उपयोग एकाधिक के लिए किया जाता है तर्कों में किसी फ़ंक्शन की योग्यता जानना आवश्यक नहीं है, इसकी टाइपिंग निर्धारित करने का आदेश उदाहरण के लिए, यदि हम यह जानते हैं$c:1{\to }C$ फिर यह अभिव्यक्ति इस प्रकार हैं-

j c

जब तक यह अच्छी तरह से टाइप किया गया है, जिसे j प्रकार से इंगित करते हैं।

$(C\times \alpha ){\to }\beta$ कुछ के लिए α

और β की गणना करते समय यह संपत्ति महत्वपूर्ण है, इसकी अभिव्यक्ति का मुख्य प्रकार जो उच्च-क्रम को बाहर करने का प्रयास करते समय कठिन हो सकता है, इनके प्रकारों के व्याकरण को सीमित करके टाइप किए गए लैम्ब्डा कैलकुली से कार्य करता है।

इतिहास

बेरेन्ड्रेट ने मूल रूप से परिचय दिया गया हैं।

संयोजन बीजगणित के संदर्भ में कार्यात्मक पूर्णता

कप्पा कैलकुलस लैम्बेक कार्यात्मक का उपयुक्त एनालॉग तैयार करने के लिए इस श्रेणियों के लिए पूर्णता द्वारा प्रतिपादित किया जाता हैं। हसेगावा ने बाद में कप्पा विकसित किया गया हैं। इस कैलकुलस को प्रयोग करने योग्य यद्यपि सरल प्रोग्रामिंग भाषा में उपस्थित करते हैं, इसकी प्राकृतिक संख्याओं और पुनरावृत्ति पर अंकगणित को व्यक्त करते हैं। एरो से कनेक्शन के लिए कंप्यूटर विज्ञान में जांच की गई पावर, थिएलेके और अन्य लोगो द्वारा की गई थी।(see Hermida and Jacobs, section 1)

वेरिएंट

कप्पा कैलकुलस के संस्करणों का पता लगाना संभव है, इस प्रकार अवसंरचनात्मक तर्क जैसे रैखिक प्रकार प्रणाली, एफ़िन तर्क और गैरअनुवांशिक तर्क प्रकार के हैं। इन एक्सटेंशन को हटाने की आवश्यकता है, जिसे प्रतिबंधित करना $!_{\tau }$ की अभिव्यक्ति हैं। ऐसी परिस्थितियों में × प्रकार के ऑपरेटर के लिए यह सत्य कार्टेशियन उत्पाद नहीं है, और इसे सामान्यत रूप से ⊗ द्वारा लिखा जाता है।