में कार्यात्मक विस्तारशीलता का उपयोग करने का नकारात्मक पक्ष क्या है सीओक्यू में एक्सीम्स जोड़ना अक्सर सबूत आसान बनाता है लेकिन कुछ दुष्प्रभाव भी पेश करता है। उदाहरण के लिए, शास्त्रीय का उपयोग करके एक व्यक्ति अंतर्ज्ञानवादी क्षेत्र छोड़ देता है और सबूत अब गणना नहीं कर सकते हैं। मेरा सवाल है, कार्यात्मक विस्तार एक्सीमॉम का उपयोग करने का नकारात्मक पक्ष क्या है?सीओक्यू
मेरे लिए, कार्यात्मक विस्तारशीलता का उपयोग करने की कमी कोक में किसी भी अन्य सिद्धांत का उपयोग करने के समान ही कम है: यह प्रणाली की जटिलता को बढ़ाता है और हमें कितना भरोसा करने की आवश्यकता है। यद्यपि सिद्धांत में हम इन सुप्रसिद्ध सिद्धांतों के साथ काम करने के तार्किक परिणामों को काफी अच्छी तरह समझते हैं (उदाहरण के लिए, स्थिरता सुनिश्चित करने के लिए सिद्धांतों के संयोजनों से बचा जाना चाहिए), अभ्यास में हमें कभी-कभी गार्ड से पकड़ा जाता है। उदाहरण के लिए, यह recently found out था कि प्रस्तावांक विस्तार वसंत संस्करण 8.4 में कोक के सिद्धांत के साथ असंगत था, भले ही इसे व्यापक रूप से संगत माना जाता था। यह प्रतीत होता है प्राकृतिक स्वयंसिद्ध बस का कहना है कि बराबर प्रस्ताव के बराबर हैं, और कई Coq के घटनाक्रम में अपनाया जाता है:
Axiom propositional_extensionality :
forall P Q : Prop, (P <-> Q) -> P = Q.
जवाब linked above में, एंड्रेज बॉयर पता चलता है कि इस कमजोरी इन गणना के साथ जुड़े नियम नहीं होने सूक्तियों से संबंधित हो सकता उन्हें, कोक के सिद्धांत के बाकी हिस्सों के विपरीत।
इस सामान्य टिप्पणी के अलावा, मैंने लोगों को यह कहते हुए सुना है कि डिफ़ॉल्ट रूप से कार्यात्मक विस्तारशीलता अवांछनीय हो सकती है क्योंकि यह बहुत अलग कम्प्यूटेशनल व्यवहार (उदाहरण के लिए, बबल सॉर्ट और त्वरित सॉर्ट) के साथ कार्यों को समानता देती है, और हम कारण चाहते हैं इन मतभेदों के बारे में। मैं व्यक्तिगत रूप से इस तर्क को नहीं खरीदता, क्योंकि कोक पहले से ही कई मान समझाता है, जो 0 और 47^1729 - 47 mod 1729 जैसे बहुत अलग गणना की जाती हैं। मैं कार्यात्मक विस्तार को मानने के इच्छुक नहीं होने के अन्य कारणों से अवगत नहीं हूं।
मुझे लगता है कि अंतिम पैराग्राफ में आपकी तुलना थोड़ा सा त्रुटिपूर्ण है। आप मॉड फॉर्मूला को शून्य में सरल बना सकते हैं लेकिन आप कुछ कैननिकल सॉर्टिंग एल्गोरिदम को बबल सॉर्ट और त्वरित सॉर्ट को सरल नहीं बना सकते हैं। साथ ही, मॉड फॉर्मूला को पूर्व-गणना की जा सकती है लेकिन एक अनंत अपरिवर्तनीय प्रकार पर एक फ़ंक्शन हमेशा मांग पर गणना की जाती है। – Cryptostasis
मैं आर्थर से सहमत हूं कि कार्यात्मक विस्तारशीलता सिद्धांत हानिकारक है और इसे अस्वीकार करने के लिए कुछ आकर्षक तर्क हैं। कोक में इसकी "विफलता" को किसी अन्य गहरे कारण से अधिक वाक्य रचनात्मक तरीकों की सीमा के रूप में देखा जा सकता है। व्यक्तिगत रूप से, मैं सिद्धांतों से बचने की कोशिश करता हूं, इस प्रकार यदि संभव हो तो मैं विस्तारित वांछित टेबलों के रूप में कार्यों का प्रतिनिधित्व करता हूं। – ejgallego
बस एडम चिपिपला द्वारा पढ़ा गया है कि सरल समानता: 'प्रमेय दो_फन: (मजेदार एन => एन) = (मजेदार एन => एन + 0) 'कार्यात्मक विस्तारशीलता के बिना सीओक्यू में साबित नहीं है। यह मुझे इंप्रेशन देता है कि इस वसंत के बिना कोई बहुत दूर नहीं होगा। – Cryptostasis
एक समान [प्रश्न] (http://mathoverflow.net/questions/156238/function-extensionality-does-it-make-a-difference-why-would-one-keep-it-out-of) - इसके भाग 2 और [स्वीकृत उत्तर] देखें (http://mathoverflow.net/a/156295)। –