टाइप थ्योरी और करी-हावर्ड आइसोमोर्फिज्म: प्रस्ताव = प्रकार, प्रमाण = प्रोग्राम का गहरा सामंजस्य

कंप्यूटर विज्ञान और गणित के इतिहास में सबसे सुंदर और गहरी खोजों में से एक “करी-हावर्ड आइसोमोर्फिज्म (Curry-Howard Isomorphism)” है। यह अवधारणा मात्र एक सादृश्य (analogy) नहीं है। यह दर्शाता है कि “कंप्यूटर प्रोग्राम लिखना” और “गणितीय प्रमेय सिद्ध करना” वाक्यात्मक (syntactically), अर्थपूर्ण (semantically) और गणितीय संरचना के रूप में पूरी तरह से समान कार्य हैं। हम जिस प्रोग्राम को कंपाइलर के माध्यम से चलाते हैं, उसे तर्कशास्त्र की प्रमाण प्रणाली (proof system) में औपचारिक प्रमाण (formal proof) के रूप में व्याख्यायित किया जा सकता है।

इस लेख में, हम सिम्पली टाइप्ड लैम्ब्डा कैलकुलस (Simply Typed Lambda Calculus) से लेकर सिस्टम एफ (System F), डिपेंडेंट टाइप थ्योरी (Dependent Type Theory), और आधुनिक गणित के सबसे आगे के क्षेत्र, होमोटोपी टाइप थ्योरी (Homotopy Type Theory; HoTT) तक, टाइप थ्योरी और तर्कशास्त्र के चौराहे का पता लगाएंगे। इसके अलावा, हम अनुमान के नियमों (inference rules) के सख्त सूत्रीकरण (formulation) और विशिष्ट प्रमाण कोड को शामिल करते हुए पूरी तरह से समझाएंगे कि आधुनिक प्रमेय प्रमाण सहायक (theorem proof assistants जैसे Coq, Lean 4, आदि) सॉफ़्टवेयर सत्यापन (software verification) के अंतिम रूप को कैसे महसूस कर रहे हैं। 10,000 से अधिक वर्णों की इस यात्रा के माध्यम से, प्रोग्राम और गणित के सच्चे सामंजस्य का अनुभव करें।

अध्याय 1: तर्कशास्त्र और गणना के चमत्कारिक चौराहे: इतिहास और BHK व्याख्या

हास्केल करी और विलियम एल्विन हावर्ड की खोज

करी-हावर्ड आइसोमोर्फिज्म का नाम अमेरिकी गणितज्ञ हास्केल करी (Haskell Curry) और तर्कशास्त्री विलियम एल्विन हावर्ड (William Alvin Howard) के नाम पर रखा गया है। 1934 में, करी ने देखा कि कॉम्बिनेटरी लॉजिक (Combinatory Logic) में प्रकार (type) की संरचना और इंट्यूशनिस्टिक लॉजिक (Intuitionistic Logic) के निहितार्थ प्रस्तावों (implication propositions) के स्वयंसिद्ध सिस्टम (हिल्बर्ट-शैली) के बीच एक आश्चर्यजनक गणितीय समानता है। बाद में, 1969 में, हावर्ड ने एक पेपर प्रकाशित किया जिसमें दिखाया गया कि गेरहार्ड जेंटजेन (Gerhard Gentzen) द्वारा तैयार किया गया “प्राकृतिक निगमन (Natural Deduction)” और अलोंजो चर्च (Alonzo Church) का “लैम्ब्डा कैलकुलस (Lambda Calculus)” पूरी तरह से आइसोमोर्फिक पत्राचार (isomorphic correspondence) में हैं, और इस अवधारणा को मजबूती से स्थापित किया गया।

इंट्यूशनिस्टिक लॉजिक और BHK व्याख्या की सख्त रचनात्मकता (Constructivity)

शास्त्रीय तर्कशास्त्र (Classical logic) में, एक प्रस्ताव का सत्य मूल्य (truth value) या तो “सत्य (True)” या “असत्य (False)” होता है (मध्यम के बहिष्करण का नियम - Law of excluded middle)। हालाँकि, एल. ई. जे. ब्रॉवर (L. E. J. Brouwer) द्वारा स्थापित इंट्यूशनिस्टिक लॉजिक (Intuitionistic Logic) में, सत्य मूल्य की अवधारणा को खारिज कर दिया गया है और इसे परिभाषित किया गया है कि “एक प्रस्ताव सत्य है यदि उसका प्रमाण (साक्ष्य) निर्मित किया जा सकता है”। इस स्थिति को सख्ती से तैयार करने वाला BHK व्याख्या (Brouwer-Heyting-Kolmogorov व्याख्या) है।

