लैम्ब्डा क्यूब: Difference between revisions

Latest revision as of 15:32, 31 July 2023

लैम्ब्डा क्यूब. प्रत्येक तीर की दिशा समावेशन की दिशा है।

गणितीय तर्क और प्रकार सिद्धांत में λ-क्यूब जिसे लैम्ब्डा क्यूब भी लिखा जाता है, मुख्य रूप से यह हेन्क बेरेन्ड्रेट द्वारा प्रस्तुत रूपरेखा है।^[1] इस प्रकार विभिन्न आयामों की जांच करने के लिए जिसमें निर्माणों की गणना सरल रूप से टाइप किए जाने वाले λ-कैलकुलस का सामान्यीकरण है। इसके आधार पर इस घन का प्रत्येक आयामों पर प्राप्त होने वाले शब्दों और प्रकारों के बीच नए प्रकार की निर्भरता से मेल खाता है। यहाँ पर इस निर्भरता से तात्पर्य किसी शब्द या प्रकार के मुक्त वैरियेबल और किसी शब्द या प्रकार से बंधे वैरियेबल की क्षमता से है। इस प्रकार λ-घन के संबंधित आयाम इसके अनुरूप हैं:

x-अक्ष ( $\rightarrow$ ): ऐसे प्रकार जो आश्रित प्रकार के अनुरूप शब्दों को बांध सकते हैं।
y-अक्ष ( $\uparrow$ ): वे शब्द जो पैरामीट्रिक बहुरूपता के अनुरूप प्रकारों को बांध सकते हैं।
z-अक्ष ( $\nearrow$ ): ऐसे प्रकार जो बाध्यकारी प्रकार के ऑपरेटरों के अनुरूप प्रकारों को बांध सकते हैं।

इन तीन आयामों को संयोजित करने के विभिन्न तरीकों से घन के 8 शीर्ष प्राप्त होते हैं, जिनमें इस प्रकार से प्रत्येक अलग प्रकार की टाइप की गई प्रणाली के अनुरूप होता है। इस प्रकार λ-क्यूब को शुद्ध प्रकार की प्रणाली की अवधारणा में सामान्यीकृत किया जा सकता है।

सिस्टम के उदाहरण

(λ→) बस लैम्ब्डा कैलकुलस टाइप किया गया हैं।

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

${\frac {\Gamma ,x:\sigma \;\vdash \;t:\tau }{\Gamma \;\vdash \;\lambda x.t:\sigma \to \tau }}$

(λ2) सिस्टम एफ

सिस्टम एफ को दूसरे क्रम में टाइप किए गए लैम्ब्डा कैलकुलस के लिए इसे λ2 भी कहा जाता है,^[2] इसके लिए अन्य प्रकार का अमूर्त मान इस प्रकार हैं कि इसे ए ( $\Lambda$ ) के साथ लिखा जाता है, जो निम्नलिखित नियम के साथ शब्दों को प्रकारों पर निर्भर करने की अनुमति देता है:

${\frac {\Gamma \;\vdash \;t:\sigma }{\Gamma \;\vdash \;\Lambda \alpha .t:\Pi \alpha .\sigma }}\;{\text{ if }}\alpha {\text{ does not occur free in }}\Gamma$

$\Lambda$ से प्रारंभ होने वाले शब्द $\Lambda$ इन्हें पैरामीट्रिक बहुरूपता कहा जाता है, क्योंकि इस प्रकार इन्हें विभिन्न कार्यों को प्राप्त करने के लिए विभिन्न प्रकारों पर लागू किया जा सकता है, जो एमएल (प्रोग्रामिंग भाषा) या एमएल जैसी भाषाओं में बहुरूपी कार्यों के समान हैं। उदाहरण के लिए बहुरूपी पहचान इस प्रकार हैं-

fun x -> x

OCaml इसका प्रकार है

'a -> 'a

इसका अर्थ यह हैं कि 'a किसी भी प्रकार का तर्क ले सकता है, और उस प्रकार का तत्व रिटर्न भी कर सकता हैं। यह प्रकार λ2 में $\Pi \alpha .\alpha \to \alpha$ . प्रकार से मेल खाता है।

(λω) सिस्टम Fω

सिस्टम एफ में ${\underline {\omega }}$ के निर्माण की आपूर्ति से जुड़े प्रकारों के लिए प्रस्तुत किया जाता है, जो इस प्रकार अन्य प्रकारों पर निर्भर होते हैं। इसे कंस्ट्रक्टर टाइप कहा जाता है, और वैल्यू प्रकार के साथ फ़ंक्शन बनाने का तरीका प्रदान करता है।^[3] इस प्रकार के कंस्ट्रक्टर का उदाहरण बाइनरी ट्री का प्रकार है, जिसमें किसी दिए गए $A$ प्रकार के डेटा द्वारा लेबल किए गए पत्ते होते हैं: ${\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B$ , जहाँ $A:*$ का अनौपचारिक रूप से अर्थ है, जो $A$ प्रकार के है, यह इस प्रकार ऐसा फ़ंक्शन है जो $A$ प्रकार का पैरामीटर लेता है, तथा तार्किक रूप में और इसे ${\mathsf {TREE}}$ प्रकार से लौटाता है, इस प्रकार के मानों का s $A$ में प्रयोग किया जाता हैं। इस प्रोग्रामिंग में यह सुविधा टाइप कंस्ट्रक्टरों को उपयोगी मानने के अतिरिक्त भाषा के अंदर परिभाषित करने की क्षमता से मेल खाती है। जिसके लिए इस प्रकार पिछले प्रकार वाले कंस्ट्रक्टर को मुख्य रूप से OCaml में लेबल वाली पत्तियों वाले पेड़ की निम्नलिखित परिभाषा से मेल खाता है:

type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree

इस प्रकार के नए प्रकारों को प्राप्त करने के लिए इस प्रकार के कंस्ट्रक्टर को अन्य प्रकारों पर लागू किया जा सकता है। उदाहरण के लिए, पूर्णांकों के वृक्षों के प्रकार प्राप्त करने के लिए हैं:

type int_tree = int tree

इस सिस्टम को एफ ${\underline {\omega }}$ के अनुसार सामान्य रूप से उपयोग करके अपने आप नहीं किया जाता है, अपितु इस प्रकार यह टाइप कंस्ट्रक्टर की स्वतंत्र सुविधा को अलग करने के लिए उपयोगी है।^[4]

(λP) लैम्ब्डा-पी

ΛΠ-कैलकुलस या λP प्रणाली में, जिसे ΛΠ भी कहा जाता है, और तार्किक रूप से उपयोग किये जाने वाले फ्रेमवर्क के लिए LF की निकटता से संबंधित है, तथाकथित रूप से यह इस प्रकार का आश्रित प्रकार है। ये ऐसे प्रकार हैं, जिन्हें शर्तों पर निर्भर रहने की अनुमति देता है। इस सिस्टम का महत्वपूर्ण परिचय नियम इस प्रकार है-

${\frac {\Gamma ,x:A\;\vdash \;B:*}{\Gamma \;\vdash \;(\Pi x:A.B):*}}$

जहाँ $*$ वैध प्रकार का प्रतिनिधित्व करता है। इस प्रकार नए प्रकार के कंस्ट्रक्टर $\Pi$ करी हावर्ड समरूपता के माध्यम से सार्वभौमिक क्वांटिफायर से मेल खाता है, और सिस्टम λP समग्र रूप से केवल संयोजी के रूप में निहितार्थ के साथ प्रथम-क्रम तर्क से मेल खाता है। इस प्रकार प्रोग्रामिंग में इन आश्रित प्रकारों का उदाहरण निश्चित लंबाई पर वैक्टर का प्रकार है, जहाँ लंबाई शब्द है, जो इसके प्रकार पर निर्भर करता है।

(Fω) सिस्टम Fω

सिस्टम एफ-ओमेगा|सिस्टम एफω दोनों को जोड़ता है, जहाँ पर $\Lambda$ सिस्टम F का कंस्ट्रक्टर और सिस्टम F से टाइप कंस्ट्रक्टर ${\underline {\omega }}$ हैं। इस प्रकार सिस्टम Fω दोनों शब्द प्रदान करता है, जो इसके प्रकारों पर निर्भर करते हैं, और प्रकार जो प्रकारों पर निर्भर करते हैं।

(λC) निर्माणों की गणना

निर्माणों की गणना में उपयुक्त घन में λC के रूप में या λPω के रूप में दर्शाया गया है,^[1]^: 130 ये चार विशेषताएं एक साथ उपयोग होती हैं, जिससे ये प्रकार और पद दोनों प्रकार से और उक्त पद पर निर्भर हो सकते हैं। इस प्रकार शब्दों और प्रकारों के बीच λ→ में सम्मिलित स्पष्ट सीमा को कुछ हद तक समाप्त कर दिया गया है, क्योंकि सार्वभौमिक को छोड़कर सभी प्रकार $\square$ स्वयं प्रकार के पद हैं।

औपचारिक परिभाषा

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

इस प्रकार के सेट को $S:=\{*,\square \}$ प्रकार परिभाषित किया गया है, इसके प्रकारों को $s$ अक्षर से दर्शाया जाता है, इसके लिए $V$ वैरियेबल का सेट भी है, जो $x,y,\dots$ . अक्षरों द्वारा दर्शाया गया हैं। इसके घनों की आठ प्रणालियों के मूल शब्द निम्नलिखित वाक्यविन्यास द्वारा दिए गए हैं:

$A:=x\mid s\mid A~A\mid \lambda x:A.A\mid \Pi x:A.A$

और $A\to B$ दर्शाने के लिए $\Pi x:A.B$ जहाँ पर $B$ , $x$ में मुक्त नहीं होता है।

इस इंन्वायरमेंट में सामान्यतः टाइप की गई प्रणालियों में होता है, जिसे $\Gamma :=\emptyset \mid \Gamma ,x:T$ द्वारा उपयोग किया जाता है। क्यूब में सभी प्रणालियों के लिए β-कमी की धारणा साधारण है। जिसे $\to _{\beta }$ द्वारा लिखा जाता है, और इसे नियमानुसार दिया जाता है-

{\frac {}{(\lambda x:A.B)~C\to _{\beta }B[C/x]}}

{\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}

{\frac {A\to _{\beta }A'}{\lambda x:A.B\to _{\beta }\lambda x:A'.B}}

{\frac {B\to _{\beta }B'}{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}

{\frac {A\to _{\beta }A'}{\Pi x:A.B\to _{\beta }\Pi x:A'.B}}

इसका रिफ्लेक्सिव ट्रांजिटिव क्लोजर या रिफ्लेक्सिव, ट्रांजिटिव क्लोजर $=_{\beta }$ लिखा है।

निम्नलिखित टाइपिंग नियम भी क्यूब की सभी प्रणालियों के लिए सामान्य हैं:

{\frac {}{\vdash *:\square }}\quad {\text{(Axiom)}}

{\frac {\Gamma \vdash A:s\quad x{\text{ does not occur in }}\Gamma }{\Gamma ,x:A\vdash x:A}}\quad {\text{(Start)}}

{\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}\quad {\text{(Weakening)}}

{\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[a/x]}}\quad {\text{(Application)}}

{\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(Conversion)}}

प्रणालियों के बीच अंतर प्रकार

{\textstyle (s_{1},s_{2})}

के जोड़े में है, इसे निम्नलिखित दो टाइपिंग नियमों में इसकी अनुमति किया जाता है:

{\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \Pi x:A.B:s_{2}}}\quad {\text{(Product)}}

