वे समान उद्देश्यों को पूरा करते हैं। अब तक मैंने जो अंतर देखा है वह यह है कि Program Fixpoint{measure (length l1 + length l2) }, Function जैसे यौगिक उपाय स्वीकार करेगा, इसे अस्वीकार कर दिया जाएगा और केवल {measure length l1} की अनुमति देगा।कोक में प्रोग्राम फिक्सपॉइंट और फ़ंक्शन के बीच क्या अंतर है?
Program FixpointFunction से सख्ती से अधिक शक्तिशाली है, या वे विभिन्न उपयोग मामलों के लिए बेहतर अनुकूल हैं?
यह एक पूरी सूची नहीं हो सकता है, लेकिन यह मैं अब तक क्या पाया है है:
Program Fixpoint उपाय एक से अधिक तर्क को देखने के लिए अनुमति देता है।Functionfoo_equation लेम्मा बनाता है जिसका उपयोग foo पर अपने आरएचएस के साथ कॉल को फिर से लिखने के लिए किया जा सकता है। Coq simpl for Program Fixpoint जैसी समस्याओं से बचने के लिए बहुत उपयोगी है।Functionfoo की पुनरावर्ती कॉल की संरचना के साथ प्रेरण प्रदर्शन करने के लिए एक foo_ind लेम्मा परिभाषित कर सकते हैं। फिर, सबूत में समाप्ति तर्क को प्रभावी ढंग से दोहराए बिना foo के बारे में चीजों को साबित करने के लिए बहुत उपयोगी है।Program Fixpoint नेस्टेड रिकर्सन का समर्थन करने में धोखा दिया जा सकता है, https://stackoverflow.com/a/46859452/946226 देखें। यह भी है कि Program Fixpointdefine the Ackermann फ़ंक्शन Function नहीं कर सकता है।'फ़ंक्शन' के साथ एकरमेन फ़ंक्शन को परिभाषित करना भी असंभव प्रतीत होता है, लेकिन 'प्रोग्राम फिक्सपॉइंट' [यह कर सकता है] (https://stackoverflow.com/questions/10292421/error-in-defining-ackermann-in-coq) । –
धन्यवाद, उत्तर में कहा गया। –
संयोग से, [Coq v8.7 रोडमैप] (https://github.com/coq/roadmaps/blob/master/text/roadmap-8.7.md#implementation-cleanups) का कहना है कि उनके कार्यान्वयन विलय हो। –
यह एक अच्छा सवाल है, मैं आपको कोक के गिटर पर जाने की सलाह देता हूं यदि आपको विस्तृत उत्तर देने की आवश्यकता है क्योंकि लोगों को इसके बारे में जानकारियों को पढ़ना नहीं है SO AFAIK; फंक्शन और प्रोग्राम का कार्यान्वयन विभिन्न व्यक्तियों द्वारा और विभिन्न संदर्भों में किया गया था, इसलिए वास्तव में उनके विशेषताओं का सेट दूसरे के सब्सट्रेट का सख्ती से नहीं है। एक नई "समीकरण" प्लगइन में दोनों पर विलय करने की योजना है, लेकिन यह 8.7 में नहीं होगा, भले ही बहुत प्रगति हुई हो। ऐसा कहा जा रहा है कि, मुझे लगता है कि अगर आप भावी कोक रिलीज के साथ संगतता की परवाह करते हैं तो आप आम तौर पर कार्यक्रम से बेहतर होंगे। – ejgallego