BHK व्याख्या के अनुसार, प्रत्येक तार्किक संयोजक (logical connective) के “प्रमाण” को रचनात्मक रूप से (constructively) निम्नानुसार परिभाषित किया गया है:

प्रस्ताव $A \land B$ का प्रमाण एक जोड़ी $(p, q)$ है। यहाँ $p$, $A$ का प्रमाण है, और $q$, $B$ का प्रमाण है।
प्रस्ताव $A \lor B$ का प्रमाण जोड़ी $(0, p)$ या $(1, q)$ है। यहाँ $p$, $A$ का प्रमाण है, और $q$, $B$ का प्रमाण है। टैग (0 या 1) से यह स्पष्ट होता है कि दोनों में से कौन सिद्ध हुआ है।
प्रस्ताव $A \to B$ का प्रमाण एक फ़ंक्शन $f$ है। यह फ़ंक्शन $A$ के किसी भी प्रमाण $x$ को इनपुट के रूप में लेता है और $B$ का प्रमाण $f(x)$ आउटपुट करता है।
प्रस्ताव $\bot$ (विरोधाभास / contradiction) का कोई प्रमाण मौजूद नहीं है।
प्रस्ताव $\exists x \in D, P(x)$ का प्रमाण एक जोड़ी $(d, p)$ है। यहाँ $d \in D$ एक विशिष्ट वस्तु है, और $p$, $P(d)$ का प्रमाण है।
प्रस्ताव $\forall x \in D, P(x)$ का प्रमाण एक फ़ंक्शन $f$ है। यह फ़ंक्शन किसी भी $d \in D$ के लिए $P(d)$ का प्रमाण $f(d)$ आउटपुट करता है।

यदि हम प्रोग्रामिंग के दृष्टिकोण से इस व्याख्या को देखें, तो “प्रस्ताव” कुछ और नहीं बल्कि “प्रकार (Type)” है, और “प्रमाण” कुछ और नहीं बल्कि “उस प्रकार का मान (प्रोग्राम, फ़ंक्शन)” है। इंट्यूशनिस्टिक लॉजिक में प्रमाणों का निर्माण स्वयं डेटा संरचनाओं (data structures) और एल्गोरिदम (algorithms) का निर्माण है।

अध्याय 2: प्राकृतिक निगमन (Natural Deduction) और प्रकार अनुमान नियमों (Type Inference Rules) की पूर्ण तुलना तालिका और सख्त सूत्रीकरण

करी-हावर्ड पत्राचार का मूल जेंटजेन के प्राकृतिक निगमन के अनुमान नियमों और सिम्पली टाइप्ड लैम्ब्डा कैलकुलस के टाइपिंग नियमों के बीच पूर्ण मेल है। नीचे प्रत्येक तार्किक संयोजक (logical connective) के लिए परिचय नियमों (Introduction Rule) और उन्मूलन नियमों (Elimination Rule) की एक सख्त तुलना तालिका दी गई है।

संदर्भ (Context) $\Gamma$ मान्यताओं (चरों और उनके प्रकारों के जोड़े) के सेट को दर्शाता है। $\Gamma \vdash M : A$ का अर्थ है कि “संदर्भ $\Gamma$ के तहत, पद (term) $M$ का प्रकार $A$ है (अर्थात, यह प्रस्ताव $A$ का प्रमाण है)"।

निहितार्थ (Implication) ($\to$) और फ़ंक्शन प्रकार (Function Type)

$$ \frac{\Gamma, x:A \vdash M : B}{\Gamma \vdash (\lambda x:A. M) : A \to B} \quad (\to\text{-}I) $$

यदि मान्यता $A$ (चर $x$) का परिचय करके $B$ (पद $M$) को प्रमाणित किया जा सकता है, तो $A$ से $B$ का निहितार्थ (फ़ंक्शन $\lambda x:A. M$) प्रमाणित हो जाता है। यह अनाम फ़ंक्शन (anonymous function) की बहुत परिभाषा है।

$$ \frac{\Gamma \vdash M : A \to B \quad \Gamma \vdash N : A}{\Gamma \vdash (M\ N) : B} \quad (\to\text{-}E) $$

जब $A \to B$ का प्रमाण $M$ (फ़ंक्शन) और $A$ का प्रमाण $N$ (तर्क/argument) हो, तो इन्हें लागू (Apply) करके $B$ का प्रमाण $M\ N$ प्राप्त किया जाता है। यह मोड्स पोनेन्स (Modus Ponens) है।

संयोजन (Conjunction) ($\land$) और उत्पाद प्रकार (Product Type / Tuple)