{\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash b:B\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(Abstraction)}}

सिस्टम और जोड़ियों के बीच पत्राचार

{\textstyle (s_{1},s_{2})}

नियमों में निम्नलिखित की अनुमति है:

$(s_{1},s_{2})$	$(,)$	$(*,\square )$	$(\square ,*)$	$(\square ,\square )$
λ→
λP
λ2
λω
λP2
λPω
λω
λC

घन की प्रत्येक दिशा जोड़ी (जोड़ी को छोड़कर) से मेल खाती है, इस प्रकार ${\textstyle (*,*)}$ सभी प्रणालियों द्वारा साझा किया जाता है, और इसके अतिरिक्त प्रत्येक जोड़ी शब्दों और प्रकारों के बीच निर्भरता की संभावना से मेल खाती है:

${\textstyle (*,*)}$ शर्तों को शर्तों पर निर्भर रहने की अनुमति देता है।
${\textstyle (*,\square )}$ प्रकारों को शर्तों पर निर्भर करने की अनुमति देता है।
${\textstyle (\square ,*)}$ शर्तों को प्रकारों पर निर्भर करने की अनुमति देता है।
${\textstyle (\square ,\square )}$ प्रकारों को प्रकारों पर निर्भर रहने की अनुमति देता है।

प्रणालियों के बीच तुलना

λ→

विशिष्ट व्युत्पत्ति जो प्राप्त की जा सकती है वह है

\alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha

या तीर शॉर्टकट के साथ

\alpha :*\vdash \lambda x:\alpha .x:\alpha \to \alpha

इकसा पहचान करने से अत्यधिक मिलते-जुलते प्रकार का

{\textstyle \alpha }

) सामान्य λ→ का हैं। यहाँ पर ध्यान दें कि उपयोग किए गए सभी प्रकार संदर्भ में दिखाई देने चाहिए, क्योंकि एकमात्र व्युत्पत्ति जो खाली संदर्भ

{\textstyle \vdash *:\square }

. में व्यक्त की जा सकती है।

कंप्यूटिंग शक्ति बहुत कमजोर है, यह विस्तारित बहुपद सशर्त ऑपरेटर के साथ बहुपद से मेल खाती है।^[5]

λ2

λ2 में, ऐसे पद प्राप्त किए जा सकते हैं

\vdash (\lambda \beta :*.\lambda x:\bot .x\beta ):\Pi \beta :*.\bot \to \beta

{\textstyle \bot =\Pi \alpha :*.\alpha }

के साथ यदि कोई

{\textstyle \Pi }

पढ़ता है, तो सार्वभौमिक परिमाणीकरण के रूप में, करी-हावर्ड समरूपता के माध्यम से, इसे विस्फोट के सिद्धांत के प्रमाण के रूप में देखा जा सकता है। सामान्य तौर पर, λ2 में असंभाव्यता प्रकार जैसे होने की संभावना

{\textstyle \bot }

से जुड़ती है, यह स्वयं सहित सभी प्रकारों पर मात्रा निर्धारित करने वाला शब्द है।
इसकी बहुरूपता उन कार्यों के निर्माण की भी अनुमति देती है, जो λ→ में निर्माण योग्य नहीं थे। इसके अधिक सटीक रूप से λ2 में परिभाषित कार्य दूसरे क्रम के पीनो अंकगणित में सिद्ध रूप से कुल हैं।^[6] विशेष रूप से, सभी आदिम पुनरावर्ती कार्य निश्चित हैं।

λP

λP में, शब्दों के आधार पर प्रकार रखने की क्षमता का मतलब है कि कोई तार्किक विधेय व्यक्त कर सकता है। उदाहरण के लिए, निम्नलिखित व्युत्पन्न है:

\alpha :*,a_{0}:\alpha ,p:\alpha \to *,q:*\vdash \lambda z:(\Pi x:\alpha .px\to q).\lambda y:(\Pi x:\alpha .px).(za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to (\Pi x:\alpha .px)\to q

जो करी-हावर्ड समरूपता के माध्यम से इसके प्रमाण

(\forall x:A,Px\to Q)\to (\forall x:A,Px)\to Q

से मेल खाता है,
कम्प्यूटेशनल दृष्टिकोण से आश्रित प्रकार होने से कम्प्यूटेशनल शक्ति में वृद्धि नहीं होती है, केवल अधिक सटीक प्रकार के गुणों को व्यक्त करने की संभावना होती है।^[7]आश्रित प्रकारों से निपटने के समय रूपांतरण नियम की अत्यधिक आवश्यकता होती है, क्योंकि यह प्रकार की शर्तों पर गणना करने की अनुमति देता है। उदाहरण के लिए, यदि आपके पास है

\Gamma \vdash A:P((\lambda x.x)y)

और

\Gamma \vdash B:\Pi x:P(y).C

, प्राप्त करने के लिए आपको रूपांतरण नियम लागू करना होगा, जिसे

\Gamma \vdash A:P(y)

टाइप करने में सक्षम होने के लिए

\Gamma \vdash BA:C

द्वारा उपयोग किया जाता हैं।

एल

एलō में, निम्नलिखित ऑपरेटर

AND:=\lambda \alpha :*.\lambda \beta :*.\Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma

निश्चित है, अर्थात्

\vdash AND:*\to *\to *

इसकी व्युत्पत्ति हैं।

\alpha :*,\beta :*\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*

इसके पहले से ही λ2 में प्राप्त किया जा सकता है, चूंकि बहुरूपी

{\textstyle AND}

केवल तभी परिभाषित किया जा सकता है, जब नियम

{\textstyle (\square ,*)}

भी सम्मिलित है।

कंप्यूटिंग के दृष्टिकोण से, λω बेहद शक्तिशाली है, और इसे प्रोग्रामिंग भाषाओं के लिए आधार माना गया है।^[8]

λC

निर्माणों की गणना में λP की विधेय अभिव्यंजना और λω की कम्प्यूटेशनल शक्ति दोनों हैं, इसलिए λC को λPω भी कहा जाता है,^[1]^: 130 इसलिए यह तार्किक पक्ष और कम्प्यूटेशनल पक्ष दोनों पर बहुत शक्तिशाली है।

अन्य प्रणालियों से संबंध

सिस्टम स्वचालित तार्किक दृष्टिकोण से λ2 के समान है। एमएल (प्रोग्रामिंग भाषा) या एमएल जैसी भाषाएं, टाइपिंग के दृष्टिकोण से, λ→ और λ2 के बीच कहीं स्थित होती हैं, क्योंकि वे प्रतिबंधित प्रकार के बहुरूपी प्रकारों को स्वीकार करते हैं, जो कि प्रीनेक्स सामान्य रूप में प्रकार हैं। चूंकि, क्योंकि उनमें कुछ रिकर्सन ऑपरेटर होते हैं, उनकी कंप्यूटिंग शक्ति λ2 से अधिक होती है।^[7] इस प्रकार Coq प्रणाली केवल अप्राप्य के अतिरिक्त ब्रह्मांडों के रैखिक पदानुक्रम के साथ λC के विस्तार ${\textstyle \square }$ पर आधारित है, और आगमनात्मक प्रकार के निर्माण की क्षमता प्राप्त करता हैं।

इसके शुद्ध प्रकार की प्रणालियों को घन के सामान्यीकरण के रूप में देखा जा सकता है, जिसमें प्रकार को स्वयंसिद्ध, उत्पाद और अमूर्त नियमों के द्वारा सेट किया जाता है। इसके विपरीत, लैम्ब्डा क्यूब के सिस्टम को दो प्रकार के शुद्ध प्रकार के सिस्टम के रूप में व्यक्त किया जा सकता है, इसके लिए $\{*,\square \}$ , एकमात्र स्वयंसिद्ध ${\textstyle \{*,\square \}}$ , और नियमों का सेट ${\textstyle R}$ के लिए इस प्रकार हैं कि $\{(*,*,*)\}\subseteq R\subseteq \{(*,*,*),(*,\square ,\square ),(\square ,*,*),(\square ,\square ,\square )\}$ .^[1]

करी-हावर्ड समरूपता के माध्यम से, लैम्ब्डा क्यूब और तार्किक प्रणालियों में सिस्टम के बीच एक-से-एक पत्राचार होता है,^[1] अर्थात्:

घन की प्रणाली	तार्किक प्रणाली
λ→	(प्रथम-क्रम) प्रस्तावात्मक कलन
λ2	दूसरे क्रम का प्रस्तावात्मक कैलकुलस
λω	कमज़ोर उच्च क्रम प्रस्तावक कलन
λω	उच्च क्रम प्रस्ताव कलन
λP	(प्रथम क्रम) विधेय तर्क
λP2	दूसरे क्रम का विधेय कलन
λPω	कमज़ोर उच्चतर क्रम विधेय कलन
λC	निर्माणों की गणना

सभी तर्क निहितार्थ हैं, अर्थात केवल संयोजक हैं ${\textstyle \to }$ और ${\textstyle \forall }$ के रूप में प्रदर्शित होते हैं, चूंकि कोई अन्य संयोजकों को परिभाषित कर सकता है, जैसे कि $\wedge$ या $\neg$ दूसरे और उच्च क्रम के तर्कों में अव्यवहारिक तरीके से व्यक्त किये जाते हैं। इस प्रकार कमजोर उच्च क्रम तार्किकी में उच्च क्रम विधेय के लिए चर होते हैं, अपितु उन पर कोई परिमाणीकरण नहीं किया जा सकता है।

सामान्य गुण

क्यूब के सभी प्रणालियो का उपोयग करते हैं

चर्च-रोसेर संपत्ति: यदि $M\to _{\beta }N$ और $M\to _{\beta }N'$ तो वहाँ अस्तित्व है $N''$ ऐसा है कि $N\to _{\beta }^{*}N''$ और $N'\to _{\beta }^{*}N''$ ;
विषय में कमी: यदि $\Gamma \vdash M:T$ और $M\to _{\beta }M'$ तब $\Gamma \vdash M':T$ ;
प्रकारों की विशिष्टता: यदि $\Gamma \vdash A:B$ और $\Gamma \vdash A:B'$ तब $B=_{\beta }B'$ .

ये सभी सामान्य शुद्ध प्रकार की प्रणालियों पर सिद्ध किए जा सकते हैं।^[9] क्यूब की प्रणाली में अच्छी तरह से टाइप किया गया कोई भी शब्द दृढ़ता से सामान्यीकरण कर रहा है,^[1] चूंकि यह गुण सभी शुद्ध प्रकार की प्रणालियों के लिए सामान्य नहीं है। क्यूब में कोई भी सिस्टम ट्यूरिंग पूर्ण नहीं है।^[7]

उपप्रकार

चूंकि, सबटाइपिंग को क्यूब में प्रदर्शित नहीं किया जाता है, इसके आधार पर $F_{<:}^{\omega }$ भले ही सिस्टम पसंद करता हो, जिसे उच्च-क्रम सीमाबद्ध परिमाणीकरण के रूप में जाना जाता है, जो उपप्रकार और बहुरूपता को जोड़ता है, व्यावहारिक रुचि का है, और इसे आगे बंधे हुए प्रकार के ऑपरेटरों के लिए सामान्यीकृत किया जा सकता है। आगे विस्तार $F_{<:}^{\omega }$ विशुद्ध रूप से कार्यात्मक वस्तुओं की परिभाषा की अनुमति दें; ये सिस्टम सामान्यतः लैम्ब्डा क्यूब पेपर प्रकाशित होने के बाद विकसित किए गए थे।^[10]

क्यूब का विचार गणितज्ञ हेन्क बेरेन्ड्रेट (1991) की देन है। शुद्ध प्रकार की प्रणालियों का ढांचा लैम्ब्डा क्यूब को इस अर्थ में सामान्यीकृत करता है कि क्यूब के सभी कोनों, साथ ही कई अन्य प्रणालियों को इस सामान्य ढांचे के उदाहरण के रूप में दर्शाया जा सकता है।^[11] यह प्रारूप लैम्ब्डा क्यूब से कुछ साल पहले का है। अपने 1991 के पेपर में, बेरेन्ड्रेट ने इस ढांचे में घन के कोनों को भी परिभाषित किया है।

यह भी देखें

अनुसंधान को निर्देशित करने की उनकी क्षमता में,^[12] ओलिवियर रिडौक्स लैम्ब्डा क्यूब का कट-आउट टेम्प्लेट देता है और क्यूब का ऑक्टाहेड्रोन के रूप में दोहरा प्रतिनिधित्व भी देता है, जहां 8 शीर्षों को चेहरों द्वारा प्रतिस्थापित किया जाता है, साथ ही डोडेकाहेड्रोन के रूप में दोहरा प्रतिनिधित्व दिया जाता है, जहां 12 किनारों को परिवर्तित कर दिया जाता है।
होमोटोपी प्रकार सिद्धांत

↑ ^1.0 ^1.1 ^1.2 ^1.3 ^1.4 ^1.5 Barendregt, Henk (1991). "सामान्यीकृत प्रकार की प्रणालियों का परिचय". Journal of Functional Programming. 1 (2): 125–154. doi:10.1017/s0956796800020025. hdl:2066/17240. ISSN 0956-7968. S2CID 44757552.
↑ Nederpelt, Rob; Geuvers, Herman (2014). प्रकार सिद्धांत और औपचारिक प्रमाण. Cambridge University Press. p. 69. ISBN 9781107036505.
↑ Nederpelt & Geuvers 2014, p. 85
↑ Nederpelt & Geuvers 2014, p. 100
↑ Schwichtenberg, Helmut (1975). "Definierbare Funktionen imλ-Kalkül mit Typen". Archiv für Mathematische Logik und Grundlagenforschung (in Deutsch). 17 (3–4): 113–114. doi:10.1007/bf02276799. ISSN 0933-5846. S2CID 11598130.
↑ Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). प्रमाण एवं प्रकार. Cambridge Tracts in Theoretical Computer Science. Vol. 7. Cambridge University Press. ISBN 9780521371810.
↑ ^7.0 ^7.1 ^7.2 Ridoux, Olivier (1998). Lambda-Prolog de A à Z ... ou presque (PDF). [s.n.] OCLC 494473554.
↑ Pierce, Benjamin; Dietzen, Scott; Michaylov, Spiro (1989). उच्च-क्रम टाइप किए गए लैम्ब्डा-कैलकुली में प्रोग्रामिंग. Computer Science Department, Carnegie Mellon University. OCLC 20442222. CMU-CS-89-111 ERGO-89-075.
↑ Sørensen, Morten Heine; Urzyczyin, Pawel (2006). "Pure type systems and the λ-cube". करी-हावर्ड समरूपता पर व्याख्यान. Elsevier. pp. 343–359. doi:10.1016/s0049-237x(06)80015-7. ISBN 9780444520777.
↑ Pierce, Benjamin (2002). प्रकार और प्रोग्रामिंग भाषाएँ. MIT Press. pp. 467–490. ISBN 978-0262162098. OCLC 300712077.
↑ Pierce 2002, p. 466
↑ Ridoux 1998, p. 70

