कोक में एक निर्माता क्या है?

Question

मुझे कन्स्ट्रक्टर के सिद्धांतों के बारे में समझने में समस्या हो रही है और यह कैसे काम करता है।

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

Inductive nat : Type := 
    | O : nat 
    | S : nat -> nat. 

और बताया गया है कि S एक निर्माता है, लेकिन यह वास्तव में क्या मतलब है?

अगर मैं तो कार्य करें:

Check (S (S (S (S O)))). 

मुझे लगता है कि यह 4 और के प्रकार nat है मिलता है।

यह कैसे काम करता है, और कोक कैसे जानता है कि (S (S (S (S O))))4 का प्रतिनिधित्व करता है?

मुझे लगता है कि इसका उत्तर कोक में कुछ बेहद चालाक पृष्ठभूमि जादू है।

Answer 1

Inductive naturals : Type := 
    | Z : naturals 
    | N : naturals -> naturals. 

कहते हैं निम्नलिखित बातें:

1. Z प्रकार naturals

2. का एक शब्द है जब e प्रकार naturals का एक शब्द है, N e प्रकार naturals का एक शब्द है।

3. Z या N लागू करने से प्राकृतिक बनाने के लिए केवल दो तरीके हैं। जब मनमाना प्राकृतिक दिया जाता है, तो आप जानते हैं कि यह या तो एक या दूसरे से बनाया गया था।

4. दो शब्दों e1 और प्रकार naturals की e2 हैं बराबर यदि और केवल यदि वे दोनों Z हैं या वे क्रमशः N t1 और t1t2 के बराबर के साथ N t2 हैं।

आप देख सकते हैं कि ये नियम मनमाने ढंग से अपरिवर्तनीय प्रकार की परिभाषाओं को कैसे सामान्यीकृत करेंगे। हालांकि, यह पता चला है कि जब टाइप परिभाषा Z और N के आकार के रचनाकारों के लिए है, तो ये गुण प्राकृतिक संख्याओं के लिए Peano's axioms से कम या कम मेल खाते हैं। यही कारण है कि nat नामक एक प्रकार को प्राकृतिक आकारों का प्रतिनिधित्व करने के लिए इन आकारों के रचनाकारों के साथ कोक में पूर्व परिभाषित किया गया है। इस प्रकार को विशेष उपचार प्राप्त होता है क्योंकि कच्चे रूप में हेरफेर करने के लिए यह बहुत जल्दी थकाऊ हो जाता है, लेकिन विशेष उपचार केवल सुविधा के लिए होते हैं।

Answer 2

टाइप सिद्धांत में, एक (प्रकार) कन्स्ट्रक्टर मौजूदा लोगों (http://en.wikipedia.org/wiki/Type_constructor) से नए प्रकार बनाने का एक तरीका है।

नाट की आपकी अनिवार्य परिभाषा में, एस एक कन्स्ट्रक्टर है क्योंकि (यदि आप हस्ताक्षर को देखते हैं) तो यह एक नट लेता है और एक और नाट उत्पन्न करता है।

उदाहरण के लिए, Nats की एक जोड़ी के लिए एक प्रकार का निर्माता हो जाएगा:

Inductive pair : Type := P: nat->nat->pair. 

Check P (S (O)) (S(S(O))).