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

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

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

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

परिभाषा

नीचे दी गई परिभाषा हसेगावा के पृष्ठ 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}$ हैं

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

Juxtaposition का प्रयोग अक्सर संयोजन के संक्षिप्त रूप के रूप में किया जाता है $\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$
• Comp: यदि लक्ष्य प्रकार का $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$ कुछ के लिए α

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

इतिहास

बेरेन्ड्रेट ने मूल रूप से परिचय दियाशब्द

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

कप्पा कैलकुलस लैम्बेक कार्यात्मक का एक उपयुक्त एनालॉग तैयार करने के लिए मनमानी श्रेणियों के लिए पूर्णता (हर्मिडा और जैकब्स देखें,<रेफरी)। नाम=हर्मिडा जैकब्स/> अनुभाग 1)। हसेगावा ने बाद में कप्पा विकसित किया कैलकुलस को एक प्रयोग करने योग्य (यद्यपि सरल) प्रोग्रामिंग भाषा में शामिल करें प्राकृतिक संख्याओं और आदिम पुनरावृत्ति पर अंकगणित।<रेफरी नाम = हसेगावा /> एरो से कनेक्शन (कंप्यूटर विज्ञान) बाद में जांच की गईपावर, थिएलेके और अन्य द्वारा।

वेरिएंट

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

× प्रकार ऑपरेटर एक सच्चा कार्टेशियन उत्पाद नहीं है,

और आम तौर पर लिखा जाता है ⊗ इसे स्पष्ट करने के लिए।