बहु-मार्ग (गुलाब) पेड़ों के लिए संरचनात्मक प्रेरण - हैकेल, पेड़, सबूत, प्रेरण

चूंकि बहु-प्रकार के पेड़ों को एक पुनरावर्ती प्रकार के रूप में परिभाषित किया जा सकता है:

data RoseTree a = Node {leaf :: a, subTrees :: [RoseTree a]}

क्या इस प्रकार पर संरचनात्मक प्रेरण करने के लिए एक समान सिद्धांत है?

उत्तर:

उस संपत्ति का उल्लेख करने के लिए P सभी (*) गुलाब के पेड़ों के लिए, आपको यह साबित करना होगा

• अगर l :: [RoseTree] गुलाब के पेड़ों की सूची है जिनके तत्व संतुष्ट करते हैं P, तथा x :: a मनमाना है, फिर Note x l संतुष्ट P

के बारे में हिस्सा है P के तत्वों पर पकड़ l प्रेरण परिकल्पना है, जिसे आप साबित करने के लिए उपयोग कर सकते हैं P(Node x l).

यहाँ कोई स्पष्ट आधार मामला नहीं है: इसका कारण यह है कि कोई स्पष्ट आधार मामला निर्माता नहीं है। Node x [] पेड़ों के लिए एक अंतर्निहित आधार मामले के रूप में कार्य करता है, और वास्तव में जब l खाली है हमें अंतर्निहित रूप से प्रेरण के लिए एक आधार मामला मिलता है। अफसोस, परिकल्पना "के सभी तत्वों l बदला देना P"जब वास्तव में सच हो जाता है l खाली है, इसलिए हम मिलते हैं P(Node x []) ऊपर दिए गए प्रेरण सिद्धांत से।

(*) अधिक सटीक रूप से, यह सिद्धांत सिद्ध होता है P हर परिमित गहराई वाले गुलाब के पेड़ के लिए। यदि आपको वास्तव में अनंत-गहराई वाले लोगों (जैसे वृत्ताकार वृक्षों) पर विचार करना है, तो आपको सहवास की आवश्यकता है।