$$ \frac{\Gamma \vdash M : A \quad \Gamma \vdash N : B}{\Gamma \vdash (M, N) : A \land B} \quad (\land\text{-}I) $$

यदि $A$ और $B$ के प्रमाण अलग-अलग उपलब्ध हैं, तो उन्हें एक जोड़ी बनाने से $A \land B$ प्रमाणित हो जाता है।

$$ \frac{\Gamma \vdash P : A \land B}{\Gamma \vdash \pi_1(P) : A} \quad (\land\text{-}E_1) \qquad \frac{\Gamma \vdash P : A \land B}{\Gamma \vdash \pi_2(P) : B} \quad (\land\text{-}E_2) $$

जोड़ी $P$ से पहले तत्व को निकालने का ऑपरेशन $\pi_1$, $A$ की ओर जाता है, और दूसरे तत्व को निकालने का ऑपरेशन $\pi_2$, $B$ की ओर जाता है।

वियोजन (Disjunction) ($\lor$) और सम प्रकार (Sum Type / Either / Coproduct)

$$ \frac{\Gamma \vdash M : A}{\Gamma \vdash \text{inl}(M) : A \lor B} \quad (\lor\text{-}I_1) \qquad \frac{\Gamma \vdash N : B}{\Gamma \vdash \text{inr}(N) : A \lor B} \quad (\lor\text{-}I_2) $$

यदि $A$ या $B$ में से किसी एक का प्रमाण है, तो $A \lor B$ का निर्माण किया जा सकता है। यह Haskell के Left या Right के बराबर है।

$$ \frac{\Gamma \vdash P : A \lor B \quad \Gamma, x:A \vdash M_1 : C \quad \Gamma, y:B \vdash M_2 : C}{\Gamma \vdash \text{case } P \text{ of } \text{inl}(x) \Rightarrow M_1 \mid \text{inr}(y) \Rightarrow M_2 : C} \quad (\lor\text{-}E) $$

यदि $A \lor B$ मान्य है, और $A$ से $C$, तथा $B$ से $C$ प्राप्त किया जा सकता है, तो $C$ का निष्कर्ष निकाला जा सकता है। यह प्रोग्रामिंग में केस एनालिसिस (पैटर्न मिलान) है।

विरोधाभास (Contradiction) ($\bot$) और खाली प्रकार (Empty Type / Void)

$$ \frac{\Gamma \vdash M : \bot}{\Gamma \vdash \text{abort}_A(M) : A} \quad (\bot\text{-}E) $$

यदि विरोधाभास $\bot$ सिद्ध हो जाता है, तो किसी भी प्रस्ताव $A$ को प्राप्त किया जा सकता है। यह एक खाली प्रकार (Void) से किसी भी मान का उत्पादन करने वाले एक आभासी (virtual) फ़ंक्शन abort से मेल खाता है जिसमें कोई तत्व नहीं होता है (वास्तव में इसे कभी कॉल नहीं किया जाता है)।

अध्याय 3: प्रमाण का सामान्यीकरण (Proof Normalization / Cut Elimination) और $\beta$-रिडक्शन का गणितीय मेल

प्राकृतिक निगमन में एक महत्वपूर्ण प्रमेय “सामान्यीकरण प्रमेय (Normalization Theorem)” है। जेंटजेन ने दिखाया कि सीक्वेंट कैलकुलस में “कट नियम (Cut Rule)” को हटाया जा सकता है (कट एलिमिनेशन थ्योरम, जेंटजेन का हॉपत्सत्ज़ / Gentzen’s Hauptsatz)। प्राकृतिक निगमन में, इसका अर्थ है कि “एक चक्कर (Detour) जहाँ परिचय नियम के तुरंत बाद उन्मूलन नियम लागू किया जाता है, उसे सीधे प्रमाण में बदला जा सकता है”।

आश्चर्यजनक रूप से, तर्कशास्त्र में “प्रमाण के परिवर्तन/सरलीकरण” की यह प्रक्रिया लैम्ब्डा कैलकुलस में “प्रोग्राम के निष्पादन (मूल्यांकन)”, यानी $\beta$-रिडक्शन (Beta Reduction) के बिल्कुल समान है।

निहितार्थ में सामान्यीकरण और $\beta$-रिडक्शन

निम्नलिखित चक्कर (detour) वाले प्रमाण (प्रोग्राम) पर विचार करें:

$x:A$ मान लें और $M:B$ प्राप्त करें, और $A \to B$ का परिचय ($\to\text{-}I$) दें। अर्थात् $\lambda x:A. M$।
तुरंत बाद, $A$ के प्रमाण $N$ का उपयोग करके निहितार्थ को हटा दें ($\to\text{-}E$)। अर्थात् $(\lambda x:A. M)\ N$।