अग्रिम पठन

Peyton Jones, Simon; Meijer, Erik (1997). "Henk: A Typed Intermediate Language" (PDF). Microsoft. Henk is based directly on the lambda cube, an expressive family of typed lambda calculi.

बाहरी संबंध

Barendregt's Lambda Cube in the context of pure type systems by Roger Bishop Jones

[:0-1] 1.0 ^1.1 ^1.2 ^1.3 ^1.4 ^1.5 Barendregt, Henk (1991). "सामान्यीकृत प्रकार की प्रणालियों का परिचय". Journal of Functional Programming. 1 (2): 125–154. doi:10.1017/s0956796800020025. hdl:2066/17240. ISSN 0956-7968. S2CID 44757552.

[2] Nederpelt, Rob; Geuvers, Herman (2014). प्रकार सिद्धांत और औपचारिक प्रमाण. Cambridge University Press. p. 69. ISBN 9781107036505.

[3] Nederpelt & Geuvers 2014, p. 85

[4] Nederpelt & Geuvers 2014, p. 100

[5] Schwichtenberg, Helmut (1975). "Definierbare Funktionen imλ-Kalkül mit Typen". Archiv für Mathematische Logik und Grundlagenforschung (in Deutsch). 17 (3–4): 113–114. doi:10.1007/bf02276799. ISSN 0933-5846. S2CID 11598130.

[6] Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). प्रमाण एवं प्रकार. Cambridge Tracts in Theoretical Computer Science. Vol. 7. Cambridge University Press. ISBN 9780521371810.

[:1-7] 7.0 ^7.1 ^7.2 Ridoux, Olivier (1998). Lambda-Prolog de A à Z ... ou presque (PDF). [s.n.] OCLC 494473554.

[8] Pierce, Benjamin; Dietzen, Scott; Michaylov, Spiro (1989). उच्च-क्रम टाइप किए गए लैम्ब्डा-कैलकुली में प्रोग्रामिंग. Computer Science Department, Carnegie Mellon University. OCLC 20442222. CMU-CS-89-111 ERGO-89-075.

[9] Sørensen, Morten Heine; Urzyczyin, Pawel (2006). "Pure type systems and the λ-cube". करी-हावर्ड समरूपता पर व्याख्यान. Elsevier. pp. 343–359. doi:10.1016/s0049-237x(06)80015-7. ISBN 9780444520777.

[10] Pierce, Benjamin (2002). प्रकार और प्रोग्रामिंग भाषाएँ. MIT Press. pp. 467–490. ISBN 978-0262162098. OCLC 300712077.

[11] Pierce 2002, p. 466

[12] Ridoux 1998, p. 70

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

