के अभ्यावेदन पर मैं क्रमपरिवर्तन और कुछ कंटेनरों पर उनकी कार्रवाई का वर्णन करने के लिए एक आगमनात्मक प्रकार करना चाहते हैं। यह स्पष्ट है कि इस प्रकार के वर्णन के आधार पर परिभाषा जटिलता (इसकी लंबाई के संदर्भ में) एल्गोरिदम (कंप्यूटिंग संरचना या उलटा, विघटन चक्रों में विघटन, आदि) अलग-अलग होंगे।क्रमपरिवर्तन
Coq में निम्नलिखित परिभाषा पर विचार करें। मेरा मानना है कि यह लेह्मर कोड का औपचारिक होने के लिए: रचना की औपचारिक पता लगाने के लिए (कम से कम मेरे लिए) हार्ड
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
यह अपनी कार्रवाई अन्य कंटेनरों पर थोड़ा कठिन है, आकार n का वैक्टर पर परिभाषित करने के लिए आसान है और या श्लोक में।
वैकल्पिक रूप से हम गुणों के साथ एक परिमित नक्शे के रूप में परिवर्तन का प्रतिनिधित्व कर सकते हैं। संरचना या उलटा आसानी से परिभाषित किया जा सकता है लेकिन इसे विषम चक्रों में विघटित करना मुश्किल है।
तो मेरे सवाल है: क्या कोई कागजात है कि इस व्यापार बंद मुद्दे के समाधान कर रहे हैं? सभी कार्यों, जिन्हें मैं ढूंढने में कामयाब रहा, अनिवार्य सेटिंग्स में एक कम्प्यूटेशनल जटिलता से निपटता हूं, जबकि मुझे "तर्क जटिलता" और कार्यात्मक प्रोग्रामिंग में रूचि है।
मुझे कोक के बारे में कुछ नहीं पता, लेकिन क्या यह मदद करता है? http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html –
दुर्भाग्यवश, ऐसा नहीं है। मैं चाहता हूं कि एक कंटेनर के संदर्भ के बिना क्रमपरिवर्तन के एन्कोडिंग। हालांकि उल्लेख किया गया है कि संबंध के संबंध में एक कंटेनर-जेनेरिक परिभाषा होना सुखद होगा। –
शायद आप इसे विशेषज्ञ बना सकते हैं, इसलिए यह सूचकांक की क्रमबद्ध सूची की अनुमति देता है? –