तार्किक रूप से, आप मान्यता $x$ का परिचय देकर एक प्रमाण बनाते हैं और तुरंत उस मान्यता में एक विशिष्ट प्रमाण $N$ को प्रतिस्थापित करते हैं। यह निरर्थक (redundant) है, और यदि आप शुरुआत से ही $M$ में मान्यता $x$ वाले सभी स्थानों पर $N$ को शामिल करते हैं, तो आप सीधे $B$ का प्रमाण प्राप्त कर सकते हैं। कंप्यूटर विज्ञान की दृष्टि से, यह वास्तव में फ़ंक्शन का अनुप्रयोग है, और जब इसे निष्पादित किया जाता है, तो तर्क (argument) $N$ को पैरामीटर $x$ में प्रतिस्थापित किया जाता है।

$$ (\lambda x:A. M)\ N \quad \longrightarrow_\beta \quad M[x := N] $$

यह $\beta$-रिडक्शन है। तर्कशास्त्र में “प्रमाण का कट एलिमिनेशन” वास्तव में वह कदम है जिसके द्वारा एक प्रोग्राम वास्तव में “गणना” को आगे बढ़ाता है।

मजबूत सामान्यीकरण प्रमेय (Strong Normalization Theorem) और चर्च-रॉसर प्रमेय (Church-Rosser Theorem)

सिम्पली टाइप्ड लैम्ब्डा कैलकुलस में, कोई भी टाइप करने योग्य पद (term) हमेशा $\beta$-रिडक्शन की एक परिमित संख्या में ऐसी अवस्था (सामान्य रूप, Normal Form) तक पहुँच जाता है जहाँ आगे कोई गणना नहीं की जा सकती है। इसे “मजबूत सामान्यीकरण प्रमेय (Strong Normalization Theorem)” कहा जाता है। यह तर्कशास्त्र में इस तथ्य से मेल खाता है कि “किसी भी प्रमाण को हमेशा बिना चक्कर वाले सीधे प्रमाण में फिर से लिखा जा सकता है”। इसके अलावा, चर्च-रॉसर प्रमेय (Church-Rosser Theorem) के कारण, अंतिम सामान्य रूप विशिष्ट (unique) होता है, चाहे गणना का क्रम कुछ भी हो। मजबूत सामान्यीकरण गुण वाले सिस्टम में, प्रोग्राम को रोकना (Turing अपूर्ण) निश्चित है। यदि कोई अनंत लूप (जैसे कि Y कॉम्बिनेटर या $\Omega = (\lambda x. x\ x)(\lambda x. x\ x)$) मौजूद है, तो तार्किक रूप से इसका अर्थ “आत्म-संदर्भ से उत्पन्न विरोधाभास” होगा, और सिस्टम की सुदृढ़ता (consistency) ढह जाएगी।

अध्याय 4: डिपेंडेंट टाइप्स (Dependent Types) और फर्स्ट-ऑर्डर प्रेडिकेट लॉजिक (First-Order Predicate Logic) का पत्राचार

अब तक का पत्राचार प्रपोजिशनल लॉजिक (Propositional Logic) के दायरे में था। यह “डिपेंडेंट टाइप थ्योरी (Dependent Type Theory)” थी, जिसे पर मार्टिन-लोफ (Per Martin-Löf) और अन्य लोगों द्वारा बनाया गया था, जिसने करी-हावर्ड पत्राचार को “फर्स्ट-ऑर्डर लॉजिक (First-Order Logic)” तक बढ़ाया।

डिपेंडेंट टाइप का अर्थ है “एक प्रकार जो किसी मान (term) के आधार पर बदलता है”। उदाहरण के लिए, “लंबाई $n$ के एक वेक्टर” का प्रकार प्राकृत संख्या (natural number) मान $n$ पर निर्भर करता है।

सार्वभौमिक प्रतीक (Universal Symbol) $\forall$ और डिपेंडेंट प्रोडक्ट टाइप ($\Pi$ प्रकार)

सार्वभौमिक प्रस्ताव (universal proposition) $\forall x:A, B(x)$ कि “सभी $x \in A$ के लिए, $B(x)$ मान्य है” को एक ऐसे फ़ंक्शन के रूप में माना जा सकता है जो तर्क (argument) $x:A$ को स्वीकार करता है और प्रकार $B(x)$ का मान लौटाता है। इस फ़ंक्शन प्रकार को $\Pi$ प्रकार (Pi Type, Dependent Product Type) कहा जाता है।

