लैम्ब्डा क्यूब

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

गणितीय तर्क और प्रकार सिद्धांत में λ-क्यूब जिसे लैम्ब्डा क्यूब भी लिखा जाता है, मुख्य रूप से यह हेन्क बेरेन्ड्रेट द्वारा प्रस्तुत रूपरेखा है।^[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]