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

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

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

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

परिभाषा

नीचे दी गई परिभाषा हसेगावा के पृष्ठ 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)
$\frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->e:1\to <!--\; \to \; -->{\mathrm{\tau <!--\; \tau \; -->}}_1}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->}$