$$ \frac{\Gamma, x:A \vdash M : B(x)}{\Gamma \vdash (\lambda x:A. M) : \Pi x:A. B(x)} \quad (\Pi\text{-}I) $$

उदाहरण के लिए, इस प्रमेय का प्रमाण कि “सभी प्राकृत संख्याओं $n$ के लिए, $n+n = 2n$ है”, एक फ़ंक्शन के रूप में कार्यान्वित किया जाता है जो प्राकृत संख्या $n$ को तर्क के रूप में लेता है और “$n+n = 2n$ के प्रमाण (इस प्रकार वाला मान)” को लौटाता है।

अस्तित्व प्रतीक (Existential Symbol) $\exists$ और डिपेंडेंट सम टाइप ($\Sigma$ प्रकार)

अस्तित्वपरक प्रस्ताव (existential proposition) $\exists x:A, B(x)$ कि “एक $x \in A$ मौजूद है जिसके लिए $B(x)$ मान्य है” को “शर्त को पूरा करने वाले एक विशिष्ट मान $x$” और “उस प्रमाण के रूप में कि $x$ शर्त को पूरा करता है” की एक जोड़ी के रूप में दर्शाया जाता है। इसे $\Sigma$ प्रकार (Sigma Type, Dependent Sum Type) कहा जाता है।

$$ \frac{\Gamma \vdash M : A \quad \Gamma \vdash N : B(M)}{\Gamma \vdash (M, N) : \Sigma x:A. B(x)} \quad (\Sigma\text{-}I) $$

इसके परिणामस्वरूप, “सॉर्ट की गई सरणी (sorted array) लौटाने वाला फ़ंक्शन” केवल एक सरणी लौटाने के बजाय, “लौटाई गई सरणी $y$” और “प्रमाण कि $y$ सॉर्ट की गई है” की $\Sigma$ जोड़ी लौटाने वाले फ़ंक्शन के रूप में कड़ाई से टाइप करने योग्य हो जाता है। यह “करेक्ट-बाय-कंस्ट्रक्शन (Correct-by-Construction - निर्माण द्वारा शुद्धता की गारंटी)” की नींव है।

अध्याय 5: Lean 4 / Coq के साथ गणितीय प्रमेयों का प्रमाण और स्पष्टीकरण (व्यावहारिक संस्करण)

आइए देखें कि डिपेंडेंट टाइप थ्योरी पर आधारित आधुनिक प्रमेय प्रमाण सहायकों (Theorem Proof Assistants जैसे Lean 4 और Coq) का उपयोग करके वास्तविक गणितीय प्रमाणों को प्रोग्राम के रूप में कैसे लिखा जाता है।

डी मॉर्गन का नियम (इंट्यूशनिस्टिक सत्यापन)

शास्त्रीय तर्कशास्त्र (Classical logic) में $\neg(A \lor B) \iff \neg A \land \neg B$ मान्य है, लेकिन इंट्यूशनिस्टिक लॉजिक में भी इस दिशा को साबित किया जा सकता है। Lean 4 में इसका प्रमाण नीचे दिया गया है। ध्यान दें कि Lean में, नकार (negation) $\neg A$ को $A \to \bot$ (एक फ़ंक्शन जो A को मानने पर विरोधाभास की ओर ले जाता है) के रूप में परिभाषित किया गया है।

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
-- Lean 4: डी मॉर्गन के नियम का एक भाग ¬(A ∨ B) → ¬A ∧ ¬B
theorem de_morgan_1 {A B : Prop} (h : ¬(A ∨ B)) : ¬A ∧ ¬B :=
  -- And.intro संयोजन (∧) का परिचय नियम (जोड़ी का निर्माण) है।
  And.intro
    -- पहला तत्व: ¬A का प्रमाण (अर्थात् A → False)
    (fun (ha : A) =>
      -- A से A ∨ B का निर्माण करें (Or.inl), और विरोधाभास (False) प्राप्त करने के लिए इसे h पर लागू करें
      h (Or.inl ha))
    -- दूसरा तत्व: ¬B का प्रमाण (अर्थात् B → False)
    (fun (hb : B) =>
      -- B से A ∨ B का निर्माण करें (Or.inr), और विरोधाभास (False) प्राप्त करने के लिए इसे h पर लागू करें
      h (Or.inr hb))

पंक्ति-दर-पंक्ति व्याख्या:

h : ¬(A ∨ B) प्रकार (A ∨ B) → False का एक फ़ंक्शन है।
And.intro द्वारा, ¬A और ¬B के प्रमाणों की एक जोड़ी का निर्माण किया जाता है।
fun (ha : A) => ... एक लैम्ब्डा एब्स्ट्रेक्शन (फ़ंक्शन की परिभाषा) है। तर्क ha का उपयोग करके, हम Or.inl ha के साथ A ∨ B का प्रमाण बनाते हैं, और इसे फ़ंक्शन h को पास करके False वापस करते हैं।

इस प्रकार, एक प्रमाण कुछ और नहीं बल्कि पूरी तरह से प्रकार-सुरक्षित (type-safe) लैम्ब्डा एक्सप्रेशन का निर्माण है।

सूची संयोजन (List Concatenation) की साहचर्य संपत्ति (Associativity) का आगमनात्मक (Inductive) प्रमाण

प्रोग्रामिंग में प्रसिद्ध सूची संयोजन ऑपरेशन ++ के संबंध में, हम गणितीय आगमन (mathematical induction) का उपयोग करके साहचर्य संपत्ति (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) को साबित करेंगे। टाइप थ्योरी में, आगमन को “पुनरावर्ती फ़ंक्शन (Recursive Function)” के रूप में महसूस किया जाता है।

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
-- Lean 4: सूची संयोजन की साहचर्य संपत्ति
theorem append_assoc {α : Type} (l1 l2 l3 : List α) : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) :=
  match l1 with
  -- बेस केस: यदि l1 एक खाली सूची [] है
  | [] =>
    -- क्योंकि [] ++ l2 को l2 में कम (reduce) किया जाता है, l2 ++ l3 = l2 ++ l3 हो जाता है जो कि स्वयं स्पष्ट है (Reflexivity)
    rfl
  -- आगमनात्मक कदम (Inductive step): यदि l1, head :: tail है
  | head :: tail =>
    -- आगमन परिकल्पना (पुनरावर्ती कॉल) के रूप में tail के लिए साहचर्य संपत्ति का उपयोग करें
    have ih : (tail ++ l2) ++ l3 = tail ++ (l2 ++ l3) := append_assoc tail l2 l3
    -- (head :: tail ++ l2) ++ l3 को head :: ((tail ++ l2) ++ l3) में कम कर दिया जाता है
    -- आगमन परिकल्पना `ih` का उपयोग करके अभिव्यक्ति को फिर से लिखें (rewrite)
    by rw [ih]

यहाँ, सूची की संरचना पर पैटर्न मिलान match गणितीय आगमन की संरचना प्रदान करता है, और पुनरावर्ती कॉल append_assoc tail l2 l3 आगमन परिकल्पना (Induction Hypothesis) से मेल खाती है। चूँकि पुनरावर्तन (recursion) के रुकने की गारंटी है, इसलिए यह एक सुदृढ़ प्रमाण बन जाता है।

अध्याय 6: सिस्टम एफ, पॉलीमॉर्फिक लैम्ब्डा कैलकुलस, यूनिवर्स लेवल्स और जेरार्ड का विरोधाभास

अभिव्यक्ति (expressive power) को और अधिक बढ़ाने के लिए, हम “बहुरूपता (Polymorphism)” का परिचय देते हैं जो प्रकारों (types) को पैरामीटर के रूप में लेता है। यह “सिस्टम एफ (System F)” या “सेकंड-ऑर्डर लैम्ब्डा कैलकुलस” है, जिसे स्वतंत्र रूप से जीन-यवेस जेरार्ड (Jean-Yves Girard) और जॉन रेनॉल्ड्स (John Reynolds) द्वारा खोजा गया था।

सिस्टम एफ और सार्वभौमिक परिमाणीकरण (Universal Quantification)

सिस्टम एफ में, प्रकार चर (type variables) पर सार्वभौमिक परिमाणीकरण $\forall \alpha. \tau$ को एक प्रकार के रूप में अनुमति दी जाती है। इसने हास्केल (Haskell) जैसे जेनरिक (पैरामीट्रिक पॉलीमॉर्फिज्म - Parametric Polymorphism) की नींव रखी। उदाहरण के लिए, पॉलीमॉर्फिक आइडेंटिटी फ़ंक्शन id का प्रकार $\forall \alpha. \alpha \to \alpha$ है। तार्किक रूप से, यह “सेकंड-ऑर्डर प्रपोजिशनल लॉजिक (तर्कशास्त्र जो प्रस्ताव संबंधी चरों के परिमाणीकरण की अनुमति देता है)” से मेल खाता है।

यूनिवर्स लेवल्स (Universe Levels) और जेरार्ड का विरोधाभास (Girard’s Paradox)

सिस्टम एफ या डिपेंडेंट टाइप थ्योरी को डिज़ाइन करते समय, क्या “सभी प्रकारों के सेट” का प्रतिनिधित्व करने वाला प्रकार Type स्वयं को एक प्रकार के रूप में रख सकता है (Type : Type)?

यदि हम इसकी अनुमति देते हैं, तो टाइप थ्योरी में रसेल का विरोधाभास (Russell’s Paradox) यानी “जेरार्ड का विरोधाभास (Girard’s Paradox)” उत्पन्न होता है। सीज़ारे बुराली-फोर्टि (Cesare Burali-Forti) के विरोधाभास के समान, क्रमिक संख्याओं (ordinal numbers) की संरचना का उपयोग करके “सभी क्रमिक संख्याओं का सेट” बनाना और आत्म-संदर्भ (self-reference) द्वारा विरोधाभास ($\bot$ का प्रमाण) प्राप्त करना संभव हो जाता है।

इसे रोकने के लिए, आधुनिक डिपेंडेंट टाइप थ्योरी (जैसे Coq और Lean) यूनिवर्स लेवल्स (Universe Levels) का परिचय देती है। Type 0 नियमित डेटा प्रकारों (Nat, Bool) का प्रकार है। स्वयं Type 0 का प्रकार Type 1 है, और Type 1 का प्रकार Type 2 है, जिससे एक अनंत पदानुक्रम (hierarchy) बनता है:

$$ \text{Type}_0 : \text{Type}_1 : \text{Type}_2 : \dots $$

यह आत्म-संदर्भ को रोकता है और तर्क की स्थिरता (consistency) को बनाए रखते हुए समृद्ध गणितीय संरचनाओं को व्यक्त करना संभव बनाता है।

अध्याय 7: होमोटोपी टाइप थ्योरी (HoTT) में पहचान प्रकार (Identity Types) और पथों (Paths) की टोपोलॉजिकल (Topological) व्याख्या

21वीं सदी में प्रवेश करते हुए, करी-हावर्ड पत्राचार टोपोलॉजी (Topology) और श्रेणी सिद्धांत (Category Theory) के साथ जुड़ गया, और एक नया प्रतिमान “होमोटोपी टाइप थ्योरी (Homotopy Type Theory; HoTT)” बनाया। फील्ड्स मेडल विजेता व्लादिमीर वोएवोड्स्की (Vladimir Voevodsky) और अन्य लोगों के नेतृत्व में यह सिद्धांत गणित की नींव को मौलिक रूप से फिर से लिखने की कोशिश कर रहा है।

पहचान प्रकार (Identity Types) और पथ (Paths)

डिपेंडेंट टाइप थ्योरी में, यह दावा कि “$x$ और $y$ समान हैं” को पहचान प्रकार (Identity Type) $Id_A(x, y)$ के प्रकार के रूप में दर्शाया गया है। आमतौर पर, इसे केवल रिफ्लेक्सिविटी ($x = x$) द्वारा सिद्ध करने योग्य माना जाता है (refl : Id_A(x, x))।

हालाँकि, HoTT में, हम इस $Id_A(x, y)$ के प्रमाण $p$ को एक टोपोलॉजिकल अर्थ देते हैं। अर्थात्, “प्रमाण $p : Id_A(x, y)$” की व्याख्या “अंतरिक्ष $A$ पर बिंदु $x$ से बिंदु $y$ तक के एक पथ (Path)” के रूप में की जाती है। इसके अलावा, जब $p, q : Id_A(x, y)$ दो अलग-अलग प्रमाण (पथ) मौजूद होते हैं, तो यह प्रमाण कि वे समान हैं $\alpha : Id_{Id_A(x, y)}(p, q)$, पथ $p$ से पथ $q$ तक निरंतर विरूपण (continuous deformation) होने वाले “होमोटोपी (Homotopy)” के अनुरूप होता है। इसके परिणामस्वरूप, टाइप थ्योरी में अनंत हायर ग्रुपॉइड (Higher Groupoid) की संरचना स्वाभाविक रूप से प्रकट होती है।

J-एलिमिनेटर और पथ आगमन (Path Induction)

पहचान प्रकार का उन्मूलन नियम, J-एलिमिनेटर (J-eliminator / Path Induction), HoTT में अत्यंत महत्वपूर्ण भूमिका निभाता है। यह नियम है कि “समीकरण $x = y$ पर निर्भर करने वाले प्रस्ताव $P(x, y, p)$ को साबित करने के लिए, केवल उस मामले (बेस केस) को साबित करना पर्याप्त है जहां $x = x$ और $p = \text{refl}$ है”। टोपोलॉजिकल रूप से, यह इस तथ्य से मेल खाता है कि “बिंदु $x$ पर रहने वाला एक स्थिर (constant) पथ किसी भी पथ में निरंतर विकृत (contractibility) हो सकता है”।