@@ Line 1: / Line 1: @@
-{{Cleanup rewrite|article uses pervasively inconsistent, confusing and misleading terminology for basic concepts fundamental to the understanding of the article's subject||date=September 2020}}
+[[File:Lambda_Cube_img.svg|alt=|frame|लैम्ब्डा क्यूब. प्रत्येक तीर की दिशा समावेशन की दिशा है।]][[गणितीय तर्क]] और [[प्रकार सिद्धांत]] में λ-क्यूब जिसे '''लैम्ब्डा क्यूब''' भी लिखा जाता है, मुख्य रूप से यह [[हेन्क बेरेन्ड्रेट]] द्वारा प्रस्तुत रूपरेखा है।<ref name=":0">{{Cite journal|last=Barendregt|first=Henk|date=1991|title=सामान्यीकृत प्रकार की प्रणालियों का परिचय|journal=Journal of Functional Programming|volume=1|issue=2|pages=125–154|doi=10.1017/s0956796800020025|issn=0956-7968|hdl=2066/17240|s2cid=44757552 |hdl-access=free}}</ref> इस प्रकार विभिन्न आयामों की जांच करने के लिए जिसमें [[निर्माणों की गणना]] सरल रूप से टाइप किए जाने वाले λ-कैलकुलस का सामान्यीकरण है। इसके आधार पर इस घन का प्रत्येक आयामों पर प्राप्त होने वाले शब्दों और प्रकारों के बीच नए प्रकार की निर्भरता से मेल खाता है। यहाँ पर इस निर्भरता से तात्पर्य किसी शब्द या प्रकार के मुक्त वैरियेबल और किसी शब्द या प्रकार से बंधे वैरियेबल की क्षमता से है। इस प्रकार λ-घन के संबंधित आयाम इसके अनुरूप हैं:
-[[File:Lambda_Cube_img.svg|alt=|frame|लैम्ब्डा क्यूब. प्रत्येक तीर की दिशा समावेशन की दिशा है।]][[गणितीय तर्क]] और [[प्रकार सिद्धांत]] में, λ-क्यूब (जिसे लैम्ब्डा क्यूब भी लिखा जाता है) [[हेन्क बेरेन्ड्रेट]] द्वारा प्रस्तुत एक रूपरेखा है।<ref name=":0">{{Cite journal|last=Barendregt|first=Henk|date=1991|title=सामान्यीकृत प्रकार की प्रणालियों का परिचय|journal=Journal of Functional Programming|volume=1|issue=2|pages=125–154|doi=10.1017/s0956796800020025|issn=0956-7968|hdl=2066/17240|s2cid=44757552 |hdl-access=free}}</ref> विभिन्न आयामों की जांच करने के लिए जिसमें [[निर्माणों की गणना]] सरल रूप से टाइप किए गए λ-कैलकुलस का सामान्यीकरण है। घन का प्रत्येक आयाम शब्दों और प्रकारों के बीच एक नई प्रकार की निर्भरता से मेल खाता है। यहां, निर्भरता से तात्पर्य किसी शब्द या प्रकार की मुक्त चर और किसी शब्द या प्रकार से बंधे चर की क्षमता से है। λ-घन के संबंधित आयाम इसके अनुरूप हैं:
+* x-अक्ष (<math>\rightarrow</math>): ऐसे प्रकार जो [[आश्रित प्रकार]] के अनुरूप शब्दों को बांध सकते हैं।
-* एक्स-अक्ष (<math>\rightarrow</math>): ऐसे प्रकार जो [[आश्रित प्रकार]]ों के अनुरूप शब्दों को बांध सकते हैं।
 * y-अक्ष (<math>\uparrow</math>): वे शब्द जो [[पैरामीट्रिक बहुरूपता]] के अनुरूप प्रकारों को बांध सकते हैं।
-* z-अक्ष (<math>\nearrow</math>): ऐसे प्रकार जो (बाध्यकारी) प्रकार ऑपरेटरों के अनुरूप प्रकारों को बांध सकते हैं।
+* z-अक्ष (<math>\nearrow</math>): ऐसे प्रकार जो बाध्यकारी प्रकार के ऑपरेटरों के अनुरूप प्रकारों को बांध सकते हैं।
-इन तीन आयामों को संयोजित करने के विभिन्न तरीकों से घन के 8 शीर्ष प्राप्त होते हैं, जिनमें से प्रत्येक एक अलग प्रकार की टाइप की गई प्रणाली के अनुरूप होता है। λ-क्यूब को [[शुद्ध प्रकार की प्रणाली]] की अवधारणा में सामान्यीकृत किया जा सकता है।
+इन तीन आयामों को संयोजित करने के विभिन्न तरीकों से घन के 8 शीर्ष प्राप्त होते हैं, जिनमें इस प्रकार से प्रत्येक अलग प्रकार की टाइप की गई प्रणाली के अनुरूप होता है। इस प्रकार λ-क्यूब को [[शुद्ध प्रकार की प्रणाली]] की अवधारणा में सामान्यीकृत किया जा सकता है।
 == सिस्टम के उदाहरण ==
-=== (λ→) [[बस लैम्ब्डा कैलकुलस टाइप किया गया]] ===
+=== (λ→) [[बस लैम्ब्डा कैलकुलस टाइप किया गया|बस लैम्ब्डा कैलकुलस टाइप किया गया हैं।]] ===
-λ-क्यूब में पाई जाने वाली सबसे सरल प्रणाली सरल रूप से टाइप किया गया लैम्ब्डा कैलकुलस है, जिसे λ→ भी कहा जाता है। इस प्रणाली में, एक अमूर्तता का निर्माण करने का एकमात्र तरीका [[टाइपिंग नियम]] के साथ, एक शब्द को एक शब्द पर निर्भर बनाना है
+λ-क्यूब में पाई जाने वाली सबसे सरल प्रणाली सरल रूप से टाइप किया गया लैम्ब्डा कैलकुलस है, जिसे इस प्रकार λ→ भी कहा जाता है। इस प्रणाली में इसका निर्माण करने का एकमात्र तरीका [[टाइपिंग नियम]] के साथ उपयोग किए जाने वाले शब्द को इसके उपयोगी शब्दों के लिए निर्भर बनाना है-
 <math>\frac{\Gamma, x : \sigma \;\vdash\; t : \tau}{\Gamma \;\vdash\; \lambda x . t : \sigma \to \tau}</math>
 === (λ2) [[सिस्टम एफ]] ===
-सिस्टम एफ में (दूसरे क्रम में टाइप किए गए लैम्ब्डा कैलकुलस के लिए इसे λ2 भी कहा जाता है)<ref>{{cite book |last1=Nederpelt |first1=Rob |last2=Geuvers |first2=Herman |title=प्रकार सिद्धांत और औपचारिक प्रमाण|date=2014 |publisher=Cambridge University Press |isbn=9781107036505 |page=69 |url=https://www.cambridge.org/vi/academic/subjects/computer-science/programming-languages-and-applied-logic/type-theory-and-formal-proof-introduction?format=HB }}</ref> एक अन्य प्रकार का अमूर्तन है, जिसे ए के साथ लिखा जाता है <math>\Lambda</math>, जो निम्नलिखित नियम के साथ शब्दों को प्रकारों पर निर्भर करने की अनुमति देता है:
+सिस्टम एफ को दूसरे क्रम में टाइप किए गए लैम्ब्डा कैलकुलस के लिए इसे λ2 भी कहा जाता है,<ref>{{cite book |last1=Nederpelt |first1=Rob |last2=Geuvers |first2=Herman |title=प्रकार सिद्धांत और औपचारिक प्रमाण|date=2014 |publisher=Cambridge University Press |isbn=9781107036505 |page=69 |url=https://www.cambridge.org/vi/academic/subjects/computer-science/programming-languages-and-applied-logic/type-theory-and-formal-proof-introduction?format=HB }}</ref> इसके लिए अन्य प्रकार का अमूर्त मान इस प्रकार हैं कि इसे ए (<math>\Lambda</math>) के साथ लिखा जाता है, जो निम्नलिखित नियम के साथ शब्दों को प्रकारों पर निर्भर करने की अनुमति देता है:
 <math>\frac{\Gamma \;\vdash\; t : \sigma}{\Gamma \;\vdash\; \Lambda \alpha . t : \Pi \alpha . \sigma} \;\text{ if } \alpha\text{ does not occur free in }\Gamma</math>
-ए से शुरू होने वाले शब्द <math>\Lambda</math> इन्हें पैरामीट्रिक बहुरूपता कहा जाता है, क्योंकि इन्हें विभिन्न कार्यों को प्राप्त करने के लिए विभिन्न प्रकारों पर लागू किया जा सकता है, [[एमएल (प्रोग्रामिंग भाषा)]] | एमएल जैसी भाषाओं में बहुरूपी कार्यों के समान। उदाहरण के लिए, बहुरूपी पहचान <syntaxhighlight lang="ocaml">
+<math>\Lambda</math> से प्रारंभ होने वाले शब्द <math>\Lambda</math> इन्हें पैरामीट्रिक बहुरूपता कहा जाता है, क्योंकि इस प्रकार इन्हें विभिन्न कार्यों को प्राप्त करने के लिए विभिन्न प्रकारों पर लागू किया जा सकता है, जो [[एमएल (प्रोग्रामिंग भाषा)]] या एमएल जैसी भाषाओं में बहुरूपी कार्यों के समान हैं। उदाहरण के लिए बहुरूपी पहचान इस प्रकार हैं- <syntaxhighlight lang="ocaml">
 fun x -> x
-</syntaxhighlight>[[OCaml]] का प्रकार है <syntaxhighlight lang="ocaml">
+</syntaxhighlight>[[OCaml]] इसका प्रकार है <syntaxhighlight lang="ocaml">
 'a -> 'a
-</syntaxhighlight>मतलब यह किसी भी प्रकार का तर्क ले सकता है <code>'a</code> और उस प्रकार का एक तत्व लौटाएँ। यह प्रकार λ2 में प्रकार से मेल खाता है <math>\Pi \alpha . \alpha \to \alpha</math>.
+</syntaxhighlight>इसका अर्थ यह हैं कि <code>'a</code>  किसी भी प्रकार का तर्क ले सकता है, और उस प्रकार का तत्व रिटर्न भी कर सकता हैं। यह प्रकार λ2 में  <math>\Pi \alpha . \alpha \to \alpha</math>. प्रकार से मेल खाता है।
 === (λ<u>ω</u>) सिस्टम F<u>ω</u> ===
-सिस्टम एफ में<math>\underline{\omega}</math> एक निर्माण को आपूर्ति प्रकारों के लिए पेश किया जाता है जो अन्य प्रकारों पर निर्भर होते हैं। इसे [[कंस्ट्रक्टर टाइप करें]] कहा जाता है और ''वैल्यू'' प्रकार के साथ फ़ंक्शन बनाने का एक तरीका प्रदान करता है।<ref>{{harvnb|Nederpelt|Geuvers|2014|p=85}}</ref> इस प्रकार के कंस्ट्रक्टर का एक उदाहरण बाइनरी पेड़ों का प्रकार है जिसमें किसी दिए गए प्रकार के डेटा द्वारा लेबल किए गए पत्ते होते हैं <math>A</math>: <math>\mathsf{TREE} := \lambda A : * . \Pi B . (A \to B) \to (B \to B \to B) \to B</math>, कहाँ<math>A:*</math>अनौपचारिक रूप से मतलब है<math>A</math> एक प्रकार है. यह एक फ़ंक्शन है जो एक प्रकार का पैरामीटर लेता है <math>A</math> एक तर्क के रूप में और का प्रकार लौटाता है <math>\mathsf{TREE}</math>प्रकार के मानों का s <math>A</math>. In concrete programming, this feature corresponds to the ability to define type constructors inside the language, rather than considering them as primitives. The previous type constructor roughly corresponds to the following definition of a tree with labeled leaves in OCaml:<syntaxhighlight lang="ocaml">
+सिस्टम एफ में <math>\underline{\omega}</math> के निर्माण की आपूर्ति से जुड़े प्रकारों के लिए प्रस्तुत किया जाता है, जो इस प्रकार अन्य प्रकारों पर निर्भर होते हैं। इसे [[कंस्ट्रक्टर टाइप करें|कंस्ट्रक्टर टाइप कहा]] जाता है, और ''वैल्यू'' प्रकार के साथ फ़ंक्शन बनाने का तरीका प्रदान करता है।<ref>{{harvnb|Nederpelt|Geuvers|2014|p=85}}</ref> इस प्रकार के कंस्ट्रक्टर का उदाहरण बाइनरी ट्री का प्रकार है, जिसमें किसी दिए गए <math>A</math> प्रकार के डेटा द्वारा लेबल किए गए पत्ते होते हैं: <math>\mathsf{TREE} := \lambda A : * . \Pi B . (A \to B) \to (B \to B \to B) \to B</math>, जहाँ<math>A:*</math> का अनौपचारिक रूप से अर्थ है, जो <math>A</math> प्रकार के है, यह इस प्रकार ऐसा फ़ंक्शन है जो <math>A</math> प्रकार का पैरामीटर लेता है, तथा तार्किक रूप में और इसे <math>\mathsf{TREE}</math> प्रकार से लौटाता है, इस प्रकार के मानों का s <math>A</math> में प्रयोग किया जाता हैं। इस प्रोग्रामिंग में यह सुविधा टाइप कंस्ट्रक्टरों को उपयोगी मानने के अतिरिक्त भाषा के अंदर परिभाषित करने की क्षमता से मेल खाती है। जिसके लिए इस प्रकार पिछले प्रकार वाले कंस्ट्रक्टर को मुख्य रूप से OCaml में लेबल वाली पत्तियों वाले पेड़ की निम्नलिखित परिभाषा से मेल खाता है:<syntaxhighlight lang="ocaml">
 type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree
 </syntaxhighlight>
-नए प्रकार प्राप्त करने के लिए इस प्रकार के कंस्ट्रक्टर को अन्य प्रकारों पर लागू किया जा सकता है। उदाहरण के लिए, पूर्णांकों के वृक्षों के प्रकार प्राप्त करने के लिए:<syntaxhighlight lang="ocaml">type int_tree = int tree</syntaxhighlight>
+इस प्रकार के नए प्रकारों को प्राप्त करने के लिए इस प्रकार के कंस्ट्रक्टर को अन्य प्रकारों पर लागू किया जा सकता है। उदाहरण के लिए, पूर्णांकों के वृक्षों के प्रकार प्राप्त करने के लिए हैं:<syntaxhighlight lang="ocaml">type int_tree = int tree</syntaxhighlight>
-सिस्टम एफ<math>\underline{\omega}</math> आम तौर पर इसका उपयोग अपने आप नहीं किया जाता है, लेकिन यह टाइप कंस्ट्रक्टर की स्वतंत्र सुविधा को अलग करने के लिए उपयोगी है।<ref>{{harvnb|Nederpelt|Geuvers|2014|p=100}}</ref>
+इस सिस्टम को एफ <math>\underline{\omega}</math> के अनुसार सामान्य रूप से उपयोग करके अपने आप नहीं किया जाता है, अपितु इस प्रकार यह टाइप कंस्ट्रक्टर की स्वतंत्र सुविधा को अलग करने के लिए उपयोगी है।<ref>{{harvnb|Nederpelt|Geuvers|2014|p=100}}</ref>
 === (λP) लैम्ब्डा-पी ===
-ΛΠ-कैलकुलस|λP प्रणाली में, जिसे ΛΠ भी कहा जाता है, और लॉजिकल फ्रेमवर्क#LF से निकटता से संबंधित है, एक तथाकथित [[आश्रित प्रकार]] है। ये ऐसे प्रकार हैं जिन्हें शर्तों पर निर्भर रहने की अनुमति है। सिस्टम का महत्वपूर्ण परिचय नियम है
+ΛΠ-कैलकुलस या λP प्रणाली में, जिसे ΛΠ भी कहा जाता है, और तार्किक रूप से उपयोग किये जाने वाले फ्रेमवर्क के लिए LF की निकटता से संबंधित है, तथाकथित रूप से यह इस प्रकार का [[आश्रित प्रकार]] है। ये ऐसे प्रकार हैं, जिन्हें शर्तों पर निर्भर रहने की अनुमति देता है। इस सिस्टम का महत्वपूर्ण परिचय नियम इस प्रकार है-
 <math>\frac{\Gamma, x : A \;\vdash\; B : *}{\Gamma \;\vdash\; (\Pi x : A . B) : *}</math>
-कहाँ <math>*</math> वैध प्रकार का प्रतिनिधित्व करता है। नए प्रकार का कंस्ट्रक्टर <math>\Pi</math> [[करी हावर्ड समरूपता]] के माध्यम से एक सार्वभौमिक क्वांटिफायर से मेल खाता है, और सिस्टम λP समग्र रूप से केवल संयोजी के रूप में निहितार्थ के साथ [[प्रथम-क्रम तर्क]] से मेल खाता है। ठोस प्रोग्रामिंग में इन आश्रित प्रकारों का एक उदाहरण एक निश्चित लंबाई पर वैक्टर का प्रकार है: लंबाई एक शब्द है, जिस पर प्रकार निर्भर करता है।
+जहाँ <math>*</math> वैध प्रकार का प्रतिनिधित्व करता है। इस प्रकार नए प्रकार के कंस्ट्रक्टर <math>\Pi</math> [[करी हावर्ड समरूपता]] के माध्यम से सार्वभौमिक क्वांटिफायर से मेल खाता है, और सिस्टम λP समग्र रूप से केवल संयोजी के रूप में निहितार्थ के साथ [[प्रथम-क्रम तर्क]] से मेल खाता है। इस प्रकार प्रोग्रामिंग में इन आश्रित प्रकारों का उदाहरण निश्चित लंबाई पर वैक्टर का प्रकार है, जहाँ लंबाई शब्द है, जो इसके प्रकार पर निर्भर करता है।
 === (Fω) सिस्टम Fω ===
-सिस्टम एफ-ओमेगा|सिस्टम एफω दोनों को जोड़ता है <math>\Lambda</math> सिस्टम F का कंस्ट्रक्टर और सिस्टम F से टाइप कंस्ट्रक्टर<math>\underline{\omega}</math>. इस प्रकार सिस्टम Fω दोनों शब्द प्रदान करता है जो प्रकारों पर निर्भर करते हैं और प्रकार जो प्रकारों पर निर्भर करते हैं।
+सिस्टम एफ-ओमेगा|सिस्टम एफω दोनों को जोड़ता है, जहाँ पर <math>\Lambda</math> सिस्टम F का कंस्ट्रक्टर और सिस्टम F से टाइप कंस्ट्रक्टर <math>\underline{\omega}</math> हैं। इस प्रकार सिस्टम Fω दोनों शब्द प्रदान करता है, जो इसके प्रकारों पर निर्भर करते हैं, और प्रकार जो प्रकारों पर निर्भर करते हैं।
 === (λC) निर्माणों की गणना ===
-निर्माणों की गणना में, घन में λC के रूप में या λPω के रूप में दर्शाया गया है,<ref name=:0/>{{rp|130}} ये चार विशेषताएं सहवास करती हैं, जिससे प्रकार और पद दोनों प्रकार और पद पर निर्भर हो सकते हैं। शब्दों और प्रकारों के बीच λ→ में मौजूद स्पष्ट सीमा को कुछ हद तक समाप्त कर दिया गया है, क्योंकि सार्वभौमिक को छोड़कर सभी प्रकार <math>\square</math> स्वयं एक प्रकार के पद हैं।
+निर्माणों की गणना में उपयुक्त घन में λC के रूप में या λPω के रूप में दर्शाया गया है,<ref name=:0/>{{rp|130}} ये चार विशेषताएं एक साथ उपयोग होती हैं, जिससे ये प्रकार और पद दोनों प्रकार से और उक्त पद पर निर्भर हो सकते हैं। इस प्रकार शब्दों और प्रकारों के बीच λ→ में सम्मिलित स्पष्ट सीमा को कुछ हद तक समाप्त कर दिया गया है, क्योंकि सार्वभौमिक को छोड़कर सभी प्रकार <math>\square</math> स्वयं प्रकार के पद हैं।
 == औपचारिक परिभाषा ==
-सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित सभी प्रणालियों के लिए, क्यूब में सभी सिस्टम दो चरणों में दिए गए हैं: पहले, कच्चे शब्द, β-कमी की धारणा के साथ, और फिर टाइपिंग नियम जो उन शब्दों को टाइप करने की अनुमति देते हैं।
+सरल रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित सभी प्रणालियों के लिए, क्यूब में सभी सिस्टम दो चरणों में दिए गए हैं: इसके पहले इस प्रकार के शब्द β-कमी की धारणा के साथ और फिर टाइपिंग नियम जो उन शब्दों को टाइप करने की अनुमति देते हैं।
-प्रकार के सेट को इस प्रकार परिभाषित किया गया है <math>S := \{*, \square \}</math>, प्रकार को अक्षर से दर्शाया जाता है <math>s</math>. एक सेट भी है <math>V</math> चरों का, अक्षरों द्वारा दर्शाया गया <math>x,y,\dots</math>. घन की आठ प्रणालियों के मूल शब्द निम्नलिखित वाक्यविन्यास द्वारा दिए गए हैं:
+इस प्रकार के सेट को <math>S := \{*, \square \}</math> प्रकार परिभाषित किया गया है, इसके प्रकारों को <math>s</math> अक्षर से दर्शाया जाता है, इसके लिए <math>V</math> वैरियेबल का सेट भी है, जो <math>x,y,\dots</math>. अक्षरों द्वारा दर्शाया गया हैं। इसके घनों की आठ प्रणालियों के मूल शब्द निम्नलिखित वाक्यविन्यास द्वारा दिए गए हैं:
 <math>A := x \mid s \mid A~A \mid \lambda x : A . A \mid \Pi x : A . A</math>
-और <math>A \to B</math> दर्शाने <math>\Pi x : A . B</math> कब <math>x</math> में मुक्त नहीं होता है <math>B</math>.
-पर्यावरण, जैसा कि आमतौर पर टाइप की गई प्रणालियों में होता है, द्वारा दिया जाता है
+और <math>A \to B</math> दर्शाने के लिए <math>\Pi x : A . B</math> जहाँ पर <math>B</math>, <math>x</math> में मुक्त नहीं होता है।
-<math>\Gamma := \emptyset \mid \Gamma, x : T</math>
-क्यूब में सभी प्रणालियों के लिए β-कमी की धारणा आम है। यह लिखा है <math>\to_{\beta}</math> और नियमानुसार दिया गया है<math display="block">\frac{}{(\lambda x : A . B)~C \to_{\beta} B[C/x]}</math><math display="block">\frac{B \to_{\beta} B'}{\lambda x : A . B \to_{\beta} \lambda x : A . B'}</math><math display="block">\frac{A \to_{\beta} A'}{\lambda x : A . B \to_{\beta} \lambda x : A' . B}</math><math display="block">\frac{B \to_{\beta} B'}{\Pi x : A . B \to_{\beta} \Pi x : A . B'}</math><math display="block">\frac{A \to_{\beta} A'}{\Pi x : A . B \to_{\beta} \Pi x : A' . B}</math>इसका रिफ्लेक्सिव ट्रांजिटिव क्लोजर|रिफ्लेक्सिव, ट्रांजिटिव क्लोजर लिखा है <math>=_\beta</math>.
-निम्नलिखित टाइपिंग नियम भी क्यूब की सभी प्रणालियों के लिए सामान्य हैं:<math display="block">\frac{}{\vdash * : \square}\quad \text{(Axiom)}</math><math display="block">\frac{\Gamma \vdash A : s \quad x\text{ does not occur in }\Gamma}{\Gamma, x : A \vdash x : A }\quad \text{(Start)}</math><math display="block">\frac{\Gamma \vdash A : B \quad \Gamma \vdash C : s}{\Gamma, x : C \vdash A : B}\quad \text{(Weakening)}</math><math display="block">\frac{\Gamma \vdash C : \Pi x : A . B \quad \Gamma \vdash a : A}{\Gamma \vdash Ca : B[a/x]}\quad\text{(Application)}</math><math display="block">\frac{\Gamma \vdash A : B \quad B =_{\beta} B' \quad \Gamma \vdash B' : s}{\Gamma \vdash A : B'}\quad\text{(Conversion)}</math>प्रणालियों के बीच अंतर प्रकार के जोड़े में है <math display="inline">(s_1,s_2)</math> निम्नलिखित दो टाइपिंग नियमों में इसकी अनुमति है:<math display="block">\frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2}{\Gamma \vdash \Pi x : A . B : s_2}\quad\text{(Product)}</math><math>\frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash b : B \quad \Gamma, x : A \vdash B : s_2}{\Gamma \vdash \lambda x : A . b : \Pi x : A . B}\quad\text{(Abstraction)}</math>
+इस इंन्वायरमेंट में सामान्यतः टाइप की गई प्रणालियों में होता है, जिसे <math>\Gamma := \emptyset \mid \Gamma, x : T</math> द्वारा उपयोग किया जाता है।
+क्यूब में सभी प्रणालियों के लिए β-कमी की धारणा साधारण है। जिसे <math>\to_{\beta}</math> द्वारा लिखा जाता है, और इसे नियमानुसार दिया जाता है-<math display="block">\frac{}{(\lambda x : A . B)~C \to_{\beta} B[C/x]}</math><math display="block">\frac{B \to_{\beta} B'}{\lambda x : A . B \to_{\beta} \lambda x : A . B'}</math><math display="block">\frac{A \to_{\beta} A'}{\lambda x : A . B \to_{\beta} \lambda x : A' . B}</math><math display="block">\frac{B \to_{\beta} B'}{\Pi x : A . B \to_{\beta} \Pi x : A . B'}</math><math display="block">\frac{A \to_{\beta} A'}{\Pi x : A . B \to_{\beta} \Pi x : A' . B}</math>
+इसका रिफ्लेक्सिव ट्रांजिटिव क्लोजर या रिफ्लेक्सिव, ट्रांजिटिव क्लोजर <math>=_\beta</math> लिखा है।
+निम्नलिखित टाइपिंग नियम भी क्यूब की सभी प्रणालियों के लिए सामान्य हैं:<math display="block">\frac{}{\vdash * : \square}\quad \text{(Axiom)}</math><math display="block">\frac{\Gamma \vdash A : s \quad x\text{ does not occur in }\Gamma}{\Gamma, x : A \vdash x : A }\quad \text{(Start)}</math><math display="block">\frac{\Gamma \vdash A : B \quad \Gamma \vdash C : s}{\Gamma, x : C \vdash A : B}\quad \text{(Weakening)}</math><math display="block">\frac{\Gamma \vdash C : \Pi x : A . B \quad \Gamma \vdash a : A}{\Gamma \vdash Ca : B[a/x]}\quad\text{(Application)}</math><math display="block">\frac{\Gamma \vdash A : B \quad B =_{\beta} B' \quad \Gamma \vdash B' : s}{\Gamma \vdash A : B'}\quad\text{(Conversion)}</math>प्रणालियों के बीच अंतर प्रकार <math display="inline">(s_1,s_2)</math> के जोड़े में है, इसे निम्नलिखित दो टाइपिंग नियमों में इसकी अनुमति किया जाता है:<math display="block">\frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2}{\Gamma \vdash \Pi x : A . B : s_2}\quad\text{(Product)}</math><math>\frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash b : B \quad \Gamma, x : A \vdash B : s_2}{\Gamma \vdash \lambda x : A . b : \Pi x : A . B}\quad\text{(Abstraction)}</math>
 सिस्टम और जोड़ियों के बीच पत्राचार <math display="inline">(s_1,s_2)</math> नियमों में निम्नलिखित की अनुमति है:
 {| class="wikitable"
@@ Line 119: / Line 117: @@
 |{{ya}}
 |}
-घन की प्रत्येक दिशा एक जोड़ी (जोड़ी को छोड़कर) से मेल खाती है <math display="inline">(*,*)</math> सभी प्रणालियों द्वारा साझा किया जाता है), और बदले में प्रत्येक जोड़ी शब्दों और प्रकारों के बीच निर्भरता की एक संभावना से मेल खाती है:
+घन की प्रत्येक दिशा जोड़ी (जोड़ी को छोड़कर) से मेल खाती है, इस प्रकार <math display="inline">(*,*)</math> सभी प्रणालियों द्वारा साझा किया जाता है, और इसके अतिरिक्त प्रत्येक जोड़ी शब्दों और प्रकारों के बीच निर्भरता की संभावना से मेल खाती है:
 * <math display="inline">(*,*)</math> शर्तों को शर्तों पर निर्भर रहने की अनुमति देता है।
@@ Line 130: / Line 128: @@
 ===λ→===
-एक विशिष्ट व्युत्पत्ति जो प्राप्त की जा सकती है वह है<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \Pi x : \alpha . \alpha</math>या तीर शॉर्टकट के साथ<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \alpha \to \alpha</math>पहचान से काफी मिलता-जुलता (प्रकार का)। <math display="inline">\alpha</math>) सामान्य λ→ का। ध्यान दें कि उपयोग किए गए सभी प्रकार संदर्भ में दिखाई देने चाहिए, क्योंकि एकमात्र व्युत्पत्ति जो खाली संदर्भ में की जा सकती है <math display="inline">\vdash * : \square</math>.
+विशिष्ट व्युत्पत्ति जो प्राप्त की जा सकती है वह है<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \Pi x : \alpha . \alpha</math>या तीर शॉर्टकट के साथ<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \alpha \to \alpha</math>इकसा पहचान करने से अत्यधिक मिलते-जुलते प्रकार का  <math display="inline">\alpha</math>) सामान्य λ→ का हैं। यहाँ पर ध्यान दें कि उपयोग किए गए सभी प्रकार संदर्भ में दिखाई देने चाहिए, क्योंकि एकमात्र व्युत्पत्ति जो खाली संदर्भ <math display="inline">\vdash * : \square</math>. में व्यक्त की जा सकती है।
-कंप्यूटिंग शक्ति काफी कमजोर है, यह विस्तारित बहुपद (एक सशर्त ऑपरेटर के साथ बहुपद) से मेल खाती है।<ref>{{Cite journal |last=Schwichtenberg |first=Helmut |author-link=Helmut Schwichtenberg |date=1975 |title=Definierbare Funktionen imλ-Kalkül mit Typen |journal=Archiv für Mathematische Logik und Grundlagenforschung |volume=17 |issue=3–4 |pages=113–114 |doi=10.1007/bf02276799 |s2cid=11598130 |issn=0933-5846 |language=DE}}</ref>
+कंप्यूटिंग शक्ति बहुत कमजोर है, यह विस्तारित बहुपद सशर्त ऑपरेटर के साथ बहुपद से मेल खाती है।<ref>{{Cite journal |last=Schwichtenberg |first=Helmut |author-link=Helmut Schwichtenberg |date=1975 |title=Definierbare Funktionen imλ-Kalkül mit Typen |journal=Archiv für Mathematische Logik und Grundlagenforschung |volume=17 |issue=3–4 |pages=113–114 |doi=10.1007/bf02276799 |s2cid=11598130 |issn=0933-5846 |language=DE}}</ref>
 ===λ2===
-λ2 में, ऐसे पद प्राप्त किए जा सकते हैं<math display="block">\vdash (\lambda \beta : * . \lambda x : \bot . x \beta) : \Pi \beta : * . \bot \to \beta</math>साथ <math display="inline">\bot = \Pi \alpha : * . \alpha</math>. अगर कोई पढ़ता है <math display="inline">\Pi</math> एक सार्वभौमिक परिमाणीकरण के रूप में, करी-हावर्ड समरूपता के माध्यम से, इसे विस्फोट के सिद्धांत के प्रमाण के रूप में देखा जा सकता है। सामान्य तौर पर, λ2 में [[ असंभाव्यता ]] प्रकार जैसे होने की संभावना जुड़ती है <math display="inline">\bot</math>, यह स्वयं सहित सभी प्रकारों पर मात्रा निर्धारित करने वाला शब्द है।<br />बहुरूपता उन कार्यों के निर्माण की भी अनुमति देती है जो λ→ में निर्माण योग्य नहीं थे। अधिक सटीक रूप से, λ2 में परिभाषित कार्य दूसरे क्रम के [[पीनो अंकगणित]] में सिद्ध रूप से कुल हैं।<ref>{{cite book |first1=Jean-Yves |last1=Girard |first2=Yves |last2=Lafont |first3=Paul |last3=Taylor |title=प्रमाण एवं प्रकार|publisher=Cambridge University Press |year=1989 |isbn=9780521371810 |volume=7 |series=Cambridge Tracts in Theoretical Computer Science }}</ref> विशेष रूप से, सभी आदिम पुनरावर्ती कार्य निश्चित हैं।
+λ2 में, ऐसे पद प्राप्त किए जा सकते हैं<math display="block">\vdash (\lambda \beta : * . \lambda x : \bot . x \beta) : \Pi \beta : * . \bot \to \beta</math><math display="inline">\bot = \Pi \alpha : * . \alpha</math> के साथ यदि कोई <math display="inline">\Pi</math> पढ़ता है, तो सार्वभौमिक परिमाणीकरण के रूप में, करी-हावर्ड समरूपता के माध्यम से, इसे विस्फोट के सिद्धांत के प्रमाण के रूप में देखा जा सकता है। सामान्य तौर पर, λ2 में [[ असंभाव्यता |असंभाव्यता]] प्रकार जैसे होने की संभावना <math display="inline">\bot</math> से जुड़ती है, यह स्वयं सहित सभी प्रकारों पर मात्रा निर्धारित करने वाला शब्द है।<br />इसकी बहुरूपता उन कार्यों के निर्माण की भी अनुमति देती है, जो λ→ में निर्माण योग्य नहीं थे। इसके अधिक सटीक रूप से λ2 में परिभाषित कार्य दूसरे क्रम के [[पीनो अंकगणित]] में सिद्ध रूप से कुल हैं।<ref>{{cite book |first1=Jean-Yves |last1=Girard |first2=Yves |last2=Lafont |first3=Paul |last3=Taylor |title=प्रमाण एवं प्रकार|publisher=Cambridge University Press |year=1989 |isbn=9780521371810 |volume=7 |series=Cambridge Tracts in Theoretical Computer Science }}</ref> विशेष रूप से, सभी आदिम पुनरावर्ती कार्य निश्चित हैं।
 ===λP===
-λP में, शब्दों के आधार पर प्रकार रखने की क्षमता का मतलब है कि कोई तार्किक विधेय व्यक्त कर सकता है। उदाहरण के लिए, निम्नलिखित व्युत्पन्न है:<math display="block">\alpha : *, a_0 : \alpha, p : \alpha \to *, q : * \vdash \lambda z : (\Pi x : \alpha . p x \to q) . \lambda y : (\Pi x : \alpha . p x) . (z a_0) (y a_0) : (\Pi x : \alpha . p x \to q) \to (\Pi x : \alpha . p x) \to q</math>जो, करी-हावर्ड समरूपता के माध्यम से, के प्रमाण से मेल खाता है <math>(\forall x : A, P x \to Q) \to (\forall x : A, P x) \to Q</math>.<br />कम्प्यूटेशनल दृष्टिकोण से, हालांकि, आश्रित प्रकार होने से कम्प्यूटेशनल शक्ति में वृद्धि नहीं होती है, केवल अधिक सटीक प्रकार के गुणों को व्यक्त करने की संभावना होती है।<ref name=":1">{{Cite book|title=Lambda-Prolog de A à Z ... ou presque|last=Ridoux|first=Olivier|date=1998|publisher=[s.n.]|oclc=494473554|url=ftp://ftp.irisa.fr/techreports/habilitations/ridoux.pdf }}</ref>
+λP में, शब्दों के आधार पर प्रकार रखने की क्षमता का मतलब है कि कोई तार्किक विधेय व्यक्त कर सकता है। उदाहरण के लिए, निम्नलिखित व्युत्पन्न है:<math display="block">\alpha : *, a_0 : \alpha, p : \alpha \to *, q : * \vdash \lambda z : (\Pi x : \alpha . p x \to q) . \lambda y : (\Pi x : \alpha . p x) . (z a_0) (y a_0) : (\Pi x : \alpha . p x \to q) \to (\Pi x : \alpha . p x) \to q</math>जो करी-हावर्ड समरूपता के माध्यम से इसके प्रमाण <math>(\forall x : A, P x \to Q) \to (\forall x : A, P x) \to Q</math> से मेल खाता है,<br />कम्प्यूटेशनल दृष्टिकोण से आश्रित प्रकार होने से कम्प्यूटेशनल शक्ति में वृद्धि नहीं होती है, केवल अधिक सटीक प्रकार के गुणों को व्यक्त करने की संभावना होती है।<ref name=":1">{{Cite book|title=Lambda-Prolog de A à Z ... ou presque|last=Ridoux|first=Olivier|date=1998|publisher=[s.n.]|oclc=494473554|url=ftp://ftp.irisa.fr/techreports/habilitations/ridoux.pdf }}</ref>आश्रित प्रकारों से निपटने के समय रूपांतरण नियम की अत्यधिक आवश्यकता होती है, क्योंकि यह प्रकार की शर्तों पर गणना करने की अनुमति देता है। उदाहरण के लिए, यदि आपके पास है <math>\Gamma \vdash A : P((\lambda x . x)y)</math> और <math>\Gamma \vdash B : \Pi x : P(y) . C</math>, प्राप्त करने के लिए आपको रूपांतरण नियम लागू करना होगा, जिसे <math>\Gamma \vdash  A : P(y)</math> टाइप करने में सक्षम होने के लिए <math>\Gamma \vdash B A : C</math> द्वारा उपयोग किया जाता हैं।
-आश्रित प्रकारों से निपटने के दौरान रूपांतरण नियम की अत्यधिक आवश्यकता होती है, क्योंकि यह प्रकार की शर्तों पर गणना करने की अनुमति देता है। उदाहरण के लिए, यदि आपके पास है <math>\Gamma \vdash A : P((\lambda x . x)y)</math> और <math>\Gamma \vdash B : \Pi x : P(y) . C</math>, प्राप्त करने के लिए आपको रूपांतरण नियम लागू करना होगा <math>\Gamma \vdash  A : P(y)</math> टाइप करने में सक्षम होने के लिए <math>\Gamma \vdash B A : C</math>.
 ===एल===
-एलō में, निम्नलिखित ऑपरेटर<math display="block">AND := \lambda \alpha : * . \lambda \beta : * . \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma</math>निश्चित है, अर्थात् <math>\vdash AND : * \to * \to *</math>. व्युत्पत्ति<math display="block">\alpha : *, \beta : * \vdash \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma : *</math>पहले से ही λ2 में प्राप्त किया जा सकता है, हालाँकि बहुरूपी <math display="inline">AND</math> केवल तभी परिभाषित किया जा सकता है जब नियम <math display="inline">(\square, *)</math> भी मौजूद है.
+एलō में, निम्नलिखित ऑपरेटर<math display="block">AND := \lambda \alpha : * . \lambda \beta : * . \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma</math>निश्चित है, अर्थात् <math>\vdash AND : * \to * \to *</math> इसकी व्युत्पत्ति हैं।<math display="block">\alpha : *, \beta : * \vdash \Pi \gamma : * . (\alpha \to \beta \to \gamma) \to \gamma : *</math>इसके पहले से ही λ2 में प्राप्त किया जा सकता है, चूंकि बहुरूपी <math display="inline">AND</math> केवल तभी परिभाषित किया जा सकता है, जब नियम <math display="inline">(\square, *)</math> भी सम्मिलित है।
-कंप्यूटिंग के दृष्टिकोण से, λω बेहद मजबूत है, और इसे प्रोग्रामिंग भाषाओं के लिए आधार माना गया है।<ref>{{Cite book|title=उच्च-क्रम टाइप किए गए लैम्ब्डा-कैलकुली में प्रोग्रामिंग|last1=Pierce |first1=Benjamin |first2=Scott |last2=Dietzen |first3=Spiro |last3=Michaylov |date=1989 |publisher=Computer Science Department, Carnegie Mellon University |id=CMU-CS-89-111 ERGO-89-075 |oclc=20442222}}</ref>
+कंप्यूटिंग के दृष्टिकोण से, λω बेहद शक्तिशाली है, और इसे प्रोग्रामिंग भाषाओं के लिए आधार माना गया है।<ref>{{Cite book|title=उच्च-क्रम टाइप किए गए लैम्ब्डा-कैलकुली में प्रोग्रामिंग|last1=Pierce |first1=Benjamin |first2=Scott |last2=Dietzen |first3=Spiro |last3=Michaylov |date=1989 |publisher=Computer Science Department, Carnegie Mellon University |id=CMU-CS-89-111 ERGO-89-075 |oclc=20442222}}</ref>
 ===λC===
@@ Line 156: / Line 150: @@
 == अन्य प्रणालियों से संबंध ==
-सिस्टम [[ स्वचालित ]] तार्किक दृष्टिकोण से λ2 के समान है। एमएल (प्रोग्रामिंग भाषा)|एमएल जैसी भाषाएं, टाइपिंग के दृष्टिकोण से, λ→ और λ2 के बीच कहीं स्थित होती हैं, क्योंकि वे एक प्रतिबंधित प्रकार के बहुरूपी प्रकारों को स्वीकार करते हैं, जो कि प्रीनेक्स सामान्य रूप में प्रकार हैं। हालाँकि, क्योंकि उनमें कुछ रिकर्सन ऑपरेटर होते हैं, उनकी कंप्यूटिंग शक्ति λ2 से अधिक होती है।<ref name=":1" />Coq प्रणाली केवल एक अप्राप्य के बजाय ब्रह्मांडों के एक रैखिक पदानुक्रम के साथ λC के विस्तार पर आधारित है <math display="inline">\square</math>, और आगमनात्मक प्रकार के निर्माण की क्षमता।
+सिस्टम [[ स्वचालित |स्वचालित]] तार्किक दृष्टिकोण से λ2 के समान है। एमएल (प्रोग्रामिंग भाषा) या एमएल जैसी भाषाएं, टाइपिंग के दृष्टिकोण से, λ→ और λ2 के बीच कहीं स्थित होती हैं, क्योंकि वे प्रतिबंधित प्रकार के बहुरूपी प्रकारों को स्वीकार करते हैं, जो कि प्रीनेक्स सामान्य रूप में प्रकार हैं। चूंकि, क्योंकि उनमें कुछ रिकर्सन ऑपरेटर होते हैं, उनकी कंप्यूटिंग शक्ति λ2 से अधिक होती है।<ref name=":1" /> इस प्रकार Coq प्रणाली केवल अप्राप्य के अतिरिक्त ब्रह्मांडों के रैखिक पदानुक्रम के साथ λC के विस्तार <math display="inline">\square</math> पर आधारित है, और आगमनात्मक प्रकार के निर्माण की क्षमता प्राप्त करता हैं।
-शुद्ध प्रकार की प्रणालियों को घन के सामान्यीकरण के रूप में देखा जा सकता है, जिसमें प्रकार, स्वयंसिद्ध, उत्पाद और अमूर्त नियमों का एक मनमाना सेट होता है। इसके विपरीत, लैम्ब्डा क्यूब के सिस्टम को दो प्रकार के शुद्ध प्रकार के सिस्टम के रूप में व्यक्त किया जा सकता है <math>\{*, \square\}</math>, एकमात्र स्वयंसिद्ध <math display="inline">\{*,\square\}</math>, और नियमों का एक सेट <math display="inline">R</math> ऐसा है कि <math>\{(*,*,*)\} \subseteq R \subseteq \{(*,*,*), (*,\square, \square), (\square, *, *), (\square, \square, \square) \}</math>.<ref name=":0" />
+इसके शुद्ध प्रकार की प्रणालियों को घन के सामान्यीकरण के रूप में देखा जा सकता है, जिसमें प्रकार को स्वयंसिद्ध, उत्पाद और अमूर्त नियमों के द्वारा सेट किया जाता है। इसके विपरीत, लैम्ब्डा क्यूब के सिस्टम को दो प्रकार के शुद्ध प्रकार के सिस्टम के रूप में व्यक्त किया जा सकता है, इसके लिए <math>\{*, \square\}</math>, एकमात्र स्वयंसिद्ध <math display="inline">\{*,\square\}</math>, और नियमों का सेट <math display="inline">R</math> के लिए इस प्रकार हैं कि <math>\{(*,*,*)\} \subseteq R \subseteq \{(*,*,*), (*,\square, \square), (\square, *, *), (\square, \square, \square) \}</math>.<ref name=":0" />
-करी-हावर्ड समरूपता के माध्यम से, लैम्ब्डा क्यूब और तार्किक प्रणालियों में सिस्टम के बीच एक-से-एक पत्राचार होता है,<ref name=":0" />अर्थात्:
+करी-हावर्ड समरूपता के माध्यम से, लैम्ब्डा क्यूब और तार्किक प्रणालियों में सिस्टम के बीच एक-से-एक पत्राचार होता है,<ref name=":0" /> अर्थात्:
 {| class="wikitable"
-!System of the cube
+!घन की प्रणाली
-!Logical System
+!तार्किक प्रणाली
 |-
 |λ→
-|(First-order) [[Propositional calculus|Propositional Calculus]]
+|(प्रथम-क्रम) प्रस्तावात्मक कलन
 |-
 |λ2
-|[[Second-order propositional logic|Second-order Propositional Calculus]]
+|[[Second-order propositional logic|दूसरे क्रम का प्रस्तावात्मक कैलकुलस]]
 |-
 |λ{{Underline|ω}}
-|Weakly Higher Order Propositional Calculus
+|कमज़ोर उच्च क्रम प्रस्तावक कलन
 |-
 |λω
-|Higher Order Propositional Calculus
+|उच्च क्रम प्रस्ताव कलन
 |-
 |λP
-|(First order) [[Predicate Logic]]
+|(प्रथम क्रम) विधेय तर्क
 |-
 |λP2
-|[[Second order predicate calculus|Second-order Predicate Calculus]]
+|[[Second order predicate calculus|दूसरे क्रम का विधेय कलन]]
 |-
 |λP{{Underline|ω}}
-|Weak [[Higher-order logic|Higher Order Predicate Calculus]]
+|कमज़ोर उच्चतर क्रम विधेय कलन
 |-
 |λC
-|[[Calculus of constructions|Calculus of Constructions]]
+|[[Calculus of constructions|निर्माणों की गणना]]
 |}
-सभी तर्क एक निहितार्थ हैं (अर्थात केवल संयोजक हैं <math display="inline">\to</math> और <math display="inline">\forall</math>), हालाँकि कोई अन्य संयोजकों को परिभाषित कर सकता है जैसे कि <math>\wedge</math> या <math>\neg</math> दूसरे और उच्च क्रम के तर्कों में एक अव्यवहारिक तरीके से। कमजोर उच्च क्रम तर्कशास्त्र में, उच्च क्रम विधेय के लिए चर होते हैं, लेकिन उन पर कोई परिमाणीकरण नहीं किया जा सकता है।
+सभी तर्क निहितार्थ हैं, अर्थात केवल संयोजक हैं <math display="inline">\to</math> और <math display="inline">\forall</math> के रूप में प्रदर्शित होते हैं, चूंकि कोई अन्य संयोजकों को परिभाषित कर सकता है, जैसे कि <math>\wedge</math> या <math>\neg</math> दूसरे और उच्च क्रम के तर्कों में अव्यवहारिक तरीके से व्यक्त किये जाते हैं। इस प्रकार कमजोर उच्च क्रम तार्किकी में उच्च क्रम विधेय के लिए चर होते हैं, अपितु उन पर कोई परिमाणीकरण नहीं किया जा सकता है।
 ==सामान्य गुण==
-क्यूब के सभी सिस्टम आनंद लेते हैं
+क्यूब के सभी प्रणालियो का उपोयग करते हैं
 * [[चर्च-रोसेर संपत्ति]]: यदि <math>M \to_\beta N</math> और <math>M \to_\beta N'</math> तो वहाँ अस्तित्व है <math>N''</math> ऐसा है कि <math>N \to^*_\beta N''</math> और <math>N' \to^*_\beta N''</math>;
 * [[विषय में कमी]]: यदि <math>\Gamma \vdash M : T</math> और <math>M \to_\beta M'</math> तब <math>\Gamma \vdash M' : T</math>;
 * प्रकारों की विशिष्टता: यदि <math>\Gamma \vdash A : B</math> और <math>\Gamma \vdash A : B'</math> तब <math>B =_\beta B'</math>.
-ये सभी सामान्य शुद्ध प्रकार की प्रणालियों पर सिद्ध किए जा सकते हैं।<ref>{{Cite book |last1=Sørensen|first1=Morten Heine|chapter=Pure type systems and the λ-cube|date=2006|title=करी-हावर्ड समरूपता पर व्याख्यान|pages=343–359|publisher=Elsevier|isbn=9780444520777|last2=Urzyczyin|first2=Pawel|doi=10.1016/s0049-237x(06)80015-7}}</ref>
+ये सभी सामान्य शुद्ध प्रकार की प्रणालियों पर सिद्ध किए जा सकते हैं।<ref>{{Cite book |last1=Sørensen|first1=Morten Heine|chapter=Pure type systems and the λ-cube|date=2006|title=करी-हावर्ड समरूपता पर व्याख्यान|pages=343–359|publisher=Elsevier|isbn=9780444520777|last2=Urzyczyin|first2=Pawel|doi=10.1016/s0049-237x(06)80015-7}}</ref> क्यूब की प्रणाली में अच्छी तरह से टाइप किया गया कोई भी शब्द दृढ़ता से सामान्यीकरण कर रहा है,<ref name=":0" /> चूंकि यह गुण सभी शुद्ध प्रकार की प्रणालियों के लिए सामान्य नहीं है। क्यूब में कोई भी सिस्टम ट्यूरिंग पूर्ण नहीं है।<ref name=":1" />
-क्यूब की प्रणाली में अच्छी तरह से टाइप किया गया कोई भी शब्द दृढ़ता से सामान्यीकरण कर रहा है,<ref name=":0" />हालाँकि यह गुण सभी शुद्ध प्रकार की प्रणालियों के लिए सामान्य नहीं है। क्यूब में कोई भी सिस्टम ट्यूरिंग पूर्ण नहीं है।<ref name=":1" />
+== [[उपप्रकार]] ==
+चूंकि, सबटाइपिंग को क्यूब में प्रदर्शित नहीं किया जाता है, इसके आधार पर <math>F^\omega_{<:}</math>भले ही सिस्टम पसंद करता हो, जिसे उच्च-क्रम सीमाबद्ध परिमाणीकरण के रूप में जाना जाता है, जो उपप्रकार और बहुरूपता को जोड़ता है, व्यावहारिक रुचि का है, और इसे आगे बंधे हुए प्रकार के ऑपरेटरों के लिए सामान्यीकृत किया जा सकता है। आगे विस्तार <math>F^\omega_{<:}</math> विशुद्ध रूप से कार्यात्मक वस्तुओं की परिभाषा की अनुमति दें; ये सिस्टम सामान्यतः लैम्ब्डा क्यूब पेपर प्रकाशित होने के बाद विकसित किए गए थे।<ref>{{Cite book|title=प्रकार और प्रोग्रामिंग भाषाएँ|last=Pierce|first=Benjamin|date=2002|publisher=MIT Press|isbn=978-0262162098|pages=467–490|oclc=300712077 }}</ref>
-== [[उपप्रकार]] ==
+क्यूब का विचार गणितज्ञ हेन्क बेरेन्ड्रेट (1991) की देन है। शुद्ध प्रकार की प्रणालियों का ढांचा लैम्ब्डा क्यूब को इस अर्थ में सामान्यीकृत करता है कि क्यूब के सभी कोनों, साथ ही कई अन्य प्रणालियों को इस सामान्य ढांचे के उदाहरण के रूप में दर्शाया जा सकता है।<ref>{{harvnb|Pierce|2002|p=466}}</ref> यह प्रारूप लैम्ब्डा क्यूब से कुछ साल पहले का है। अपने 1991 के पेपर में, बेरेन्ड्रेट ने इस ढांचे में घन के कोनों को भी परिभाषित किया है।
-हालाँकि, सबटाइपिंग को क्यूब में प्रदर्शित नहीं किया जाता है, भले ही सिस्टम पसंद करता हो <math>F^\omega_{<:}</math>, जिसे उच्च-क्रम सीमाबद्ध परिमाणीकरण के रूप में जाना जाता है, जो उपप्रकार और बहुरूपता को जोड़ता है, व्यावहारिक रुचि का है, और इसे आगे बंधे हुए प्रकार के ऑपरेटरों के लिए सामान्यीकृत किया जा सकता है। आगे विस्तार <math>F^\omega_{<:}</math> विशुद्ध रूप से कार्यात्मक वस्तुओं की परिभाषा की अनुमति दें; ये सिस्टम आम तौर पर लैम्ब्डा क्यूब पेपर प्रकाशित होने के बाद विकसित किए गए थे।<ref>{{Cite book|title=प्रकार और प्रोग्रामिंग भाषाएँ|last=Pierce|first=Benjamin|date=2002|publisher=MIT Press|isbn=978-0262162098|pages=467–490|oclc=300712077 }}</ref>
-क्यूब का विचार गणितज्ञ हेन्क बेरेन्ड्रेट (1991) की देन है। शुद्ध प्रकार की प्रणालियों का ढांचा लैम्ब्डा क्यूब को इस अर्थ में सामान्यीकृत करता है कि क्यूब के सभी कोनों, साथ ही कई अन्य प्रणालियों को इस सामान्य ढांचे के उदाहरण के रूप में दर्शाया जा सकता है।<ref>{{harvnb|Pierce|2002|p=466}}</ref> यह ढांचा लैम्ब्डा क्यूब से कुछ साल पहले का है। अपने 1991 के पेपर में, बेरेन्ड्रेट ने इस ढांचे में घन के कोनों को भी परिभाषित किया है।
 == यह भी देखें ==
-* अनुसंधान को निर्देशित करने की उनकी क्षमता में,<ref>{{harvnb|Ridoux|1998|p=70}}</ref> ओलिवियर रिडौक्स लैम्ब्डा क्यूब का एक कट-आउट टेम्प्लेट देता है और क्यूब का एक ऑक्टाहेड्रोन के रूप में दोहरा प्रतिनिधित्व भी देता है, जहां 8 शीर्षों को चेहरों द्वारा प्रतिस्थापित किया जाता है, साथ ही डोडेकाहेड्रोन के रूप में एक दोहरा प्रतिनिधित्व दिया जाता है, जहां 12 किनारों को बदल दिया जाता है। चेहरे के।
+* अनुसंधान को निर्देशित करने की उनकी क्षमता में,<ref>{{harvnb|Ridoux|1998|p=70}}</ref> ओलिवियर रिडौक्स लैम्ब्डा क्यूब का कट-आउट टेम्प्लेट देता है और क्यूब का ऑक्टाहेड्रोन के रूप में दोहरा प्रतिनिधित्व भी देता है, जहां 8 शीर्षों को चेहरों द्वारा प्रतिस्थापित किया जाता है, साथ ही डोडेकाहेड्रोन के रूप में दोहरा प्रतिनिधित्व दिया जाता है, जहां 12 किनारों को परिवर्तित कर दिया जाता है।
-* [[होमोटोपी प्रकार सिद्धांत]] <!-- Not clear what the link between HoTT and the lambda cube is -->
+* [[होमोटोपी प्रकार सिद्धांत]]
 == टिप्पणियाँ ==
 {{reflist}}
 == अग्रिम पठन ==
 * {{cite web |first1=Simon |last1=Peyton Jones |first2=Erik |last2=Meijer |year=1997 |url=https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf |title=Henk: A Typed Intermediate Language |website=[[Microsoft]] |quote='''Henk''' ''is based directly on the lambda cube'', an expressive family of typed lambda calculi. }}
 == बाहरी संबंध ==
 * [http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm Barendregt's Lambda Cube] in the context of [[pure type systems]] by Roger Bishop Jones
-[[Category: लैम्ब्डा कैलकुलस]] [[Category: प्रकार सिद्धांत]]
-[[Category: Machine Translated Page]]
+[[Category:CS1 Deutsch-language sources (de)]]
 [[Category:Created On 08/07/2023]]
+[[Category:Machine Translated Page]]
+[[Category:Pages with script errors]]
+[[Category:Templates Vigyan Ready]]
+[[Category:प्रकार सिद्धांत]]
+[[Category:लैम्ब्डा कैलकुलस]]

Anonymous

Search

लैम्ब्डा क्यूब: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 15:32, 31 July 2023

Contents

सिस्टम के उदाहरण

(λ→) बस लैम्ब्डा कैलकुलस टाइप किया गया हैं।

(λ2) सिस्टम एफ

(λω) सिस्टम Fω

(λP) लैम्ब्डा-पी

(Fω) सिस्टम Fω

(λC) निर्माणों की गणना

औपचारिक परिभाषा

प्रणालियों के बीच तुलना

λ→

λ2

λP

एल

λC

अन्य प्रणालियों से संबंध

सामान्य गुण

उपप्रकार

यह भी देखें

टिप्पणियाँ

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

लैम्ब्डा क्यूब: Difference between revisions

Latest revision as of 15:32, 31 July 2023

सिस्टम के उदाहरण

(λ→) बस लैम्ब्डा कैलकुलस टाइप किया गया हैं।

(λ2) सिस्टम एफ

(λω) सिस्टम Fω

(λP) लैम्ब्डा-पी

(Fω) सिस्टम Fω

(λC) निर्माणों की गणना

औपचारिक परिभाषा

प्रणालियों के बीच तुलना

λ→

λ2

λP

एल

λC

अन्य प्रणालियों से संबंध

सामान्य गुण

उपप्रकार

यह भी देखें

टिप्पणियाँ

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories