Coq के लिए नरम परिचय: आगमनात्मक परिभाषाएँ

पिछले भाग में, हमने सीखा कि नए प्रकार कैसे सेट करें और उनके मूल्यों पर कार्य करें। इस संक्षिप्त लेख में, मैं अध्ययन के लिए आगे के विषयों को स्पष्ट करने और रेखांकित करने के लिए आगमनात्मक परिभाषाओं पर अधिक विस्तार से बताऊंगा।

मैंने पहले कहा था कि Coq में बैटरी नहीं हैं। दरअसल, मैं चालाक था - कोक के पास एक मानक पुस्तकालय है जिसमें कई उपयोगी परिभाषाएँ हैं। मानक पुस्तकालय के अतिरिक्त, कुछ और भी विशिष्ट चीजें हैं जिनके लिए हम अभी निवास नहीं करेंगे।

CoIDEIDE के प्रारंभ में, कुछ पुस्तकालय पृष्ठभूमि में मित्र बन जाते हैं, जिनमें से एक सूची Print Libraries कमांड का उपयोग करके देखी जा सकती है:

 भरी हुई और आयातित पुस्तकालय फाइलें: 
   Coq.Init.Notations 
   Coq.Init.Logic 
   Coq.Init.Datatypes 
   Coq.Init.Specif 
   Coq.Init.Peano 
   Coq.Init.Wf 
   Coq.Init.Tactics 
   Coq.Init.Prelude 
   Coq.Init.Logic_Type

शैक्षणिक उद्देश्यों के लिए, हम इन पुस्तकालयों की परिभाषाओं का उपयोग नहीं करेंगे।

जैसा कि आप जानते हैं, कार्यात्मक प्रोग्रामिंग पर कोई परिचयात्मक लेख तथ्य की गणना के बिना नहीं कर सकता है। हम इस परंपरा से विदा नहीं लेंगे और प्रेरक प्रकारों के साथ अपने स्वयं के तथ्य को लिखेंगे।

प्राकृतिक संख्या

गणित में हर जगह प्रेरक परिभाषाएँ पाई जाती हैं। उदाहरण के लिए, सेट सिद्धांत के दृष्टिकोण से प्राकृतिक संख्याएं निम्नानुसार पेश की गई हैं:



इसी तरह, हम Coq में प्राकृतिक संख्याओं को परिभाषित कर सकते हैं। नाम स्थान को रोकना नहीं करने के लिए, हम मॉड्यूल सिस्टम का उपयोग करते हैं:

 मॉड्यूल टेस्ट 1। 

 आगमनात्मक नट: प्रकार: = 
   |  ओ: नट 
   |  स: नट -> नट। 

इस घोषणा को इस तरह पढ़ना चाहिए:

1. O एक प्राकृतिक संख्या है,
2. S एक कंस्ट्रक्टर है जो एक सकारात्मक पूर्णांक लेता है और एक और सकारात्मक पूर्णांक लौटाता है: यदि n construct N, तो S n ∈ N।

इस परिभाषा का उपयोग करके, हम किसी भी प्राकृतिक संख्या का निर्माण कर सकते हैं:

 (एसओ) में सरल साक्ष्य।
 (* ==> 1: nat *)
 में सरल (एस (एसओ))।
 (* ==> 2: nat *)
 में सरल (एस (एस (एसओ)))।
 (* ==> 3: nat *)

अब जब हमारे पास प्राकृतिक संख्याएं हैं, तो इन संख्याओं पर कार्यों के एक सेट को परिभाषित करने का समय है:

 फ़िक्सपॉइंट प्लस (n: nat) (m: nat): nat: =
   n के साथ मैच
     |  ओ => म
     |  S n '=> S (प्लस n' m)
   अंत।

यहां हमने एक पुनरावर्ती ( Fixpoint कीवर्ड) plus फ़ंक्शन को परिभाषित किया है जो इनपुट के रूप में दो nat तर्क लेता है और टाइप Fixpoint एक परिणाम देता है। आप इसे Check कमांड से सत्यापित कर सकते हैं:

 प्लस चेक करें।
 (* ==> प्लस: नेट -> नेट -> नेट *)

एक विशिष्ट उदाहरण पर उसके काम पर विचार करें। हम अभिव्यक्ति 3 + 2 के मूल्य की गणना करते हैं:

 ((एस (एस (एस))) (एस (एसओ))) में सरल साक्ष्य।
 (* ==> 5: nat *)

बहुत बढ़िया! सब कुछ काम करता है। लेकिन इसका परिणाम कैसे होता है?

 (* प्लस (एस (एस (एसओ))) (एस (एसओ))    
 ==> एस (प्लस (एस (एसओ)) (एस (एसओ)) परिभाषा में दूसरा खंड
 ==> एस (एस (प्लस (एसओ) (एस (एसओ)))) परिभाषा में दूसरा खंड
 ==> एस (एस (एस (प्लस ओ (एस))))) परिभाषा में दूसरा खंड
 ==> एस (एस (एस (एस (एस)))) परिभाषा में पहला खंड है
 *)

इसी तरह से, आप एक गुणन फ़ंक्शन लिख सकते हैं और तथ्यात्मक गणना को लागू कर सकते हैं, जिसके बिना कार्यात्मक प्रोग्रामिंग पर एक भी पाठ्यपुस्तक नहीं दी जा सकती है:

 फिक्स पॉइंट मल्टी (nm: nat): nat: =
   n के साथ मैच
     |  ओ => ओ
     |  S n '=> प्लस m (बहु n' m)
   अंत।

 नियतांक तथ्य (n: nat): nat: =
   n के साथ मैच
     |  ओ => एसओ
     |  S n '=> बहु n (भाज्य n')
   अंत।

 में सरल (तथ्यात्मक (एस (एस (एस (एस (एस)))))))।
 (* ==> 120: nat *)

निष्कर्ष

सामग्री को मजबूत करने के लिए, मैं दृढ़ता से अनुशंसा करता हूं कि पाठक कोकाइड में सभी उदाहरणों को चलाएं। अगले भाग में, हम मूल Coq रणनीति के साथ काम करने पर विचार करेंगे।

जारी रखा जाए ।