यूनीवैलेंस स्वयंसिद्ध (Univalence Axiom)

वोएवोड्स्की द्वारा पेश की गई सबसे बड़ी सफलता “यूनीवैलेंस स्वयंसिद्ध (Univalence Axiom)” है। गणित में, आइसोमोर्फिक (Isomorphic) संरचनाओं (उदाहरण के लिए, समान तत्वों वाले दो परिमित सेट, या समान संरचना वाले दो समूह) को “अनिवार्य रूप से समान” माना जाता है। हालाँकि, पारंपरिक सेट थ्योरी (ZFC) में, भले ही वे आइसोमोर्फिक हों, उन्हें कड़ाई से “समान” नहीं कहा जा सकता था।

यूनीवैलेंस स्वयंसिद्ध यह दावा करता है कि प्रकार $A$ और प्रकार $B$ का समतुल्य (Equivalent, $A \simeq B$) होना और उनका “समान ($Id_{\text{Universe}}(A, B)$)” होना एक ही बात है।

$$ (A \simeq B) \simeq Id_{\text{Type}}(A, B) $$

एक नारे के रूप में कहा जाए तो: “समानता ही समतुल्यता है (Equality is Equivalence)”।

इस स्वयंसिद्ध (axiom) के साथ, “पथ के साथ परिवहन (Transport)” का उपयोग करके एक प्रतिनिधित्व में सिद्ध किए गए प्रमेय को स्वचालित रूप से और सुरक्षित रूप से पूरी तरह से अलग आइसोमोर्फिक प्रतिनिधित्व में उठाना संभव हो जाता है। प्रोग्रामिंग के दृष्टिकोण से, यदि आप डेटा संरचनाओं (उदाहरण: बाइनरी प्रतिनिधित्व और यूनरी प्रतिनिधित्व में प्राकृत संख्या) के बीच आइसोमोर्फिज्म को एक बार साबित करते हैं, तो आप अंतिम जेनरिक (ultimate generics) को महसूस कर सकते हैं जो स्वचालित रूप से एक डेटा संरचना के लिए लिखे गए सभी कार्यों और प्रमेयों को दूसरे में अनुकूलित कर सकता है।

निष्कर्ष: प्रोग्रामिंग और सार्वभौमिक सत्य की खोज

करी-हावर्ड आइसोमोर्फिज्म हमें जो सबसे महत्वपूर्ण सत्य सिखाता है, वह यह तथ्य है कि “गणित” और “कंप्यूटर विज्ञान” अनिवार्य रूप से एक ही भाषा बोलते हैं। जब हम अपनी रोज़मर्रा की प्रोग्रामिंग में टाइप त्रुटियों से संघर्ष कर रहे होते हैं, तो यह कंपाइलर नामक एक स्वचालित प्रमाण सत्यापनकर्ता (automatic proof verifier) के माध्यम से तार्किक विरोधाभासों को ठीक करने के अलावा और कुछ नहीं है।

प्रस्ताव (Proposition), प्रकार (Type) है
प्रमाण (Proof), प्रोग्राम (Program) है
प्रमाण का सामान्यीकरण (Cut Elimination), प्रोग्राम का निष्पादन ($\beta$-Reduction) है

फ़ंक्शनल प्रोग्रामिंग भाषाओं (जैसे Haskell, OCaml, Rust, आदि) में जो शक्तिशाली प्रकार प्रणालियाँ (type systems) हैं, वे इस आइसोमोर्फिज्म पत्राचार से बहुत लाभान्वित होती हैं। और Coq और Lean 4 जैसे प्रमेय प्रमाण सहायक ने प्रोग्रामिंग और गणित के बीच की सीमा को पूरी तरह से मिटा दिया है। हम जो कोड लिखते हैं वह एक निष्पादन योग्य एल्गोरिदम होने के साथ-साथ सार्वभौमिक गणितीय सत्य का प्रमाण पत्र (Certificate) भी बन जाता है जो हमेशा के लिए गारंटी देता है कि इसमें कोई बग मौजूद नहीं है।

टाइप थ्योरी और तर्कशास्त्र के चौराहे से पैदा हुआ यह गहरा सामंजस्य सॉफ्टवेयर इंजीनियरिंग को केवल “अनुभवजन्य नियमों (rules of thumb) पर आधारित कोडिंग” से “सख्त गणितीय नींव पर आधारित सत्य के निर्माण” की ओर ले जाना जारी रखे हुए है।